Coarse-graining support:

Support.Book.Ch05.Theorems.Section56.VarianceEstimateQuadratic.NormalizedStatements

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

theorem HCPolySupport.Book.Ch05.Section56.fullBlockFluctuationNormSq_le_two_descendantMean_add_two_error_of_error {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (center : ℤ) (Q : TriadicCube d) (j : ℕ) (a : RegCoeffField d) : Ch04.fullBlockNormalizedFluctuationOperatorNormSqAtScale hP hStruct center Q a ≤ 2 * descendantsAverageNormalizedFluctuationOperatorNormSq hP hStruct center Q j a + 2 * normalizedCoarseAverageErrorOperatorNormSq hP hStruct center Q j a

Pointwise form of the variance triangle after interpreting variance as the Section 5.4 squared operator-norm fluctuation.

theorem HCPolySupport.Book.Ch05.Section56.fullBlockNormalizedFluctuationOperatorNormSqAtScale_le_two_descendantsAverage_add_two_error {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (center : ℤ) (Q : TriadicCube d) (j : ℕ) (a : RegCoeffField d) : Ch04.fullBlockNormalizedFluctuationOperatorNormSqAtScale hP hStruct center Q a ≤ (2 * descendantsAverage Q j fun (R : TriadicCube d) => Ch04.fullBlockNormalizedFluctuationOperatorNormSq hP hStruct center (cubeSet R) a.toFun) + 2 * normalizedCoarseAverageErrorOperatorNormSq hP hStruct center Q j a

A version whose first term is the descendant average of the existing Section 5.4 fluctuation observable.

theorem HCPolySupport.Book.Ch05.Section56.fullBlockFluctuationNormSq_le_two_childMean_add_eight_traceAverageSq_ae {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) (m : ℕ) (Q : TriadicCube d) (j : ℕ) : (fun (a : RegCoeffField d) => Ch04.fullBlockNormalizedFluctuationOperatorNormSqAtScale hP hStruct (↑m) Q a) ≤ᵐ[P] fun (a : RegCoeffField d) => 2 * descendantsAverageNormalizedFluctuationOperatorNormSq hP hStruct (↑m) Q j a + 8 * normalizedBlockJTraceAverageSq hP hStruct (↑m) Q j a

Section 5.6 variance estimate with quadratic J error, retaining the descendant-average fluctuation term. This is the pointwise form of the manuscript variance splitting before the Jensen relaxation to the average of child variances.

theorem HCPolySupport.Book.Ch05.Section56.fullBlockFluctuationNormSq_integral_le_two_childMean_add_eight_of_eight {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) (m n k : ℕ) (hk : k ≤ n) : ∫ (a : RegCoeffField d), Ch04.fullBlockNormalizedFluctuationOperatorNormSqAtScale hP hStruct (↑m) (originCube d ↑n) a ∂P ≤ 2 * ∫ (a : RegCoeffField d), descendantsAverageNormalizedFluctuationOperatorNormSq hP hStruct (↑m) (originCube d ↑n) (n - k) a ∂P + 8 * ∫ (a : RegCoeffField d), normalizedBlockJTraceAverageSq hP hStruct (↑m) (originCube d ↑n) (n - k) a ∂P

Integrated Section 5.6 variance estimate with quadratic J error, using the Section 5.4 squared operator-norm fluctuation observable for the variance terms. The integrability needed to pass from the a.e. estimate to expectation is supplied by (P4).

theorem HCPolySupport.Book.Ch05.Section56.fullBlockFluctuationNormSq_le_two_childMean_add_eight_of_eight_JTraceAverageSq {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) (m : ℕ) (Q : TriadicCube d) (j : ℕ) : (fun (a : RegCoeffField d) => Ch04.fullBlockNormalizedFluctuationOperatorNormSqAtScale hP hStruct (↑m) Q a) ≤ᵐ[P] fun (a : RegCoeffField d) => (2 * descendantsAverage Q j fun (R : TriadicCube d) => Ch04.fullBlockNormalizedFluctuationOperatorNormSq hP hStruct (↑m) (cubeSet R) a.toFun) + 8 * normalizedBlockJTraceAverageSq hP hStruct (↑m) Q j a

Section 5.6 variance estimate with quadratic J error, expressed through the Section 5.4 squared operator-norm fluctuation observable. This is the a.s. pointwise inequality whose expectation gives the manuscript display e.var.a.star for the scalar block normalization used in Section 5.4.