Coarse-graining support:

Support.Book.Ch05.Theorems.Section54.VarianceBoundGoodScale.MatrixVariance

Imported from the Apache-2.0 CoarseGraining development at commit c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.

Matrix variance from finite scalar probes

This file integrates the finite-dimensional probe bound. It is deliberately internal: scalar probe integrability and bounds are supplied by the preceding Section 5.4 files before the public lemma is assembled.

theorem HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.fullBlockQuadratic_plusProbe_self {d : ℕ} (M : FullBlockMat d) (α : BlockCoord d) : fullBlockQuadratic M (fullBlockPlusProbe α α) = 4 * fullBlockQuadratic M (fullBlockCoordinateProbe α)

theorem HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.fullBlockQuadratic_minusProbe_self {d : ℕ} (M : FullBlockMat d) (α : BlockCoord d) : fullBlockQuadratic M (fullBlockMinusProbe α α) = 0

theorem HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.integral_fluctuationQuadratic_sq_eq_integral_abs_sub_dotProduct_sq {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) (m j : ℕ) (q : FullBlockVec d) : ∫ (a : RegCoeffField d), fullBlockQuadratic (normalizedFluctuationMatrix hP hStruct (↑m) (cubeSet (originCube d ↑j)) a.toFun) q ^ 2 ∂P = ∫ (a : RegCoeffField d), |normalizedQuadraticObservable hP hStruct (↑m) q (cubeSet (originCube d ↑j)) a.toFun - q ⬝ᵥ q| ^ 2 ∂P

theorem HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.integrable_fluctuationQuadratic_sq_from_P4 {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) (m j : ℕ) (q : FullBlockVec d) : MeasureTheory.Integrable (fun (a : RegCoeffField d) => fullBlockQuadratic (normalizedFluctuationMatrix hP hStruct (↑m) (cubeSet (originCube d ↑j)) a.toFun) q ^ 2) P

theorem HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.fullBlockNormalizedFluctuationOperatorNormSqAtScale_integral_le_probeBounds {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) (m j : ℕ) (Ccoord : BlockCoord d → ℝ) (Cplus Cminus : BlockCoord d → BlockCoord d → ℝ) (hcoord_int : ∀ (α : BlockCoord d), MeasureTheory.Integrable (fun (a : RegCoeffField d) => fullBlockQuadratic (normalizedFluctuationMatrix hP hStruct (↑m) (cubeSet (originCube d ↑j)) a.toFun) (fullBlockCoordinateProbe α) ^ 2) P) (hplus_int : ∀ (α β : BlockCoord d), MeasureTheory.Integrable (fun (a : RegCoeffField d) => fullBlockQuadratic (normalizedFluctuationMatrix hP hStruct (↑m) (cubeSet (originCube d ↑j)) a.toFun) (fullBlockPlusProbe α β) ^ 2) P) (hminus_int : ∀ (α β : BlockCoord d), MeasureTheory.Integrable (fun (a : RegCoeffField d) => fullBlockQuadratic (normalizedFluctuationMatrix hP hStruct (↑m) (cubeSet (originCube d ↑j)) a.toFun) (fullBlockMinusProbe α β) ^ 2) P) (hcoord : ∀ (α : BlockCoord d), ∫ (a : RegCoeffField d), fullBlockQuadratic (normalizedFluctuationMatrix hP hStruct (↑m) (cubeSet (originCube d ↑j)) a.toFun) (fullBlockCoordinateProbe α) ^ 2 ∂P ≤ Ccoord α) (hplus : ∀ (α β : BlockCoord d), ∫ (a : RegCoeffField d), fullBlockQuadratic (normalizedFluctuationMatrix hP hStruct (↑m) (cubeSet (originCube d ↑j)) a.toFun) (fullBlockPlusProbe α β) ^ 2 ∂P ≤ Cplus α β) (hminus : ∀ (α β : BlockCoord d), ∫ (a : RegCoeffField d), fullBlockQuadratic (normalizedFluctuationMatrix hP hStruct (↑m) (cubeSet (originCube d ↑j)) a.toFun) (fullBlockMinusProbe α β) ^ 2 ∂P ≤ Cminus α β) : ∫ (a : RegCoeffField d), Ch04.fullBlockNormalizedFluctuationOperatorNormSqAtScale hP hStruct (↑m) (originCube d ↑j) a ∂P ≤ ↑(Fintype.card (BlockCoord d)) ^ 2 * (↑(Fintype.card (BlockCoord d)) * ∑ α : BlockCoord d, ↑(Fintype.card (BlockCoord d)) * ∑ β : BlockCoord d, 3 * (Ccoord α + Cplus α β + Cminus α β))

Integrating the finite-probe pointwise bound reduces the full-block matrix variance to scalar quadratic-probe variances.