InitialJLBoundIntegrability

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

(e.initial.JL.bound), Parts A and B: envelopes and global integrability

ABK26 (the display e.initial.JL.bound) and its proof.

Content part carried by this file

This module is the first of the two files into which the Step-1 assembly of the corrected combine is split. It carries Parts A and B: the unconditional descendant envelope of the sigma_*^{-1}kappa channel, the pointwise envelopes of the two deterministic blocks of the good-event display, their global integrability at the genuine cutoff sample law, and the resulting discharge of the two IntegrableOn binders of the proved CombineExpectation endpoints. This is item (4) of the depgraph record and item (i).

Part C --- the corridor summation, the anchor wiring, the absorption and the assembly into the printed display --- is in Provider/Homogenization/InitialJLBound.lean, which imports this file.

Part A: the unconditional envelope and the two global integrabilities

VarianceClosure.lean produces the sigma_*^{-1}kappa descendant envelope only on the good event, at the cost of a geometric weight, because it routes the upper-left block through the Lambda^2 extraction. The route taken here is the other one: the unconditional chain

• Cutoff.maxDescendantBMatrixNormCoeffFieldAtScale_le_cutoffEnvelope (the ambient form of Cutoff.maxDescendantBMatrixNormAtScale_le_cutoffEnvelope), depth-uniform, no event, no weight, read on the coarseBlockMatrix carrier through the public CoarseGraining Ch05.Section52 sup identity maxDescendantBMatrixNormCoeffFieldAtScale_eq_sup_upperLeft_of_aelocallyUniformlyEllipticField. That reading is not performed here: it is the proved sibling public matrixOperatorNorm_coarseBlockMatrix_upperLeft_le_cutoffEnvelope (Provider/Homogenization/StarredFluctuationIntegrable.lean), which this file imports and consumes;
• the sharp positive semidefinite off-diagonal bound matrixOperatorNorm_lowerLeft_le_sqrt_of_isSymmetricBlockMat_of_blockPosDef (VarianceClosure.lean, public 13), whose hSymm/hPos come from the public CoarseGraining coarseBlockMatrix_cubeSet_symm_of_aelocallyUniformlyEllipticField and coarseBlockMatrix_cubeSet_blockPosDef_of_aelocallyUniformlyEllipticField, exactly as in VarianceClosure.lean;
• the deterministic lower-right envelope matrixOperatorNorm_coarseBlockMatrix_lowerRight_le_of_mem_descendantsAtScale (VarianceClosure.lean, public 9),

which gives, for every descendant R of every cube Q at every depth and for every sample,

|(sigma_*^{-1}kappa)(R;omega)| <= 4 d nu^{-1} E(omega), E := Cutoff.coefficientCutoffCubeEllipticityUpper M L omega Q.

Since every natural power of E is integrable at (Cutoff.cutoffSampleLaw M).toMeasure (Cutoff.integrable_coefficientCutoffCubeEllipticityUpper_pow), the two CombineExpectation block carriers coarseMatrixVariationBlock and coarseScaleSeparationBlock are globally integrable at that measure, with no event and no hypothesis beyond the standing model data. The corridor weight 3^{-(m-n)} is at most 1 on [L,m] and the corridor is finite, so the second block costs only the deterministic factor card (Finset.Icc L m).

Part B: the two IntegrableOn binders

IntegrableOn follows from global Integrable by Integrable.integrableOn.

Declaration census and the Internal namespace

Seven of the module's eighteen exported statements live here; the remaining eleven live in InitialJLBound.lean. Below them are five private helpers and four more in a nested namespace Internal, opened in three places so that the file's declaration order is unchanged. Those four are exactly the helpers that Part C also needs: the split forced their visibility, and Internal is the repository's convention for a helper that is public only because a sibling file consumes it (see the Internal namespaces of Provider/Diffusivity/RecurrenceIntegration/Core.lean, Bootstrap.lean and Descent.lean). They are not part of the module's exported surface.

References

• ABK26, Section 3.5, proof of p.combine.under.S, Step 1.

theorem Algsuperdiff.Section3.Provider.Homogenization.Internal.matrixOperatorNorm_sub_le_add' {d : ℕ} (X Y : HCPolySupport.Mat d) : HCPolySupport.Book.Ch02.matrixOperatorNorm (X - Y) ≤ HCPolySupport.Book.Ch02.matrixOperatorNorm X + HCPolySupport.Book.Ch02.matrixOperatorNorm Y

Two-point triangle inequality for the Chapter 2 Euclidean matrix operator norm.

theorem Algsuperdiff.Section3.Provider.Homogenization.Internal.self_mem_descendantsAtScale {d : ℕ} (Q : HCPolySupport.TriadicCube d) : Q ∈ HCPolySupport.descendantsAtScale Q (Q.scale - ↑0)

Every cube is its own descendant at depth 0.

theorem Algsuperdiff.Section3.Provider.Homogenization.matrixOperatorNorm_coarseBlockMatrix_lowerLeft_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).lowerLeft ≤ 4 * ↑d * M.nu⁻¹ * Cutoff.coefficientCutoffCubeEllipticityUpper M L omega Q

The unconditional descendant envelope of the sigma_*^{-1}kappa block. For every descendant R of every cube Q at every depth j, and for every sample omega,

|(sigma_*^{-1}kappa)(R;omega)| <= 4 d nu⁻¹ E(omega),

with E := Cutoff.coefficientCutoffCubeEllipticityUpper M L omega Q.

The three inputs are the sharp positive semidefinite off-diagonal block bound (matrixOperatorNorm_lowerLeft_le_sqrt_of_isSymmetricBlockMat_of_blockPosDef, VarianceClosure.lean), the unconditional upper-left envelope above, and the deterministic lower-right envelope (matrixOperatorNorm_coarseBlockMatrix_lowerRight_le_of_mem_descendantsAtScale, VarianceClosure.lean). Unlike geometricWeight_mul_matrixOperatorNorm_coarseBlockMatrix_lowerLeft_le (VarianceClosure.lean) this carries no good event and no geometric weight: the price is that the right side is random rather than deterministic. Every natural power of E is integrable at (Cutoff.cutoffSampleLaw M).toMeasure (Cutoff.integrable_coefficientCutoffCubeEllipticityUpper_pow), which is exactly what the integrability lane below needs.

theorem Algsuperdiff.Section3.Provider.Homogenization.Internal.vecNormSq_coarseBlockScaleSeparation_le_cutoffEnvelope {d : ℕ} [NeZero d] (M : ABKModel d) (L : ℤ) (omega : Cutoff.CutoffSample d) (Q : HCPolySupport.TriadicCube d) (p q : HCPolySupport.Vec d) : HCPolySupport.vecNormSq (coarseBlockScaleSeparation Q p q (Cutoff.coefficientCutoff M.nu L omega)) ≤ 4 * (4 * ↑d * M.nu⁻¹) ^ 2 * HCPolySupport.vecNormSq q + 2 * HCPolySupport.vecNormSq p + 4 * (4 * ↑d * M.nu⁻¹) ^ 2 * HCPolySupport.vecNormSq p * Cutoff.coefficientCutoffCubeEllipticityUpper M L omega Q ^ 2

Pointwise envelope of the comparison vector. The squared length of the block comparison vector sigma_*^{-1}(Q)q - (sigma_*^{-1}kappa)(Q)p - p at the genuine cutoff is at most a deterministic affine function of E(Q;omega)^2. The constant 4 (rather than the sharp 3) comes from applying the two-term Euclidean split vecNormSq_sub_le twice; only integrability is used downstream, so no sharpness is lost.

theorem Algsuperdiff.Section3.Provider.Homogenization.Internal.coarseBlockMatrixVariationSq_le_cutoffEnvelope {d : ℕ} [NeZero d] (M : ABKModel d) (L : ℤ) (omega : Cutoff.CutoffSample d) (Q : HCPolySupport.TriadicCube d) (p q : HCPolySupport.Vec d) {j : ℕ} {R : HCPolySupport.TriadicCube d} (hR : R ∈ HCPolySupport.descendantsAtDepth Q j) : coarseBlockMatrixVariationSq Q p q (Cutoff.coefficientCutoff M.nu L omega) R ≤ 2 * (2 * (4 * ↑d * M.nu⁻¹)) ^ 2 * HCPolySupport.vecNormSq q + 2 * (2 * (4 * ↑d * M.nu⁻¹)) ^ 2 * HCPolySupport.vecNormSq p * Cutoff.coefficientCutoffCubeEllipticityUpper M L omega Q ^ 2

Pointwise envelope of the coarse-matrix variation. For a descendant R of Q at any depth, the squared coarse-matrix variation between Q and R at the genuine cutoff is at most a deterministic affine function of E(Q;omega)^2. Both channels use the two descendant envelopes; the sigma_*^{-1} channel is deterministic, the sigma_*^{-1}kappa channel carries the random E.

theorem Algsuperdiff.Section3.Provider.Homogenization.coarseScaleSeparationBlock_nonneg {d : ℕ} (M : ABKModel d) (m L : ℤ) (e : HCPolySupport.Vec d) (omega : Cutoff.CutoffSample d) : 0 ≤ coarseScaleSeparationBlock M m L e omega

The third good-event block is a squared length, hence nonnegative.

theorem Algsuperdiff.Section3.Provider.Homogenization.coarseMatrixVariationBlock_nonneg {d : ℕ} (M : ABKModel d) (m L : ℤ) (e : HCPolySupport.Vec d) (omega : Cutoff.CutoffSample d) : 0 ≤ coarseMatrixVariationBlock M m L e omega

The second good-event block is a nonnegatively weighted corridor sum of descendant averages of squared lengths, hence nonnegative.

theorem Algsuperdiff.Section3.Provider.Homogenization.integrable_coarseScaleSeparationBlock {d : ℕ} [NeZero d] (M : ABKModel d) (m L : ℤ) (e : HCPolySupport.Vec d) : MeasureTheory.Integrable (coarseScaleSeparationBlock M m L e) ↑(Cutoff.cutoffSampleLaw M)

Global integrability of the third good-event block at the genuine cutoff sample law, with no event and no hypothesis beyond the standing model data. The dominating function is A + B E^2; Cutoff.integrable_coefficientCutoffCubeEllipticityUpper_pow supplies the integrability of E^2.

theorem Algsuperdiff.Section3.Provider.Homogenization.integrable_coarseMatrixVariationBlock {d : ℕ} [NeZero d] (M : ABKModel d) (m L : ℤ) (e : HCPolySupport.Vec d) : MeasureTheory.Integrable (coarseMatrixVariationBlock M m L e) ↑(Cutoff.cutoffSampleLaw M)

Global integrability of the second good-event block at the genuine cutoff sample law. The corridor weight 3^{-(m-n)} is at most 1 and the corridor is finite, so the envelope of the single descendant average is multiplied by the deterministic factor card (Finset.Icc L m).

theorem Algsuperdiff.Section3.Provider.Homogenization.integrableOn_coarseScaleSeparationBlock_compl_observationScaleBadEvent {d : ℕ} [NeZero d] (M : ABKModel d) (m L : ℤ) (e : HCPolySupport.Vec d) : MeasureTheory.IntegrableOn (coarseScaleSeparationBlock M m L e) (observationScaleBadEvent M L m)ᶜ ↑(Cutoff.cutoffSampleLaw M)

The second IntegrableOn binder of the proved CombineExpectation endpoints, discharged. Global integrability restricts to any set.

theorem Algsuperdiff.Section3.Provider.Homogenization.integrableOn_coarseMatrixVariationBlock_compl_observationScaleBadEvent {d : ℕ} [NeZero d] (M : ABKModel d) (m L : ℤ) (e : HCPolySupport.Vec d) : MeasureTheory.IntegrableOn (coarseMatrixVariationBlock M m L e) (observationScaleBadEvent M L m)ᶜ ↑(Cutoff.cutoffSampleLaw M)