BlockVarianceBound

Ported from scottnarmstrong/CoarseGraining at c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4. Module imports, support namespace and local option directives adapted for Lean Pool.

Block-variance bound (t.block.variance)

This is the final bridge corollary supplying the variance input consumed by the entry-scale assembly (Homogenization.HighContrast.EntryScale). That consumer integrates the concrete Chapter 4 observable Ch04.fullBlockNormalizedFluctuationOperatorNormSqAtScale hP hStruct n (originCube d n) over the origin cube at the same centre scale n; the theorem below bounds exactly that integral by Cd·Θ⁶·(3^n)^{-(d-2)/(d-1)} under a ThetaEllipticLaw Θ P and the structural law.

Proof route

The observable is controlled a.s. by finitely many quadratic probes of the normalized fluctuation matrix H = D·(A_n − Ā_n)·D (fullBlockNormalizedFluctuationOperatorNormSqAtScale_le_probeSqBudget_ae). Each probe's second moment is the centered second moment (probe_sq_integral_le), uniformly ≤ 64·Cd·Θ⁶·(3^n)^{-β}. Summing the (2d)-dimensional finite probe net absorbs the dimensional counting into the constant Cd. RestrictionObservable integrability is not required: the pointwise budget bound is combined through integral_mono_of_nonneg since the observable is a square, hence nonnegative.

The finite-probe linearity is kept generic in the matrix family so that the heavy fullBlockNormalizedFluctuationMatrix definition is never unfolded during the summation algebra.

theorem HCPolySupport.integrable_fullBlockProbeSqBudget {d : ℕ} {P : Book.Ch04.RestrictionCoeffLaw d} {M : RegCoeffField d → FullBlockMat d} (hint : ∀ (q : FullBlockVec d), MeasureTheory.Integrable (fun (a : RegCoeffField d) => Book.Ch05.Section54.VarianceBoundGoodScale.fullBlockQuadratic (M a) q ^ 2) P) : MeasureTheory.Integrable (fun (a : RegCoeffField d) => Book.Ch05.Section54.VarianceBoundGoodScale.fullBlockProbeSqBudget (M a)) P

Integrability of the finite probe square budget, generic in the matrix family.

theorem HCPolySupport.integral_fullBlockProbeSqBudget_eq {d : ℕ} {P : Book.Ch04.RestrictionCoeffLaw d} {M : RegCoeffField d → FullBlockMat d} (hint : ∀ (q : FullBlockVec d), MeasureTheory.Integrable (fun (a : RegCoeffField d) => Book.Ch05.Section54.VarianceBoundGoodScale.fullBlockQuadratic (M a) q ^ 2) P) : ∫ (a : RegCoeffField d), Book.Ch05.Section54.VarianceBoundGoodScale.fullBlockProbeSqBudget (M a) ∂P = ↑(Fintype.card (BlockCoord d)) * ∑ α : BlockCoord d, ↑(Fintype.card (BlockCoord d)) * ∑ β : BlockCoord d, 3 * (∫ (a : RegCoeffField d), Book.Ch05.Section54.VarianceBoundGoodScale.fullBlockQuadratic (M a) (Book.Ch05.Section54.VarianceBoundGoodScale.fullBlockCoordinateProbe α) ^ 2 ∂P + ∫ (a : RegCoeffField d), Book.Ch05.Section54.VarianceBoundGoodScale.fullBlockQuadratic (M a) (Book.Ch05.Section54.VarianceBoundGoodScale.fullBlockPlusProbe α β) ^ 2 ∂P + ∫ (a : RegCoeffField d), Book.Ch05.Section54.VarianceBoundGoodScale.fullBlockQuadratic (M a) (Book.Ch05.Section54.VarianceBoundGoodScale.fullBlockMinusProbe α β) ^ 2 ∂P)

The finite probe square budget integrates to a finite sum of per-probe second moments, generic in the matrix family.

theorem HCPolySupport.integral_fullBlockProbeSqBudget_le {d : ℕ} {P : Book.Ch04.RestrictionCoeffLaw d} {M : RegCoeffField d → FullBlockMat d} (K : ℝ) (hint : ∀ (q : FullBlockVec d), MeasureTheory.Integrable (fun (a : RegCoeffField d) => Book.Ch05.Section54.VarianceBoundGoodScale.fullBlockQuadratic (M a) q ^ 2) P) (hbd : ∀ (q : FullBlockVec d), q ⬝ᵥ q ≤ 4 → ∫ (a : RegCoeffField d), Book.Ch05.Section54.VarianceBoundGoodScale.fullBlockQuadratic (M a) q ^ 2 ∂P ≤ K) : ∫ (a : RegCoeffField d), Book.Ch05.Section54.VarianceBoundGoodScale.fullBlockProbeSqBudget (M a) ∂P ≤ ↑(Fintype.card (BlockCoord d)) * ∑ _α : BlockCoord d, ↑(Fintype.card (BlockCoord d)) * ∑ _β : BlockCoord d, 3 * (K + K + K)

The finite probe square budget integral is bounded by a uniform per-probe bound K (valid on probes of Euclidean square norm ≤ 4), generic in M.

theorem HCPolySupport.integral_observable_le_of_probeBounds {d : ℕ} [NeZero d] {P : Book.Ch04.RestrictionCoeffLaw d} (hP : Book.Ch04.RestrictionLawCarrier P) (hStruct : Book.Ch04.RestrictionStructuralLaw P) (m : ℤ) (K : ℝ) (hint : ∀ (q : FullBlockVec d), MeasureTheory.Integrable (fun (a : RegCoeffField d) => Book.Ch05.Section54.VarianceBoundGoodScale.fullBlockQuadratic (Book.Ch05.Section54.VarianceBoundGoodScale.normalizedFluctuationMatrix hP hStruct m (cubeSet (originCube d m)) a.toFun) q ^ 2) P) (hbd : ∀ (q : FullBlockVec d), q ⬝ᵥ q ≤ 4 → ∫ (a : RegCoeffField d), Book.Ch05.Section54.VarianceBoundGoodScale.fullBlockQuadratic (Book.Ch05.Section54.VarianceBoundGoodScale.normalizedFluctuationMatrix hP hStruct m (cubeSet (originCube d m)) a.toFun) q ^ 2 ∂P ≤ K) : ∫ (a : RegCoeffField d), Book.Ch04.fullBlockNormalizedFluctuationOperatorNormSqAtScale hP hStruct m (originCube d m) a ∂P ≤ ↑(Fintype.card (BlockCoord d)) ^ 2 * (↑(Fintype.card (BlockCoord d)) * ∑ _α : BlockCoord d, ↑(Fintype.card (BlockCoord d)) * ∑ _β : BlockCoord d, 3 * (K + K + K))

Finite-probe assembly for the fluctuation observable. The observable is nonnegative and a.s. dominated by the probe square budget, so integral_mono_of_nonneg gives the bound without observable integrability.

theorem HCPolySupport.integral_fullBlockNormalizedFluctuation_le {d : ℕ} [NeZero d] (hd : 3 ≤ d) : ∃ (Cd : ℝ), 0 ≤ Cd ∧ ∀ {Θ : ℝ}, 1 ≤ Θ → ∀ {P : Book.Ch04.RestrictionCoeffLaw d} [MeasureTheory.IsProbabilityMeasure P] (hP : Book.Ch04.RestrictionLawCarrier P) (hStruct : Book.Ch04.RestrictionStructuralLaw P), ThetaEllipticLaw Θ P → ∀ {m : ℤ}, 0 ≤ m → ∫ (a : RegCoeffField d), Book.Ch04.fullBlockNormalizedFluctuationOperatorNormSqAtScale hP hStruct m (originCube d m) a ∂P ≤ Cd * Θ ^ 6 * (3 ^ m) ^ (-(↑d - 2) / (↑d - 1))

Block-variance bound (t.block.variance). The normalized full-block fluctuation observable at centre scale m, integrated over the origin cube at the same scale, is bounded by Cd·Θ⁶·(3^m)^{-(d-2)/(d-1)} under a ThetaEllipticLaw Θ P and the structural law. The constant Cd depends only on the dimension d.

This is the variance input consumed by the entry-scale assembly (Homogenization.HighContrast.EntryScale), which integrates the same observable at the same origin-cube scale. See the high-moment paper (Armstrong–Kuusi–Loher, to appear).