The arithmetic core of the scale iteration

This file records the real arithmetic used after the analytic decay estimate in paper/ckn.tex, equations eq:theta-decay-2 and eq:kappa-props. The analytic estimate itself is supplied as a hypothesis to the iteration theorem. The radius interpolation theorem likewise takes the finiteness hypotheses required by the radius monotonicity API.

The numerical convention

noncomputable def CKN.iterationEpsilon : ℝ

The fixed exponent ε = 2/5 in conv:kappa.

Equations

• CKN.iterationEpsilon = 2 / 5

noncomputable def CKN.iterationKappa (C₂₇ : ℝ) : ℝ

The fixed contraction factor in conv:kappa.

Equations

• CKN.iterationKappa C₂₇ = min (1 / 2) ((8 * C₂₇) ^ (-1 / (2 / 3 - CKN.iterationEpsilon)))

noncomputable def CKN.iterationEta (C₂₇ : ℝ) : ℝ

The initial smallness threshold η in conv:kappa.

Equations

• CKN.iterationEta C₂₇ = min 1 ((CKN.iterationKappa C₂₇ ^ (5 + CKN.iterationEpsilon) / (16 * C₂₇)) ^ 2)

noncomputable def CKN.iterationEpsilonStar (C₂₇ : ℝ) : ℝ

The auxiliary threshold ε_* in conv:kappa.

Equations

• CKN.iterationEpsilonStar C₂₇ = min 1 ((CKN.iterationKappa C₂₇ ^ (5 + CKN.iterationEpsilon) / (32 * C₂₇)) ^ 2)

noncomputable def CKN.iterationC₂₉ (C₂₇ C₂₈ : ℝ) : ℝ

The force coefficient C₂₉ in eq:C29.

Equations

• CKN.iterationC₂₉ C₂₇ C₂₈ = 2 * C₂₈ ^ 2 * CKN.iterationKappa C₂₇ ^ (-1 - 2 * CKN.iterationEpsilon) + C₂₈ * CKN.iterationKappa C₂₇ ^ (-3 - CKN.iterationEpsilon)

noncomputable def CKN.iterationLambda₀ (C₂₇ C₂₈ : ℝ) : ℝ

The force smallness threshold Λ₀ in eq:C29.

Equations

• CKN.iterationLambda₀ C₂₇ C₂₈ = CKN.iterationEta C₂₇ / (2 * CKN.iterationC₂₉ C₂₇ C₂₈)

theorem CKN.iterationEpsilon_eq : iterationEpsilon = 2 / 5

The convention exponent is exactly the paper's 2/5.

theorem CKN.iterationKappa_pos {C₂₇ : ℝ} (hC₂₇ : 0 < C₂₇) : 0 < iterationKappa C₂₇

The contraction factor is positive when the absolute decay constant is positive.

theorem CKN.iterationKappa_le_half (C₂₇ : ℝ) : iterationKappa C₂₇ ≤ 1 / 2

The paper's convention gives κ ≤ 1/2.

theorem CKN.iterationKappa_prop₁ {C₂₇ : ℝ} (hC₂₇ : 0 < C₂₇) : C₂₇ * iterationKappa C₂₇ ^ (2 / 3 - iterationEpsilon) ≤ 1 / 8

The first numerical inequality in eq:kappa-props.

theorem CKN.iterationEta_pos {C₂₇ : ℝ} (hC₂₇ : 0 < C₂₇) : 0 < iterationEta C₂₇

The threshold η is positive.

theorem CKN.iterationEta_le_one (C₂₇ : ℝ) : iterationEta C₂₇ ≤ 1

The threshold η is at most one.

theorem CKN.iterationEpsilonStar_pos {C₂₇ : ℝ} (hC₂₇ : 0 < C₂₇) : 0 < iterationEpsilonStar C₂₇

The auxiliary threshold ε_* is positive.

theorem CKN.iterationEpsilonStar_le_one (C₂₇ : ℝ) : iterationEpsilonStar C₂₇ ≤ 1

The auxiliary threshold ε_* is at most one.

theorem CKN.iterationC₂₉_pos {C₂₇ C₂₈ : ℝ} (hC₂₇ : 0 < C₂₇) (hC₂₈ : 0 < C₂₈) : 0 < iterationC₂₉ C₂₇ C₂₈

The coefficient C₂₉ is positive when both decay constants are positive.

theorem CKN.iterationLambda₀_pos {C₂₇ C₂₈ : ℝ} (hC₂₇ : 0 < C₂₇) (hC₂₈ : 0 < C₂₈) : 0 < iterationLambda₀ C₂₇ C₂₈

The force threshold is positive under the convention hypotheses.

theorem CKN.iterationC₂₉_mul_Lambda₀ {C₂₇ C₂₈ : ℝ} (hC₂₇ : 0 < C₂₇) (hC₂₈ : 0 < C₂₈) : iterationC₂₉ C₂₇ C₂₈ * iterationLambda₀ C₂₇ C₂₈ = iterationEta C₂₇ / 2

The final convention identity is C₂₉ Λ₀ = η/2.

theorem CKN.iterationKappa_prop₂ {C₂₇ : ℝ} (hC₂₇ : 0 < C₂₇) : 2 * C₂₇ * iterationKappa C₂₇ ^ (-5 - iterationEpsilon) * iterationEta C₂₇ ^ (1 / 2) ≤ 1 / 8

The second numerical inequality in eq:kappa-props.

theorem CKN.iterationKappa_prop₃ {C₂₇ : ℝ} (hC₂₇ : 0 < C₂₇) : 2 * C₂₇ * iterationKappa C₂₇ ^ (-5 - iterationEpsilon) * (iterationEpsilonStar C₂₇ ^ (1 / 2) + iterationEpsilonStar C₂₇) ≤ 1 / 8

The third numerical inequality in eq:kappa-props.

The normalized induction

theorem CKN.iteration_normalized_bound {T L Θ : ℕ → ℝ} {κ ε η C₂₇ C₂₈ C₂₉ Λ₀ : ℝ} (hκ : 0 < κ) (hη : 0 < η) (hC₂₇ : 0 ≤ C₂₇) (hC₂₈ : 0 ≤ C₂₈) (hA : C₂₇ * κ ^ (2 / 3 - ε) ≤ 1 / 8) (hB : 2 * C₂₇ * κ ^ (-5 - ε) * η ^ (1 / 2) ≤ 1 / 8) (hC₂₉ : C₂₉ = 2 * C₂₈ ^ 2 * κ ^ (-1 - 2 * ε) + C₂₈ * κ ^ (-3 - ε)) (hC₂₉_nonneg : 0 ≤ C₂₉) (hΛ : C₂₉ * Λ₀ ≤ η / 2) (hT₀ : T 0 ≤ η) (hT_nonneg : ∀ (n : ℕ), 0 ≤ T n) (hΘ_nonneg : ∀ (n : ℕ), 0 ≤ Θ n) (hΘ_le : ∀ (n : ℕ), Θ n ≤ η) (hL_nonneg : ∀ (n : ℕ), 0 ≤ L n) (hL_le : ∀ (n : ℕ), L n ≤ Λ₀) (hrec : ∀ (n : ℕ), T (n + 1) ≤ C₂₇ * κ ^ (2 / 3 - ε) * T n + 2 * C₂₇ * κ ^ (-5 - ε) * Θ n ^ (1 / 2) * T n + C₂₈ * κ ^ (-1 / 2 - ε) * T n ^ (1 / 2) * L n ^ (1 / 2) + C₂₈ * κ ^ (-3 - ε) * L n) (n : ℕ) : T n ≤ η

The normalized four-term induction from prop:iteration.

Here T and L are the paper's normalized sequences, while Θ is the unscaled quantity appearing in the quadratic term of eq:theta-decay-2. The hypotheses are exactly the numerical smallness inequalities used in the paper's induction.

theorem CKN.theta_iteration_bound {θ T : ℕ → ℝ} {κ ε η : ℝ} (hκ : 0 < κ) (hscale : ∀ (n : ℕ), θ n = T n * κ ^ (↑n * ε)) (hT : ∀ (n : ℕ), T n ≤ η) (n : ℕ) : θ n ≤ η * κ ^ (↑n * ε)

Reconstructs the paper's bound θ_n ≤ η κ^(nε) from the normalized iteration bound.

theorem CKN.force_normalized_bound {lam : ℕ → ℝ} {κ ε σ lamZero LamZero : ℝ} (hκ : 0 < κ) (hκle : κ ≤ 1) (hεσ : ε ≤ σ) (hlamZero : 0 ≤ lamZero) (hlamZeroLam : lamZero ≤ LamZero) (hlam : ∀ (n : ℕ), 0 ≤ lam n ∧ lam n ≤ κ ^ (↑n * σ) * lamZero) (n : ℕ) : lam n / κ ^ (↑n * ε) ≤ LamZero

The paper's force decay λ_n ≤ κ^(nσ) λ₀ implies the normalized bound L_n = λ_n κ^(-nε) ≤ Λ₀ whenever ε ≤ σ and λ₀ ≤ Λ₀.

Radius interpolation

theorem CKN.theta_mono_radius_of_finite (κ : ℝ) (u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3) (p : Foundation.Parabolic.ParabolicPoint → ℝ) (z : Foundation.Parabolic.ParabolicPoint) {r ρ : ℝ} (hκ : 0 < κ) (hκle : κ ≤ 1) (hr : 0 < r) (hrr : r ≤ ρ) (hsmall : κ * ρ ≤ r) (hα : (Foundation.Parabolic.Integration.timeSliceEnergyEssSup z.1 z.2 ρ fun (w : Foundation.Parabolic.ParabolicPoint) => Foundation.Parabolic.vec3EuclideanNorm (u w)) ≠ ⊤) (hβ : ∫⁻ (w : Foundation.Parabolic.ParabolicPoint) in Foundation.Parabolic.parabolicCylinder z.1 z.2 ρ, ENNReal.ofReal (spatialGradientSq u Du w) ≠ ⊤) (hδ : ∫⁻ (w : Foundation.Parabolic.ParabolicPoint) in Foundation.Parabolic.parabolicCylinder z.1 z.2 ρ, ENNReal.ofReal |p w| ^ (3 / 2) ≠ ⊤) : theta κ u Du p z r ≤ κ ^ (-4 / 3) * theta κ u Du p z ρ

The combined quantity has the radius comparison used in the intermediate scale step of prop:iteration. The three finiteness hypotheses are the side conditions required by the established radius monotonicity theorems.

theorem CKN.theta_intermediate_scale_bound (κ ε η r₅ r : ℝ) (u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3) (p : Foundation.Parabolic.ParabolicPoint → ℝ) (z : Foundation.Parabolic.ParabolicPoint) {n : ℕ} (hκ : 0 < κ) (hκle : κ ≤ 1) (hε : 0 < ε) (hη : 0 ≤ η) (hr₅ : 0 < r₅) (hr : 0 < r) (hinterval₁ : κ ^ (n + 1) * r₅ < r) (hinterval₂ : r ≤ κ ^ n * r₅) (hdisc : theta κ u Du p z (κ ^ n * r₅) ≤ η * κ ^ (↑n * ε)) (hα : (Foundation.Parabolic.Integration.timeSliceEnergyEssSup z.1 z.2 (κ ^ n * r₅) fun (w : Foundation.Parabolic.ParabolicPoint) => Foundation.Parabolic.vec3EuclideanNorm (u w)) ≠ ⊤) (hβ : ∫⁻ (w : Foundation.Parabolic.ParabolicPoint) in Foundation.Parabolic.parabolicCylinder z.1 z.2 (κ ^ n * r₅), ENNReal.ofReal (spatialGradientSq u Du w) ≠ ⊤) (hδ : ∫⁻ (w : Foundation.Parabolic.ParabolicPoint) in Foundation.Parabolic.parabolicCylinder z.1 z.2 (κ ^ n * r₅), ENNReal.ofReal |p w| ^ (3 / 2) ≠ ⊤) : max (max (alpha u z r) (beta u Du z r)) (delta p z r ^ 2) ≤ theta κ u Du p z r ∧ theta κ u Du p z r ≤ κ ^ (-4 / 3 - ε) * η * r₅ ^ (-ε) * r ^ ε

The intermediate-scale estimate of prop:iteration, for a supplied index n satisfying κ^(n+1) r₅ < r ≤ κ^n r₅.