def BonyClosure.geometric_gain_summable : Prop

The formal definition of the fundamental geometric gain convergence that neutralizes the dyadic derivative divergence.

Equations

• BonyClosure.geometric_gain_summable = Summable fun (j : ℕ) => 2 ^ (-↑j / 2)

theorem BonyClosure.geometric_gain_converges : geometric_gain_summable

We prove the convergence of this geometric series formally. This follows from the ratio test since 2^(-1/2) < 1.

structure BonyClosure.BonyClosureTheorem (alpha : ℝ) : Type

The Bony Closure Theorem (Abstract Constraint). Given the Van der Corput gain from the Restricted Hessian and the dyadic projection bounds, the nonlinear paraproduct term is structurally bounded. If we are in the subcritical regime with $\alpha \ge 1$ and the geometric gain is summable, the $L^2$ norm of the nonlinear term is uniformly bounded by a sublinear function of the enstrophy.

• alpha_ge_one : alpha ≥ 1
• paraproduct_operator_bounded : Prop

  strict cancellation of the Bernstein divergence in subcritical regime

• closure_bound : geometric_gain_summable → alpha ≥ 1 → self.paraproduct_operator_bounded

  The abstract topological closure bound representing Eq. 94

def BonyClosure.vdc_gain (j : ℕ) : ℝ

Concrete Van der Corput dyadic gain.

Equations

• BonyClosure.vdc_gain j = (1 / √2) ^ j

def BonyClosure.dyadic_interaction_bound (interaction : ℕ → ℝ) (C : ℝ) : Prop

Pointwise dyadic interaction majoration.

Equations

• BonyClosure.dyadic_interaction_bound interaction C = ∀ (j : ℕ), interaction j ≤ C * BonyClosure.vdc_gain j

theorem BonyClosure.vdc_gain_nonneg (j : ℕ) : 0 ≤ vdc_gain j

theorem BonyClosure.vdc_ratio_lt_one : 1 / √2 < 1

theorem BonyClosure.vdc_ratio_ne_one : 1 / √2 ≠ 1

theorem BonyClosure.vdc_gain_geometric_sum_formula (N : ℕ) : ∑ j ∈ Finset.range N, vdc_gain j = (1 - (1 / √2) ^ N) / (1 - 1 / √2)

theorem BonyClosure.bony_paraproduct_closure_finite (interaction : ℕ → ℝ) (C : ℝ) (h_bound : dyadic_interaction_bound interaction C) (N : ℕ) : ∑ j ∈ Finset.range N, interaction j ≤ C * ∑ j ∈ Finset.range N, vdc_gain j

Effective finite-shell Bony closure: sum of interactions is bounded by sum of gains.

theorem BonyClosure.bony_paraproduct_closure (interaction : ℕ → ℝ) (C : ℝ) (_hC : 0 ≤ C) (h_bound : dyadic_interaction_bound interaction C) (N : ℕ) : ∑ j ∈ Finset.range N, interaction j ≤ C * ((1 - (1 / √2) ^ N) / (1 - 1 / √2))

theorem BonyClosure.bony_uniform_bound (interaction : ℕ → ℝ) (C : ℝ) (hC : 0 ≤ C) (h_bound : dyadic_interaction_bound interaction C) (N : ℕ) : ∑ j ∈ Finset.range N, interaction j ≤ C / (1 - 1 / √2)