VarianceBridge

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

Law-generic and normalized-law deterministic block-matrix variance bridges

ABK26 Lemma l.var.bounds (display e.var.a.star) bounds the variance of the normalized starred inverse coarse block matrix 𝐁^{1/2} 𝐀_{m,*}^{-1}(□_n) 𝐁^{1/2} by twice the variance of its descendant average plus eight times the second moment of the trace-type response average ⨍_z Σ_i 𝐉(z + □_k, 𝐁^{-1/2} e_i, 𝐁^{1/2} e_i; a_m).

Under that reading the printed proof is exact with the literal factors 2 and 8, and it is the reading used by the pinned CoarseGraining formalization of the same display (Homogenization.Book.Ch05.Section56, VarianceEstimateQuadratic).

This file bridges CoarseGraining's arbitrary-normalizer form to the manuscript's shape. Two changes of variable are needed.

• Reflection. CoarseGraining's fluctuating object is the coarse block matrix 𝐀(U), the manuscript's is the starred inverse 𝐀_*^{-1}(U) = 𝐑𝐀(U)𝐑, which CoarseGraining renders as blockReflect. Since 𝐑 is the symmetric involutive block swap, 𝐁^{1/2}(𝐑𝐀𝐑)𝐁^{1/2} = (𝐑𝐁^{1/2})ᵀ 𝐀 (𝐑𝐁^{1/2}), so every CoarseGraining statement transports under S ↦ 𝐑S. The same substitution turns CoarseGraining's response probes into the manuscript's, because 𝐉(U, 𝐑P, 𝐑Q) = 𝐉(U, Q, P).
• General 𝐁. CoarseGraining's integrated statement already carries arbitrary deterministic normalizers S and T; the manuscript instance is S = 𝐁^{-1/2}, T = 𝐁^{1/2}, implemented here through Mathlib's continuous functional calculus square root CFC.sqrt.

Main results

• starredFluctuationMatrix_eq_fullBlockFluctuationMatrixWithNormalizer
• blockJTraceAverageWithNormalizers_blockSwapMat_mul_ae
• starredFluctuationNormSq_le_descendantAndResponseBounds_ae

integral_starredFluctuationNormSq_le_descendantAndResponseBounds

The block swap matrix 𝐑

def Algsuperdiff.Section3.Provider.Homogenization.blockSwapMat (d : ℕ) : HCPolySupport.FullBlockMat d

The block swap matrix 𝐑 of ABK26, as a 2d × 2d matrix.

Equations

• Algsuperdiff.Section3.Provider.Homogenization.blockSwapMat d = Matrix.of fun (alpha beta : HCPolySupport.BlockCoord d) => if Sum.swap alpha = beta then 1 else 0

theorem Algsuperdiff.Section3.Provider.Homogenization.sum_swap_eq_iff {d : ℕ} (alpha beta : HCPolySupport.BlockCoord d) : Sum.swap alpha = beta ↔ alpha = Sum.swap beta

theorem Algsuperdiff.Section3.Provider.Homogenization.blockSwapMat_transpose (d : ℕ) : Matrix.transpose (blockSwapMat d) = blockSwapMat d

theorem Algsuperdiff.Section3.Provider.Homogenization.blockSwapMat_mul {d : ℕ} (M : HCPolySupport.FullBlockMat d) : blockSwapMat d * M = Matrix.submatrix M Sum.swap id

theorem Algsuperdiff.Section3.Provider.Homogenization.mul_blockSwapMat {d : ℕ} (M : HCPolySupport.FullBlockMat d) : M * blockSwapMat d = Matrix.submatrix M id Sum.swap

theorem Algsuperdiff.Section3.Provider.Homogenization.blockSwapMat_mul_mul {d : ℕ} (M : HCPolySupport.FullBlockMat d) : blockSwapMat d * M * blockSwapMat d = Matrix.submatrix M Sum.swap Sum.swap

theorem Algsuperdiff.Section3.Provider.Homogenization.toFullBlockMat_blockReflect {d : ℕ} (A : HCPolySupport.BlockMat d) : HCPolySupport.toFullBlockMat (HCPolySupport.blockReflect A) = Matrix.submatrix (HCPolySupport.toFullBlockMat A) Sum.swap Sum.swap

The manuscript's 𝐀_*^{-1} = 𝐑𝐀𝐑 in full 2d × 2d form.

theorem Algsuperdiff.Section3.Provider.Homogenization.fullBlockMatrixProbe_blockSwapMat_mul {d : ℕ} (X : HCPolySupport.FullBlockMat d) (alpha : HCPolySupport.BlockCoord d) : HCPolySupport.Book.Ch05.Section56.fullBlockMatrixProbe (blockSwapMat d * X) alpha = Prod.swap (HCPolySupport.Book.Ch05.Section56.fullBlockMatrixProbe X alpha)

The symmetric square root

theorem Algsuperdiff.Section3.Provider.Homogenization.transpose_cfcSqrt {d : ℕ} (B : HCPolySupport.FullBlockMat d) : (CFC.sqrt B).transpose = CFC.sqrt B

The continuous-functional-calculus square root of a positive semidefinite real matrix is symmetric.

The manuscript objects

noncomputable def Algsuperdiff.Section3.Provider.Homogenization.starredInverseCoarseBlockMatrix {d : ℕ} (U : Set (HCPolySupport.Vec d)) (a : HCPolySupport.RegCoeffField d) : HCPolySupport.BlockMat d

The starred inverse coarse block matrix 𝐀_*^{-1}(U;a) = 𝐑𝐀(U;a)𝐑.

Equations

• Algsuperdiff.Section3.Provider.Homogenization.starredInverseCoarseBlockMatrix U a = HCPolySupport.blockReflect (HCPolySupport.coarseBlockMatrix U a.toFun)

noncomputable def Algsuperdiff.Section3.Provider.Homogenization.starredFluctuationMatrix {d : ℕ} (B : HCPolySupport.FullBlockMat d) (C : HCPolySupport.BlockMat d) (U : Set (HCPolySupport.Vec d)) (a : HCPolySupport.RegCoeffField d) : HCPolySupport.FullBlockMat d

The manuscript fluctuation matrix 𝐁^{1/2}(𝐀_*^{-1}(U;a) - 𝐑𝐂𝐑)𝐁^{1/2}, centered at the deterministic starred inverse normalizer 𝐑𝐂𝐑 attached to the annealed block matrix 𝐂.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Algsuperdiff.Section3.Provider.Homogenization.starredFluctuationOperatorNormSq {d : ℕ} (B : HCPolySupport.FullBlockMat d) (C : HCPolySupport.BlockMat d) (U : Set (HCPolySupport.Vec d)) (a : HCPolySupport.RegCoeffField d) : ℝ

Squared operator norm of the manuscript fluctuation matrix.

Equations

• Algsuperdiff.Section3.Provider.Homogenization.starredFluctuationOperatorNormSq B C U a = ‖Matrix.toEuclideanCLM (Algsuperdiff.Section3.Provider.Homogenization.starredFluctuationMatrix B C U a)‖ ^ 2

noncomputable def Algsuperdiff.Section3.Provider.Homogenization.starredDescendantsAverageFluctuationMatrix {d : ℕ} (B : HCPolySupport.FullBlockMat d) (C : HCPolySupport.BlockMat d) (Q : HCPolySupport.TriadicCube d) (j : ℕ) (a : HCPolySupport.RegCoeffField d) : HCPolySupport.FullBlockMat d

Descendant average of the manuscript fluctuation matrices.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Algsuperdiff.Section3.Provider.Homogenization.starredDescendantsAverageFluctuationOperatorNormSq {d : ℕ} (B : HCPolySupport.FullBlockMat d) (C : HCPolySupport.BlockMat d) (Q : HCPolySupport.TriadicCube d) (j : ℕ) (a : HCPolySupport.RegCoeffField d) : ℝ

Squared operator norm of the descendant-average manuscript fluctuation.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Algsuperdiff.Section3.Provider.Homogenization.starredBlockJTraceAverage {d : ℕ} (B : HCPolySupport.FullBlockMat d) (Q : HCPolySupport.TriadicCube d) (j : ℕ) (a : HCPolySupport.RegCoeffField d) : ℝ

The manuscript trace-type response average ⨍_z Σ_i 𝐉(z + □_k, 𝐁^{-1/2} e_i, 𝐁^{1/2} e_i; a).

Equations

• Algsuperdiff.Section3.Provider.Homogenization.starredBlockJTraceAverage B Q j a = HCPolySupport.Book.Ch05.Section56.blockJTraceAverageWithNormalizers (CFC.sqrt B⁻¹) (CFC.sqrt B) Q j a

noncomputable def Algsuperdiff.Section3.Provider.Homogenization.starredBlockJTraceAverageSq {d : ℕ} (B : HCPolySupport.FullBlockMat d) (Q : HCPolySupport.TriadicCube d) (j : ℕ) (a : HCPolySupport.RegCoeffField d) : ℝ

Square of the manuscript trace-type response average.

Equations

• Algsuperdiff.Section3.Provider.Homogenization.starredBlockJTraceAverageSq B Q j a = Algsuperdiff.Section3.Provider.Homogenization.starredBlockJTraceAverage B Q j a ^ 2

Reflection transport of the fluctuation matrices

theorem Algsuperdiff.Section3.Provider.Homogenization.submatrix_swap_sub {d : ℕ} (X Y : HCPolySupport.FullBlockMat d) : Matrix.submatrix (X - Y) Sum.swap Sum.swap = Matrix.submatrix X Sum.swap Sum.swap - Matrix.submatrix Y Sum.swap Sum.swap

theorem Algsuperdiff.Section3.Provider.Homogenization.starredFluctuationMatrix_eq_fullBlockFluctuationMatrixWithNormalizer {d : ℕ} [NeZero d] {P : HCPolySupport.Book.Ch04.RestrictionCoeffLaw d} (hP : HCPolySupport.Book.Ch04.RestrictionLawCarrier P) (hStruct : HCPolySupport.Book.Ch04.RestrictionStructuralLaw P) (center : ℤ) (B : HCPolySupport.FullBlockMat d) (U : Set (HCPolySupport.Vec d)) (a : HCPolySupport.RegCoeffField d) : starredFluctuationMatrix B (HCPolySupport.Book.Ch04.scalarAnnealedBlockMatrixAtScale hP hStruct center) U a = HCPolySupport.Book.Ch05.Section56.fullBlockFluctuationMatrixWithNormalizer hP hStruct center (blockSwapMat d * CFC.sqrt B) U a

theorem Algsuperdiff.Section3.Provider.Homogenization.starredFluctuationMatrix_eq_normalizedDescendantAverage {d : ℕ} [NeZero d] {P : HCPolySupport.Book.Ch04.RestrictionCoeffLaw d} (hP : HCPolySupport.Book.Ch04.RestrictionLawCarrier P) (hStruct : HCPolySupport.Book.Ch04.RestrictionStructuralLaw P) (center : ℤ) (B : HCPolySupport.FullBlockMat d) (Q : HCPolySupport.TriadicCube d) (j : ℕ) (a : HCPolySupport.RegCoeffField d) : starredDescendantsAverageFluctuationMatrix B (HCPolySupport.Book.Ch04.scalarAnnealedBlockMatrixAtScale hP hStruct center) Q j a = HCPolySupport.Book.Ch05.Section56.descendantsAverageFluctuationMatrixWithNormalizer hP hStruct center (blockSwapMat d * CFC.sqrt B) Q j a

theorem Algsuperdiff.Section3.Provider.Homogenization.starredFluctuationOperatorNormSq_eq {d : ℕ} [NeZero d] {P : HCPolySupport.Book.Ch04.RestrictionCoeffLaw d} (hP : HCPolySupport.Book.Ch04.RestrictionLawCarrier P) (hStruct : HCPolySupport.Book.Ch04.RestrictionStructuralLaw P) (center : ℤ) (B : HCPolySupport.FullBlockMat d) (Q : HCPolySupport.TriadicCube d) (a : HCPolySupport.RegCoeffField d) : starredFluctuationOperatorNormSq B (HCPolySupport.Book.Ch04.scalarAnnealedBlockMatrixAtScale hP hStruct center) (HCPolySupport.cubeSet Q) a = HCPolySupport.Book.Ch05.Section56.fullBlockFluctuationOperatorNormSqAtScaleWithNormalizer hP hStruct center (blockSwapMat d * CFC.sqrt B) Q a

theorem Algsuperdiff.Section3.Provider.Homogenization.starredDescendantsAverageFluctuationOperatorNormSq_eq {d : ℕ} [NeZero d] {P : HCPolySupport.Book.Ch04.RestrictionCoeffLaw d} (hP : HCPolySupport.Book.Ch04.RestrictionLawCarrier P) (hStruct : HCPolySupport.Book.Ch04.RestrictionStructuralLaw P) (center : ℤ) (B : HCPolySupport.FullBlockMat d) (Q : HCPolySupport.TriadicCube d) (j : ℕ) (a : HCPolySupport.RegCoeffField d) : starredDescendantsAverageFluctuationOperatorNormSq B (HCPolySupport.Book.Ch04.scalarAnnealedBlockMatrixAtScale hP hStruct center) Q j a = HCPolySupport.Book.Ch05.Section56.descendantsAverageFluctuationOperatorNormSqWithNormalizer hP hStruct center (blockSwapMat d * CFC.sqrt B) Q j a

Reflection transport of the response probes

theorem Algsuperdiff.Section3.Provider.Homogenization.blockVecDot_swap_blockMatVecMul_swap {d : ℕ} (A : HCPolySupport.BlockMat d) (Z : HCPolySupport.BlockVec d) : HCPolySupport.blockVecDot (Prod.swap Z) (HCPolySupport.blockMatVecMul A (Prod.swap Z)) = HCPolySupport.blockVecDot Z (HCPolySupport.blockMatVecMul (HCPolySupport.blockReflect A) Z)

theorem Algsuperdiff.Section3.Provider.Homogenization.blockVecDot_swap_swap {d : ℕ} (X Y : HCPolySupport.BlockVec d) : HCPolySupport.blockVecDot (Prod.swap X) (Prod.swap Y) = HCPolySupport.blockVecDot Y X

theorem Algsuperdiff.Section3.Provider.Homogenization.fullBlockJTraceBudgetWithNormalizers_blockSwapMat_mul {d : ℕ} (X Y : HCPolySupport.FullBlockMat d) (A : HCPolySupport.BlockMat d) : HCPolySupport.Book.Ch05.Section56.fullBlockJTraceBudgetWithNormalizers (blockSwapMat d * X) (blockSwapMat d * Y) A = HCPolySupport.Book.Ch05.Section56.fullBlockJTraceBudgetWithNormalizers Y X A

𝐉(U, 𝐑P, 𝐑Q) = 𝐉(U, Q, P), at the level of the trace budget.

theorem Algsuperdiff.Section3.Provider.Homogenization.sum_blockJObservableCubeSetBlockVec_eq_fullBlockJTraceBudget {d : ℕ} [NeZero d] {a : HCPolySupport.RegCoeffField d} (ha : HCPolySupport.Book.Ch04.AELocallyUniformlyEllipticField a) (R : HCPolySupport.TriadicCube d) (S T : HCPolySupport.FullBlockMat d) : ∑ alpha : HCPolySupport.BlockCoord d, HCPolySupport.Book.Ch05.Section56.blockJObservableCubeSetBlockVec R (HCPolySupport.Book.Ch05.Section56.fullBlockMatrixProbe S alpha) (HCPolySupport.Book.Ch05.Section56.fullBlockMatrixProbe T alpha) a = HCPolySupport.Book.Ch05.Section56.fullBlockJTraceBudgetWithNormalizers S T (HCPolySupport.coarseBlockMatrix (HCPolySupport.cubeSet R) a.toFun)

The sum of block responses over the coordinate probes is the trace budget.

theorem Algsuperdiff.Section3.Provider.Homogenization.blockJTraceAverageWithNormalizers_blockSwapMat_mul {d : ℕ} [NeZero d] {a : HCPolySupport.RegCoeffField d} (ha : HCPolySupport.Book.Ch04.AELocallyUniformlyEllipticField a) (X Y : HCPolySupport.FullBlockMat d) (Q : HCPolySupport.TriadicCube d) (j : ℕ) : HCPolySupport.Book.Ch05.Section56.blockJTraceAverageWithNormalizers (blockSwapMat d * X) (blockSwapMat d * Y) Q j a = HCPolySupport.Book.Ch05.Section56.blockJTraceAverageWithNormalizers Y X Q j a

theorem Algsuperdiff.Section3.Provider.Homogenization.blockJTraceAverageWithNormalizers_blockSwapMat_mul_ae {d : ℕ} [NeZero d] {P : HCPolySupport.Book.Ch04.RestrictionCoeffLaw d} (hP : HCPolySupport.Book.Ch04.RestrictionLawCarrier P) (X Y : HCPolySupport.FullBlockMat d) (Q : HCPolySupport.TriadicCube d) (j : ℕ) : (fun (a : HCPolySupport.RegCoeffField d) => HCPolySupport.Book.Ch05.Section56.blockJTraceAverageWithNormalizers (blockSwapMat d * X) (blockSwapMat d * Y) Q j a) =ᵐ[P] fun (a : HCPolySupport.RegCoeffField d) => HCPolySupport.Book.Ch05.Section56.blockJTraceAverageWithNormalizers Y X Q j a

The law-generic starred variance estimate

theorem Algsuperdiff.Section3.Provider.Homogenization.integral_starredFluctuationNormSq_le_descendantAndResponseBounds {d : ℕ} [NeZero d] {P : HCPolySupport.Book.Ch04.RestrictionCoeffLaw d} (hP : HCPolySupport.Book.Ch04.RestrictionLawCarrier P) (hStruct : HCPolySupport.Book.Ch04.RestrictionStructuralLaw P) (center : ℤ) (B : HCPolySupport.FullBlockMat d) (hB : Matrix.PosDef B) (Q : HCPolySupport.TriadicCube d) (j : ℕ) (hdesc : MeasureTheory.Integrable (starredDescendantsAverageFluctuationOperatorNormSq B (HCPolySupport.Book.Ch04.scalarAnnealedBlockMatrixAtScale hP hStruct center) Q j) P) (hJ : MeasureTheory.Integrable (starredBlockJTraceAverageSq B Q j) P) : ∫ (a : HCPolySupport.RegCoeffField d), starredFluctuationOperatorNormSq B (HCPolySupport.Book.Ch04.scalarAnnealedBlockMatrixAtScale hP hStruct center) (HCPolySupport.cubeSet Q) a ∂P ≤ 2 * ∫ (a : HCPolySupport.RegCoeffField d), starredDescendantsAverageFluctuationOperatorNormSq B (HCPolySupport.Book.Ch04.scalarAnnealedBlockMatrixAtScale hP hStruct center) Q j a ∂P + 8 * ∫ (a : HCPolySupport.RegCoeffField d), starredBlockJTraceAverageSq B Q j a ∂P

The arbitrary-scale integrated starred variance inequality when the two right-hand observables are explicitly integrable. This separates the algebraic variance estimate from the source-specific moment argument that supplies integrability below relative scale zero.