Patching

Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.

Mesoscale patching for the lower coarse-grained ellipticity

The unconditional lambda sensitivity estimate applies the conditional per-cube estimate only on triadic cubes of a mesoscopic scale 3^{-h} and on their descendants, and then patches the resulting bounds back to the root cube. On the coarse depths 0, ..., h-1, where the conditional estimate is unavailable, the source uses subadditivity together with e.bound.one.cube.by.lambdas.

This module proves the exact Lean form of that patching step. The multiscale aggregate lambda_{t,q}^{-1}(Q; .) is a normalized weighted aggregate over all depths n >= 0 of the descendant maxima M_n(A) = maxDescendantSigmaStarInvMatrixNormAtScale Q (Q.scale - n) A,

and the two structural facts are:

• M_h(A) <= 3^{2 t h} lambda_{t,q}^{-1}(Q; A), which is exactly e.bound.one.cube.by.lambdas, obtained by composing CoarseGraining's maxDescendant_sigmaStarInv_le_maxDescendant_lambdaSq_inv with maxDescendant_lambdaSq_inv_le.

The exact geometric mass sum_{n<h} w_n = 1 - 3^{-t q h} of the coarse depths then makes the coarse block contribute 3^{t q h} - 1 and the mesoscopic block contribute 1, so the total factor is exactly 3^{2 t h} with no further loss. Combined with three_rpow_two_mul_mesoscaleDepth_le this is what produces the literal constant 6 = 2 * 3 of lambda_sensitivity_unconditional; a lossier patching would produce a larger constant.

It is a consumption point, not a proof step of these lemmas, and it must be discharged at every application. Every declaration in this module is an internal helper for the Section 2.4 sensitivity providers.

The exact geometric mass of the coarse depths

theorem Algsuperdiff.Section24.Sensitivity.Provider.Mesoscale.sum_geometricWeight_range (t q : ℝ) (htq : 0 < t * q) (h : ℕ) : ∑ n ∈ Finset.range h, HCPolySupport.Book.Ch02.geometricWeight t q n = 1 - Real.rpow 3 (-(t * q) * ↑h)

The exact geometric mass of the coarse depths n = 0, ..., h-1: sum_{n < h} c_{t,q} 3^{-t q n} = 1 - 3^{-t q h}.

e.bound.one.cube.by.lambdas at the mesoscopic depth

theorem Algsuperdiff.Section24.Sensitivity.Provider.Mesoscale.maxDescendantSigmaStarInv_le_weight_mul_lambdaSq_inv {d : ℕ} [NeZero d] (Q : HCPolySupport.TriadicCube d) (A : HCPolySupport.Book.Ch02.TriadicCoeffFamily d) {k : ℤ} {t : ℝ} {q : HCPolySupport.Book.Ch02.MultiscaleExponent} (hk : k ≤ Q.scale) (ht : 0 < t) (hq : q.IsAdmissible) : HCPolySupport.Book.Ch02.maxDescendantSigmaStarInvMatrixNormAtScale Q k A ≤ HCPolySupport.Book.Ch02.multiscaleDescendantWeight Q k t * (HCPolySupport.Book.Ch02.lambdaSq Q t q A)⁻¹

The descendant maximum of the one-cube observable |sigma_*^{-1}| at scale k is bounded by the scale weight times the root aggregate. This is e.bound.one.cube.by.lambdas.

theorem Algsuperdiff.Section24.Sensitivity.Provider.Mesoscale.maxDescendantSigmaStarInv_mesoscale_le {d : ℕ} [NeZero d] (Q : HCPolySupport.TriadicCube d) (A : HCPolySupport.Book.Ch02.TriadicCoeffFamily d) (h : ℕ) {t : ℝ} {q : HCPolySupport.Book.Ch02.MultiscaleExponent} (ht : 0 < t) (hq : q.IsAdmissible) : HCPolySupport.Book.Ch02.maxDescendantSigmaStarInvMatrixNormAtScale Q (Q.scale - ↑h) A ≤ Real.rpow 3 (2 * t * ↑h) * (HCPolySupport.Book.Ch02.lambdaSq Q t q A)⁻¹

The same bound at the mesoscopic depth h, with the scale weight computed as 3^{2 t h}.

Monotonicity of the descendant maxima in the depth

theorem Algsuperdiff.Section24.Sensitivity.Provider.Mesoscale.maxDescendantSigmaStarInv_depth_le {d : ℕ} [NeZero d] (Q : HCPolySupport.TriadicCube d) (A : HCPolySupport.Book.Ch02.TriadicCoeffFamily d) {n h : ℕ} (hnh : n ≤ h) : HCPolySupport.Book.Ch02.maxDescendantSigmaStarInvMatrixNormAtScale Q (Q.scale - ↑n) A ≤ HCPolySupport.Book.Ch02.maxDescendantSigmaStarInvMatrixNormAtScale Q (Q.scale - ↑h) A

The descendant maxima are nondecreasing in the depth: the coarse depths n <= h are dominated by the mesoscopic depth h.

The gauge-free series splitting

The patching estimate

theorem Algsuperdiff.Section24.Sensitivity.Provider.Mesoscale.lambdaSqFinite_inv_le_of_deep_descendant_ratio {d : ℕ} [NeZero d] (Q : HCPolySupport.TriadicCube d) (A₀ A₁ : HCPolySupport.Book.Ch02.TriadicCoeffFamily d) {ρ t q : ℝ} (h : ℕ) (hρ : 0 ≤ ρ) (ht : 0 < t) (hq : 1 ≤ q) (hdeep : ∀ k ≤ Q.scale - ↑h, ∀ R ∈ HCPolySupport.descendantsAtScale Q k, HCPolySupport.Book.Ch02.coarseSigmaStarInvMatrixNorm R A₁ ≤ ρ * HCPolySupport.Book.Ch02.coarseSigmaStarInvMatrixNorm R A₀) : (HCPolySupport.Book.Ch02.lambdaSq Q t (HCPolySupport.Book.Ch02.MultiscaleExponent.finite q) A₁)⁻¹ ≤ ρ * Real.rpow 3 (2 * t * ↑h) * (HCPolySupport.Book.Ch02.lambdaSq Q t (HCPolySupport.Book.Ch02.MultiscaleExponent.finite q) A₀)⁻¹

Mesoscale patching, finite exponent. If the per-cube ratio estimate holds on every triadic descendant of Q at scales at most Q.scale - h, then the root aggregate lambda_{t,q}^{-1} obeys the same ratio bound up to the single scale factor 3^{2 t h}.

theorem Algsuperdiff.Section24.Sensitivity.Provider.Mesoscale.lambdaSqInfinity_inv_le_of_deep_descendant_ratio {d : ℕ} [NeZero d] (Q : HCPolySupport.TriadicCube d) (A₀ A₁ : HCPolySupport.Book.Ch02.TriadicCoeffFamily d) {ρ t : ℝ} (h : ℕ) (hρ : 0 ≤ ρ) (ht : 0 < t) (hdeep : ∀ k ≤ Q.scale - ↑h, ∀ R ∈ HCPolySupport.descendantsAtScale Q k, HCPolySupport.Book.Ch02.coarseSigmaStarInvMatrixNorm R A₁ ≤ ρ * HCPolySupport.Book.Ch02.coarseSigmaStarInvMatrixNorm R A₀) : (HCPolySupport.Book.Ch02.lambdaSq Q t HCPolySupport.Book.Ch02.MultiscaleExponent.infinity A₁)⁻¹ ≤ ρ * Real.rpow 3 (2 * t * ↑h) * (HCPolySupport.Book.Ch02.lambdaSq Q t HCPolySupport.Book.Ch02.MultiscaleExponent.infinity A₀)⁻¹

Mesoscale patching, endpoint exponent q = infinity.

theorem Algsuperdiff.Section24.Sensitivity.Provider.Mesoscale.lambdaSq_inv_le_of_deep_descendant_ratio {d : ℕ} [NeZero d] (Q : HCPolySupport.TriadicCube d) (A₀ A₁ : HCPolySupport.Book.Ch02.TriadicCoeffFamily d) {ρ t : ℝ} {q : HCPolySupport.Book.Ch02.MultiscaleExponent} (h : ℕ) (hρ : 0 ≤ ρ) (ht : 0 < t) (hq : q.IsAdmissible) (hdeep : ∀ k ≤ Q.scale - ↑h, ∀ R ∈ HCPolySupport.descendantsAtScale Q k, HCPolySupport.Book.Ch02.coarseSigmaStarInvMatrixNorm R A₁ ≤ ρ * HCPolySupport.Book.Ch02.coarseSigmaStarInvMatrixNorm R A₀) : (HCPolySupport.Book.Ch02.lambdaSq Q t q A₁)⁻¹ ≤ ρ * Real.rpow 3 (2 * t * ↑h) * (HCPolySupport.Book.Ch02.lambdaSq Q t q A₀)⁻¹

Mesoscale patching. The per-cube ratio estimate on all triadic descendants of Q at scales at most Q.scale - h upgrades to a bound on the root aggregate lambda_{t,q}^{-1} with the single extra factor 3^{2 t h}, for every t > 0 and every admissible q, including the endpoint q = infinity.