StarredFluctuationIntegrable

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

Integrability of the starred fluctuation observable at the coefficient cutoff law

The Step-3 corridor observable

starredFluctuationOperatorNormSq 𝐁(σ_L) 𝐂 (cubeSet □_n) a = ‖𝐁^{1/2}(𝐀_*^{-1}(□_n;a) - 𝐑𝐂𝐑)𝐁^{1/2}‖²

(starredFluctuationOperatorNormSq in VarianceBridge.lean) is integrable at the genuine coefficient cutoff law Cutoff.coefficientCutoffLaw M L, for every deterministic centering 𝐂 and every cube. That is the item recorded as M7; on delivery it discharges the Integrable binder carried by the two proved publics coefficientCutoffLaw_sq_sigmaBar_mul_starInverseVarianceAtScale_add_le and exists_coefficientCutoff_finiteCorridor_starInverseVariance_withS_bound of VarianceClosure.lean, whose unconditional restatements are the last two declarations of this module.

This module makes no source-node status claim; every declaration below is a local Provider helper.

The two halves

(i) The measurable half. starredFluctuationOperatorNormSq B · is a continuous function of the full coarse block matrix toFullBlockMat (coarseBlockMatrix U a.toFun): reflection is the entry permutation Matrix.submatrix Sum.swap Sum.swap (toFullBlockMat_blockReflect), the centering is a constant, and the two-sided CFC.sqrt B conjugation and the squared Euclidean operator norm are continuous. Composing with Ch04.RestrictionLawCarrier.aemeasurable_coarseFullBlockMatrix_cubeSet gives a.e. measurability at any restriction law, in particular at Cutoff.coefficientCutoffLaw M L, a carrier by Cutoff.coefficientCutoffLaw_lawCarrier.

(ii) The gauge instance and the domination. cutoffComparatorNormalizer M L is definitionally Ch02.constantFullBlockMatrix (Observable.isotropicComparatorMatrix (Annealed.sigmaBar M L)) (cutoffComparatorNormalizer in VarianceCarrierSeam.lean), whose CFC.sqrt is the block diagonal diag(√σ 𝟙, (√σ)^{-1} 𝟙).

σ |Δ_lowerRight| + |Δ_lowerLeft| + |Δ_upperRight| + σ^{-1} |Δ_upperLeft|,

the asymmetric weighting of the proved carrier bridges. Each block is then bounded unconditionally, at a = Cutoff.coefficientCutoff M.nu L ω:

• |𝐀_lowerRight| ≤ 4dν^{-1} -- the deterministic descendant envelope, matrixOperatorNorm_coarseBlockMatrix_lowerRight_le_of_mem_descendantsAtScale (VarianceClosure.lean) at depth 0;
• |𝐀_upperLeft| ≤ 4dν^{-1}E(ω)² with E := Cutoff.coefficientCutoffCubeEllipticityUpper -- the unconditional envelope Cutoff.maxDescendantBMatrixNormCoeffFieldAtScale_le_cutoffEnvelope (the ambient form of Cutoff.maxDescendantBMatrixNormAtScale_le_cutoffEnvelope), read on the coarseBlockMatrix carrier through the public Chapter 5 sup identity;
• |𝐀_lowerLeft|, |𝐀_upperRight| ≤ 4dν^{-1}E(ω) -- the sharp positive semidefinite off-diagonal bound (matrixOperatorNorm_upperRight_le_sqrt_of_isSymmetricBlockMat_of_blockPosDef / matrixOperatorNorm_lowerLeft_le_sqrt_of_isSymmetricBlockMat_of_blockPosDef in VarianceClosure.lean) with the symmetry and positivity discharges of coarseBlockMatrix_cubeSet_symm_of_aelocallyUniformlyEllipticField and coarseBlockMatrix_cubeSet_blockPosDef_of_aelocallyUniformlyEllipticField;
• the four centering blocks are constants in ω -- the annealed block matrix is deterministic -- so their operator norms enter only as fixed additive constants. No σ sandwich is used; the proved SigmaBarAnchor premises are therefore not bound here.

The result is a pointwise bound by (a₀ + a₁E + a₂E²)², a degree-four polynomial in E with constant coefficients, and every power of E is integrable at the sample law (Cutoff.integrable_coefficientCutoffCubeEllipticityUpper_pow, Cutoff.integrable_coefficientCutoffCubeEllipticityUpper_pow, via Cutoff.integrable_cutoffLocalControl_pow and Cutoff.coefficientCutoffCubeEllipticityUpper_le_majorant). The transfer between the sample carrier and the RegCoeffField carrier is Cutoff.coefficientCutoffLaw_eq_map (Cutoff/Law.lean) with integrable_map_measure, the pattern proved in Cutoff.integrable_LambdaSqCoeffField_pow_cutoffLaw.

Elementary norm facts

The measurable half

theorem Algsuperdiff.Section3.Provider.Homogenization.starredFluctuationMatrix_eq_conj_submatrix {d : ℕ} (B : HCPolySupport.FullBlockMat d) (C : HCPolySupport.BlockMat d) (U : Set (HCPolySupport.Vec d)) (a : HCPolySupport.RegCoeffField d) : starredFluctuationMatrix B C U a = CFC.sqrt B * (Matrix.submatrix (HCPolySupport.toFullBlockMat (HCPolySupport.coarseBlockMatrix U a.toFun)) Sum.swap Sum.swap - HCPolySupport.toFullBlockMat (HCPolySupport.blockReflect C)) * CFC.sqrt B

The starred fluctuation matrix, written as a two-sided conjugation of an affine function of the full coarse block matrix. Reflection is the entry permutation Matrix.submatrix Sum.swap Sum.swap.

theorem Algsuperdiff.Section3.Provider.Homogenization.aemeasurable_starredFluctuationOperatorNormSq {d : ℕ} {P : HCPolySupport.Book.Ch04.RestrictionCoeffLaw d} (hP : HCPolySupport.Book.Ch04.RestrictionLawCarrier P) (B : HCPolySupport.FullBlockMat d) (C : HCPolySupport.BlockMat d) (Q : HCPolySupport.TriadicCube d) : AEMeasurable (fun (a : HCPolySupport.RegCoeffField d) => starredFluctuationOperatorNormSq B C (HCPolySupport.cubeSet Q) a) P

The measurable half of M7. At every restriction law carrier the starred fluctuation observable is a.e. measurable, for every normalizer, every deterministic centering and every cube.

theorem Algsuperdiff.Section3.Provider.Homogenization.aemeasurable_starredFluctuationOperatorNormSq_coefficientCutoffLaw {d : ℕ} (M : ABKModel d) (L : ℤ) (B : HCPolySupport.FullBlockMat d) (C : HCPolySupport.BlockMat d) (Q : HCPolySupport.TriadicCube d) : AEMeasurable (fun (a : HCPolySupport.RegCoeffField d) => starredFluctuationOperatorNormSq B C (HCPolySupport.cubeSet Q) a) (Cutoff.coefficientCutoffLaw M L)

The measurable half at the genuine coefficient cutoff law.

The gauge instance

theorem Algsuperdiff.Section3.Provider.Homogenization.norm_toEuclideanCLM_starredFluctuationMatrix_cutoffComparatorNormalizer_le {d : ℕ} (M : ABKModel d) (L : ℤ) (C : HCPolySupport.BlockMat d) (U : Set (HCPolySupport.Vec d)) (a : HCPolySupport.RegCoeffField d) : ‖Matrix.toEuclideanCLM (starredFluctuationMatrix (cutoffComparatorNormalizer M L) C U a)‖ ≤ ↑(Annealed.sigmaBar M L) * HCPolySupport.Book.Ch02.matrixOperatorNorm ((HCPolySupport.coarseBlockMatrix U a.toFun).lowerRight - C.lowerRight) + HCPolySupport.Book.Ch02.matrixOperatorNorm ((HCPolySupport.coarseBlockMatrix U a.toFun).lowerLeft - C.lowerLeft) + HCPolySupport.Book.Ch02.matrixOperatorNorm ((HCPolySupport.coarseBlockMatrix U a.toFun).upperRight - C.upperRight) + (↑(Annealed.sigmaBar M L))⁻¹ * HCPolySupport.Book.Ch02.matrixOperatorNorm ((HCPolySupport.coarseBlockMatrix U a.toFun).upperLeft - C.upperLeft)

The gauge instance at the comparator normalizer. Conjugating by 𝐁(σ_L)^{1/2} weights the four block operator norms of the reflected difference by σ_L, 1, 1, σ_L^{-1}; since blockReflect swaps the diagonal blocks, the weights land on lowerRight, lowerLeft, upperRight, upperLeft in that order -- the asymmetric weighting of the proved carrier bridges (sq_mul_sq_matrixOperatorNorm_lowerRight_sub_le_starredFluctuationOperatorNormSq and sq_matrixOperatorNorm_lowerLeft_sub_le_starredFluctuationOperatorNormSq in VarianceClosure.lean).

The unconditional upper-left descendant envelope

theorem Algsuperdiff.Section3.Provider.Homogenization.matrixOperatorNorm_coarseBlockMatrix_upperLeft_le_cutoffEnvelope {d : ℕ} [NeZero d] (M : ABKModel d) (L : ℤ) (omega : Cutoff.CutoffSample d) (Q : HCPolySupport.TriadicCube d) (j : ℕ) {R : HCPolySupport.TriadicCube d} (hR : R ∈ HCPolySupport.descendantsAtScale Q (Q.scale - ↑j)) : HCPolySupport.Book.Ch02.matrixOperatorNorm (HCPolySupport.coarseBlockMatrix (HCPolySupport.cubeSet R) (Cutoff.coefficientCutoff M.nu L omega).toFun).upperLeft ≤ 4 * ↑d * M.nu⁻¹ * Cutoff.coefficientCutoffCubeEllipticityUpper M L omega Q ^ 2

The unconditional upper-left envelope. The Euclidean operator norm of the upper-left coarse block -- the manuscript's b -- of every descendant of Q at depth j is below 4dν^{-1}E(ω)², with E := Cutoff.coefficientCutoffCubeEllipticityUpper the realised upper ellipticity constant of the root cube. Unlike the good-event, geometrically weighted upper-left bound of VarianceClosure.lean this bound is depth-uniform and carries no event; the price is the random envelope in place of 2σ_L.

The samplewise polynomial domination

theorem Algsuperdiff.Section3.Provider.Homogenization.norm_toEuclideanCLM_starredFluctuationMatrix_coefficientCutoff_le {d : ℕ} [NeZero d] (M : ABKModel d) (L : ℤ) (C : HCPolySupport.BlockMat d) (Q : HCPolySupport.TriadicCube d) (omega : Cutoff.CutoffSample d) : ‖Matrix.toEuclideanCLM (starredFluctuationMatrix (cutoffComparatorNormalizer M L) C (HCPolySupport.cubeSet Q) (Cutoff.coefficientCutoff M.nu L omega))‖ ≤ ↑(Annealed.sigmaBar M L) * (4 * ↑d * M.nu⁻¹ + HCPolySupport.Book.Ch02.matrixOperatorNorm C.lowerRight) + HCPolySupport.Book.Ch02.matrixOperatorNorm C.lowerLeft + HCPolySupport.Book.Ch02.matrixOperatorNorm C.upperRight + (↑(Annealed.sigmaBar M L))⁻¹ * HCPolySupport.Book.Ch02.matrixOperatorNorm C.upperLeft + 2 * (4 * ↑d * M.nu⁻¹) * Cutoff.coefficientCutoffCubeEllipticityUpper M L omega Q ^ 1 + (↑(Annealed.sigmaBar M L))⁻¹ * (4 * ↑d * M.nu⁻¹) * Cutoff.coefficientCutoffCubeEllipticityUpper M L omega Q ^ 2

The samplewise envelope. On every cutoff sample the starred fluctuation norm at the comparator normalizer, on the origin cube of the centering scale, is below an explicit quadratic polynomial in the realised upper ellipticity constant of that cube, with coefficients built from σ_L, 4dν^{-1} and the four block norms of the deterministic centering.

Integrability at the coefficient cutoff law

theorem Algsuperdiff.Section3.Provider.Homogenization.integrable_starredFluctuationOperatorNormSq_coefficientCutoffLaw {d : ℕ} [NeZero d] (M : ABKModel d) (L : ℤ) (C : HCPolySupport.BlockMat d) (Q : HCPolySupport.TriadicCube d) : MeasureTheory.Integrable (fun (a : HCPolySupport.RegCoeffField d) => starredFluctuationOperatorNormSq (cutoffComparatorNormalizer M L) C (HCPolySupport.cubeSet Q) a) (Cutoff.coefficientCutoffLaw M L)

M7. The Step-3 corridor observable is integrable at the genuine coefficient cutoff law, for every deterministic centering and every cube.

The unconditional restatements

theorem Algsuperdiff.Section3.Provider.Homogenization.exists_coefficientCutoff_finiteCorridor_starInverseVariance_withS_bound' {d : ℕ} [NeZero d] : ∃ (Chom : ℝ) (Cvar : ℝ), 64 ≤ Chom ∧ 2 * (↑(Cutoff.cutoffRelativeNormalizationShift d) + 1) ≤ Chom ∧ 1 ≤ Cvar ∧ ∀ (M : ABKModel d) (m : ℤ) (E : { E : ℝ // 1 ≤ E }), (∀ k ≤ m - 1, ∀ (s : ℝ) (hsWindow : s ∈ Set.Icc (8 * M.gamma) 1), Probability.IsTwoTermBigOWith (↑(Cutoff.cutoffSampleLaw M)) (HCPolySupport.IndependentSums.gammaSigma 2) (HCPolySupport.IndependentSums.gammaSigma (1 / 2)) (Observable.cutoffHomogenizationError M k ⟨s, ⋯⟩) (↑E * s⁻¹ * √M.gamma) (s⁻¹ ^ 2 * Real.exp (-((↑E)⁻¹ ^ 3 * M.gamma⁻¹)))) → ∀ epsilon ∈ Set.Ioc 0 (1 / 2), M.gamma ≤ Chom⁻¹ * (↑E)⁻¹ ^ 2 * epsilon → ∀ (L : ℤ), ↑L ≤ ↑m - Chom * |Real.log epsilon| → ∀ n ∈ Set.Icc L m, ↑(Annealed.sigmaBar M L) ^ 2 * starInverseVarianceAtScale M L n + starInverseKappaVarianceAtScale M L n ≤ 2 * Cvar * (↑E ^ 2 * M.gamma + Real.exp (-(2 * (↑E)⁻¹ ^ 3 * M.gamma⁻¹))) * (↑E ^ 2 * M.gamma + Real.exp (-(2 * (↑E)⁻¹ ^ 3 * M.gamma⁻¹)) + Real.rpow 3 (-↑d * ↑(n - L).toNat))

(e.var.bound.astar.withS) at the genuine cutoff law, unconditionally. This is exists_coefficientCutoff_finiteCorridor_starInverseVariance_withS_bound (VarianceClosure.lean) with its Integrable binder discharged; every other binder and the conclusion are byte-identical. The caveats recorded there are unchanged: the amplitude is the lane's two-term δ, strictly larger than the printed δ₁, so this partially supports and does not realize the printed display.