VarianceClosure

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

The carrier bridge and the descendant envelopes of the variance closure

ABK26. This module carries item (2) and the two missing inputs of item (3) of the depgraph record for node p.combine.corrected, the finite good-event Besov step.

Part A: the carrier bridge (item (2))

Two proved carriers had no seam between them.

• The variance-split carriers of VarianceSplit.lean are squared Euclidean operator norms of two single blocks of the coarse block matrix, centred at the annealed block matrix: starInverseCenteredFluctuationSq = |σ_*^{-1}(R;a) - σ_{L,*}^{-1}(□_n)|² starInverseKappaCenteredFluctuationSq = |(σ_*^{-1}κ)(R;a) - E[(σ_*^{-1}κ)(□_n)]|² (starInverseCenteredFluctuationSq and starInverseKappaCenteredFluctuationSq in VarianceSplit.lean).
• The Step-3 corridor carrier of CombineFiniteCarrierTransport.lean is the squared Euclidean operator norm of the full 2d × 2d starred fluctuation matrix 𝐁^{1/2}(𝐀_*^{-1}(U;a) - 𝐑𝐂𝐑)𝐁^{1/2} (starredFluctuationOperatorNormSq, VarianceBridge.lean).

The manuscript passes between them by conjugating with the diagonal gauge diag(λ^{1/2}𝟙, λ^{-1/2}𝟙) at λ = σ_L and reading off the two displayed entries of the conjugated matrix. Here that passage is exact: the conjugated matrix's rows are computed at the two block loads (e,0) and (0,e),

Δ (e,0) = (σ · Δ_{lowerRight} e , Δ_{upperRight} e), Δ (0,e) = (Δ_{lowerLeft} e , σ^{-1} · Δ_{upperLeft} e),

and the two single-block operator norms are recovered by ContinuousLinearMap.opNorm_le_bound. Only the two displayed halves are used; the companion halves are discarded by positivity, exactly as in the printed proof. The results are

σ² |Δ_{lowerRight}|² ≤ starredFluctuationOperatorNormSq 𝐁(σ) 𝐂 U a and |Δ_{lowerLeft}|² ≤ starredFluctuationOperatorNormSq 𝐁(σ) 𝐂 U a,

with |·| the Chapter 2 Euclidean matrix operator norm — the manuscript's |A|. The asymmetric weighting (σ² on the first, 1 on the second) is forced by the gauge and is exactly the printed weighting of (e.initial.JL.bound) and of (e.var.bound.astar.withS).

Composed with the proved corridor variance bound, Part A delivers the printed left side of the Step-3 display (e.var.bound.astar.withS) at the genuine cutoff law:

σ_L² var[σ_{L,*}^{-1}(□_n)] + var[σ_{L,*}^{-1}(□_n)κ_L(□_n)] ≤ 2 C_var δ (δ + 3^{-d(n-L)}),

where δ is the corridor's own two-term amplitude δ = E²γ + exp(-2E^{-3}γ^{-1}).

Part B: the two descendant envelopes (the missing inputs of item (3))

The hK producer (3) needs a uniform a.e. bound on the good event for CombineExpectation.coarseMatrixVariationBlock and CombineExpectation.coarseScaleSeparationBlock. Both reduce, through VarianceSplit.coarseScaleSeparation_eq_coarseBlockScaleSeparation, VarianceSplit.coarseBlockScaleSeparation_sub and the triangle inequality, to uniform bounds on

Ch02.matrixOperatorNorm (coarseBlockMatrix (cubeSet R) a.toFun).lowerRight and Ch02.matrixOperatorNorm (coarseBlockMatrix (cubeSet R) a.toFun).lowerLeft

over the descendants R of originCube d m. Both are supplied here.

• The σ_*^{-1} channel is deterministic: ≤ 4dν^{-1} at every descendant of every cube, with no event and no random envelope (matrixOperatorNorm_coarseBlockMatrix_lowerRight_le_of_mem_descendantsAtScale).
• The σ_*^{-1}κ channel is event-dependent, and of its three pieces only one is supplied here: the sharp positive semidefinite off-diagonal block bound |A_{lowerLeft}| ≤ √(|A_{upperLeft}|·|A_{lowerRight}|) (matrixOperatorNorm_lowerLeft_le_sqrt_of_isSymmetricBlockMat_of_blockPosDef). Combined with a single-term extraction from the finite-exponent upper multiscale ellipticity and with the good-event clause Λ_{1/4,1}(□_m) ≤ 2σ_L --- which is what CombineBadEvent.mem_observationScaleBadEvent_iff reads off the complement of observationScaleBadEvent M L m --- it gives c_{1/4,1}3^{-j/4} · |(σ_*^{-1}κ)(R)| ≤ √(2σ_L · 4dν^{-1}) for every descendant R of □_m at depth j, off the bad event. Since c_{1/4,1}3^{-j/4} is bounded below on j ≤ m - L, this is the K(d, σ_L, m - L, ν) shape the producer asks for. That composite is not assembled in this module. The deterministic route for this channel does not terminate in a deterministic constant: Cutoff.maxDescendantBMatrixNormAtScale_le_cutoffEnvelope bounds the upper-left block by 4dν^{-1}(coefficientCutoffCubeEllipticityUpper M L omega Q)², whose envelope Cutoff.coefficientCutoffCubeEntryBound = ν + cutoffLocalControl … (Cutoff/CoefficientFamily.lean) is a genuinely unbounded random variable. This is why the good event is needed for the κ channel and not for the other. It does terminate in an integrable random envelope, which is a different question and is exactly what item (4) needs; see below.

What is NOT proved here

• Item (3) is not closed. What remains is the mechanical assembly of the two envelopes above into the two a.e. bounds, over the corridor sum ∑_{n∈[L,m]} 3^{-(m-n)} and the descendant averages at depth (m-n).toNat: the depth-uniform weight min_{j ≤ (m-L).toNat} c_{1/4,1}3^{-j/4}, the triangle inequality on coarseBlockScaleSeparation, and descendantsAverage_le_descendantsAverage. No new mathematical input is needed; the two statements to produce are the a.e. bounds, on the good event (observationScaleBadEvent M L m)ᶜ, for the corridor sum and for vecNormSq (coarseScaleSeparation …), whose measurability halves are VarianceSplit.aemeasurable_coarseMatrixVariationCorridor and VarianceSplit.aemeasurable_coarseScaleSeparationSq.
• Item (4), global integrability of the two observables at the genuine law, is not performed here — but it is reachable, by a transcription and not a theorem. With E(ω):= Cutoff.coefficientCutoffCubeEllipticityUpper M L ω (originCube d m) the route is four proved steps, three of them in this file: (1) Cutoff.maxDescendantBMatrixNormAtScale_le_cutoffEnvelope — unconditional, depth-uniform, no event and no geometric weight — through the hmem step and its coefficient-field twin Cutoff.maxDescendantBMatrixNormCoeffFieldAtScale_le_cutoffEnvelope, gives |b(R;ω)| ≤ 4dν^{-1}E(ω)² at every descendant R of □_m, every depth, every ω; (2) the sharp lowerLeft bound below; (3) the deterministic lowerRight envelope below; hence (4) |(σ_*^{-1}κ)(R;ω)| ≤ 4dν^{-1}E(ω) on the whole sample space, and every natural power of E is integrable at (Cutoff.cutoffSampleLaw M).toMeasure (Cutoff.integrable_coefficientCutoffCubeEllipticityUpper_pow, from Cutoff.integrable_cutoffLocalControl_pow and Cutoff.coefficientCutoffCubeEllipticityUpper_le_majorant). Both target observables are already integrated against that exact measure (coarseMatrixVariationBlock, coarseScaleSeparationBlock and exists_integral_cutoffResponseJ_centralChild_le_expectationDisplay in CombineExpectation.lean); a RegCoeffField-side carrier that needs a transfer has the proved pattern Cutoff.coefficientCutoffLaw_eq_map (Cutoff/Law.lean) with integrable_map_measure and Integrable.mono', as in Cutoff.integrable_LambdaSqCoeffField_pow_cutoffLaw, and the corridor weight ∑_{n∈[L,m]}3^{-(m-n)} is a finite deterministic factor. What is to be produced is Integrable (CombineExpectation.coarseScaleSeparationBlock M m L e) (Cutoff.cutoffSampleLaw M).toMeasure and its coarseMatrixVariationBlock twin. The event-dependent route of Part B performs steps (1)--(3) and then discards the unconditional envelope in favour of the Λ² extraction plus the good event. What remains true is the item-(3)-scoped observation: item (3) asks for a deterministic constant K, and the deterministic route for the κ channel does not produce one, because the step-(1) envelope is the random E(ω). Integrable is not bounded; the two items ask different questions.
• Items (5), (6) and (7) — the corridor summation, the anchor wiring, and the +Cδ₁² absorption — are not performed.

The diagonal gauge

The two row readings

The operator-norm transfer

The carrier bridge

theorem Algsuperdiff.Section3.Provider.Homogenization.sq_mul_sq_matrixOperatorNorm_lowerRight_sub_le_starredFluctuationOperatorNormSq {d : ℕ} (sigma : Observable.PositiveScalar) (C : HCPolySupport.BlockMat d) (U : Set (HCPolySupport.Vec d)) (a : HCPolySupport.RegCoeffField d) : ↑sigma ^ 2 * HCPolySupport.Book.Ch02.matrixOperatorNorm ((HCPolySupport.coarseBlockMatrix U a.toFun).lowerRight - C.lowerRight) ^ 2 ≤ starredFluctuationOperatorNormSq (HCPolySupport.Book.Ch02.constantFullBlockMatrix (Observable.isotropicComparatorMatrix sigma)) C U a

The carrier bridge, lower-right channel. At the isotropic comparator normalizer 𝐁(σ), the squared Euclidean operator norm of the σ_*^{-1} channel of 𝐀(U;a) - 𝐂, weighted by σ², is below the squared operator norm of the full starred fluctuation matrix.

The weight σ² is the exact gauge weight of the manuscript's conjugation: the load (e,0) reads the lower-right block twice through σ^{1/2}.

theorem Algsuperdiff.Section3.Provider.Homogenization.sq_matrixOperatorNorm_lowerLeft_sub_le_starredFluctuationOperatorNormSq {d : ℕ} (sigma : Observable.PositiveScalar) (C : HCPolySupport.BlockMat d) (U : Set (HCPolySupport.Vec d)) (a : HCPolySupport.RegCoeffField d) : HCPolySupport.Book.Ch02.matrixOperatorNorm ((HCPolySupport.coarseBlockMatrix U a.toFun).lowerLeft - C.lowerLeft) ^ 2 ≤ starredFluctuationOperatorNormSq (HCPolySupport.Book.Ch02.constantFullBlockMatrix (Observable.isotropicComparatorMatrix sigma)) C U a

The carrier bridge, lower-left channel. The σ_*^{-1}κ channel of 𝐀(U;a) - 𝐂 carries no gauge weight: the load (0,e) reads the off-diagonal block once through σ^{-1/2} and once through σ^{1/2}. This is the printed asymmetry of (e.initial.JL.bound) -- weight σ_L² on the σ_*^{-1} variances, weight 1 on the σ_*^{-1}κ variances.

The genuine-law instances

theorem Algsuperdiff.Section3.Provider.Homogenization.coefficientCutoffLaw_sq_sigmaBar_mul_starInverseCenteredFluctuationSq_le {d : ℕ} (M : ABKModel d) (L n : ℤ) (R : HCPolySupport.TriadicCube d) (a : HCPolySupport.RegCoeffField d) : ↑(Annealed.sigmaBar M L) ^ 2 * starInverseCenteredFluctuationSq M L n R a ≤ starredFluctuationOperatorNormSq (cutoffComparatorNormalizer M L) (HCPolySupport.Book.Ch04.annealedBlockMatrixAtScale (Cutoff.coefficientCutoffLaw M L) n) (HCPolySupport.cubeSet R) a

The σ_*^{-1} variance carrier under the corridor observable. The variance-split integrand |σ_*^{-1}(R;a) - σ_{L,*}^{-1}(□_n)|², weighted by the printed σ_L², is below the Step-3 corridor observable at the same centering scale, sample by sample and at every cube.

theorem Algsuperdiff.Section3.Provider.Homogenization.coefficientCutoffLaw_starInverseKappaCenteredFluctuationSq_le {d : ℕ} (M : ABKModel d) (L n : ℤ) (R : HCPolySupport.TriadicCube d) (a : HCPolySupport.RegCoeffField d) : starInverseKappaCenteredFluctuationSq M L n R a ≤ starredFluctuationOperatorNormSq (cutoffComparatorNormalizer M L) (HCPolySupport.Book.Ch04.annealedBlockMatrixAtScale (Cutoff.coefficientCutoffLaw M L) n) (HCPolySupport.cubeSet R) a

The σ_*^{-1}κ variance carrier under the corridor observable. Same statement for the lower-left channel, at weight 1.

theorem Algsuperdiff.Section3.Provider.Homogenization.coefficientCutoffLaw_sq_sigmaBar_mul_starInverseVarianceAtScale_add_le {d : ℕ} (M : ABKModel d) (L n : ℤ) (hint : MeasureTheory.Integrable (fun (a : HCPolySupport.RegCoeffField d) => starredFluctuationOperatorNormSq (cutoffComparatorNormalizer M L) (HCPolySupport.Book.Ch04.annealedBlockMatrixAtScale (Cutoff.coefficientCutoffLaw M L) n) (HCPolySupport.cubeSet (HCPolySupport.originCube d n)) a) (Cutoff.coefficientCutoffLaw M L)) : ↑(Annealed.sigmaBar M L) ^ 2 * starInverseVarianceAtScale M L n + starInverseKappaVarianceAtScale M L n ≤ 2 * ∫ (a : HCPolySupport.RegCoeffField d), starredFluctuationOperatorNormSq (cutoffComparatorNormalizer M L) (HCPolySupport.Book.Ch04.annealedBlockMatrixAtScale (Cutoff.coefficientCutoffLaw M L) n) (HCPolySupport.cubeSet (HCPolySupport.originCube d n)) a ∂Cutoff.coefficientCutoffLaw M L

The left side of (e.var.bound.astar.withS) under the corridor observable. The printed combination σ_L² var[σ_{L,*}^{-1}(□_n)] + var[σ_{L,*}^{-1}(□_n)κ_L(□_n)] is at most twice the expectation of the Step-3 corridor observable.

The Integrable clause is a conditional A obligation in the convention of integral_starredFluctuationNormSq_le_descendantAndResponseBounds; see the module docstring.

The Step-3 display (e.var.bound.astar.withS)

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, MeasureTheory.Integrable (fun (a : HCPolySupport.RegCoeffField d) => starredFluctuationOperatorNormSq (cutoffComparatorNormalizer M L) (HCPolySupport.Book.Ch04.annealedBlockMatrixAtScale (Cutoff.coefficientCutoffLaw M L) n) (HCPolySupport.cubeSet (HCPolySupport.originCube d n)) a) (Cutoff.coefficientCutoffLaw M L) → ↑(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 coefficient cutoff law. Composing the carrier bridge with the proved Step-3 corridor variance bound exists_coefficientCutoff_finiteCorridor_starredFluctuationVariance_bound (CombineFiniteCarrierTransport.lean) gives the printed left side

σ_L² var[σ_{L,*}^{-1}(□_n)] + var[σ_{L,*}^{-1}(□_n)κ_L(□_n)]

below 2 C_var δ (δ + 3^{-d(n-L)}), where δ is the corridor's own two-term amplitude E²γ + exp(-2E^{-3}γ^{-1}). The printed constant C is 2 C_var.

This partially supports and does not realize the printed display: δ is strictly larger than the printed δ₁ := C E²γ, so the conclusion is a weaker form; the Integrable clause remains open; and this theorem has, as proved, no Lean consumer. What it does complete is the left-hand half — it is the first proved statement whose left side is literally the printed variance sum, the proved transport form carrying the starred integral there instead.

The last, Integrable, is the conditional obligation described there: without it the proved corridor bound is vacuous, since a non-integrable Bochner integral is 0.

This is a local Provider theorem and makes no source-node status claim.

Two inputs of the hK producer

theorem Algsuperdiff.Section3.Provider.Homogenization.matrixOperatorNorm_coarseBlockMatrix_lowerRight_le_of_mem_descendantsAtScale {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).lowerRight ≤ 4 * ↑d * M.nu⁻¹

The deterministic descendant envelope of the σ_*^{-1} channel. For the genuine coefficient cutoff, the Euclidean operator norm of the lower-right coarse block is at most 4dν^{-1} at every descendant of every cube, with no event and no random envelope: the bound is the molecular coercivity alone.

This is Cutoff.maxDescendantSigmaStarInvMatrixNormCoeffFieldAtScale_le_cutoffCoercivity (the ambient form of Cutoff.maxDescendantSigmaStarInvMatrixNormAtScale_le_cutoffCoercivity) read on the coarseBlockMatrix carrier through the public CoarseGraining Ch05.Section52 sup identity for the lower-right block (identifying the descendant inverse-ellipticity maximum with the lower-right-block supremum), applied below. It is the σ_*^{-1} half of the hK producer (3); the κ half is not supplied (see the module docstring).

The positive semidefinite off-diagonal block bound

theorem Algsuperdiff.Section3.Provider.Homogenization.matrixOperatorNorm_upperRight_le_sqrt_of_isSymmetricBlockMat_of_blockPosDef {d : ℕ} {A : HCPolySupport.BlockMat d} (hSymm : HCPolySupport.IsSymmetricBlockMat A) (hPos : HCPolySupport.Book.Ch02.BlockPosDef A) : HCPolySupport.Book.Ch02.matrixOperatorNorm A.upperRight ≤ √(HCPolySupport.Book.Ch02.matrixOperatorNorm A.upperLeft * HCPolySupport.Book.Ch02.matrixOperatorNorm A.lowerRight)

Positive block Cauchy--Schwarz, upper-right block. For a symmetric positive definite doubled block matrix the upper-right block has operator norm at most the geometric mean of the two diagonal block norms.

theorem Algsuperdiff.Section3.Provider.Homogenization.matrixOperatorNorm_lowerLeft_le_sqrt_of_isSymmetricBlockMat_of_blockPosDef {d : ℕ} {A : HCPolySupport.BlockMat d} (hSymm : HCPolySupport.IsSymmetricBlockMat A) (hPos : HCPolySupport.Book.Ch02.BlockPosDef A) : HCPolySupport.Book.Ch02.matrixOperatorNorm A.lowerLeft ≤ √(HCPolySupport.Book.Ch02.matrixOperatorNorm A.upperLeft * HCPolySupport.Book.Ch02.matrixOperatorNorm A.lowerRight)

Positive block Cauchy--Schwarz, lower-left block. This is the exact statement asked for (3), in its sharp form |A_{lowerLeft}|² ≤ |A_{upperLeft}| · |A_{lowerRight}|.