Coarse-graining support:

Support.Book.Ch05.Theorems.Section56.VarianceEstimateQuadratic.ArbitraryIntegrability

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

theorem HCPolySupport.Book.Ch05.Section56.fullBlockFluctuationOperatorNormSqWithNormalizer_translation_covariant {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (center : ℤ) (S : FullBlockMat d) : Ch04.IsRestrictionTranslationCovariant fun (U : Set (Vec d)) (a : RegCoeffField d) => fullBlockFluctuationOperatorNormSqWithNormalizer hP hStruct center S U a

Translation covariance of the arbitrary-normalizer full-block fluctuation observable.

theorem HCPolySupport.Book.Ch05.Section56.section56_norm_toEuclideanCLM_le_sum_abs_entries {ι : Type u_1} [Fintype ι] [DecidableEq ι] (M : Matrix ι ι ℝ) : ‖Matrix.toEuclideanCLM M‖ ≤ ↑(Fintype.card ι) * ∑ i : ι, ∑ j : ι, |M i j|

theorem HCPolySupport.Book.Ch05.Section56.section56_norm_toEuclideanCLM_sq_integrable_of_entry_memLp_two {d : ℕ} {P : Ch04.RestrictionCoeffLaw d} {Z : RegCoeffField d → FullBlockMat d} (hZ_aemeas : AEMeasurable Z P) (hZ_entry : ∀ (α β : BlockCoord d), MeasureTheory.MemLp (fun (a : RegCoeffField d) => Z a α β) 2 P) : MeasureTheory.Integrable (fun (a : RegCoeffField d) => ‖Matrix.toEuclideanCLM (Z a)‖ ^ 2) P

theorem HCPolySupport.Book.Ch05.Section56.integrable_fullBlockFluctuationOperatorNormSqWithNormalizer_originCube_from_P4 {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) (center : ℤ) (S : FullBlockMat d) (n : ℕ) : MeasureTheory.Integrable (fun (a : RegCoeffField d) => fullBlockFluctuationOperatorNormSqWithNormalizer hP hStruct center S (cubeSet (originCube d ↑n)) a) P

theorem HCPolySupport.Book.Ch05.Section56.integrable_fullBlockFluctuationOperatorNormSqWithNormalizer_originCube_from_P4_of_nonneg {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) (center : ℤ) (S : FullBlockMat d) (n : ℤ) (hn : 0 ≤ n) : MeasureTheory.Integrable (fun (a : RegCoeffField d) => fullBlockFluctuationOperatorNormSqWithNormalizer hP hStruct center S (cubeSet (originCube d n)) a) P

theorem HCPolySupport.Book.Ch05.Section56.integrable_fullBlockFluctuationOperatorNormSqWithNormalizer_from_P4_of_nonneg_scale {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) (center : ℤ) (S : FullBlockMat d) (R : TriadicCube d) (hR_nonneg : 0 ≤ R.scale) : MeasureTheory.Integrable (fun (a : RegCoeffField d) => fullBlockFluctuationOperatorNormSqWithNormalizer hP hStruct center S (cubeSet R) a) P

theorem HCPolySupport.Book.Ch05.Section56.fluctuationNormSq_descendantAverage_integrable_from_P4_stationary {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) (m n k : ℕ) (_hk : k ≤ n) (S : FullBlockMat d) : MeasureTheory.Integrable (fun (a : RegCoeffField d) => descendantsAverage (originCube d ↑n) (n - k) fun (R : TriadicCube d) => fullBlockFluctuationOperatorNormSqWithNormalizer hP hStruct (↑m) S (cubeSet R) a) P

theorem HCPolySupport.Book.Ch05.Section56.aemeasurable_fullBlockFluctuationMatrixWithNormalizer_cubeSet {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (center : ℤ) (S : FullBlockMat d) (Q : TriadicCube d) : AEMeasurable (fun (a : RegCoeffField d) => fullBlockFluctuationMatrixWithNormalizer hP hStruct center S (cubeSet Q) a) P

theorem HCPolySupport.Book.Ch05.Section56.aemeasurable_descendantsAverageFluctuationMatrixWithNormalizer {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (center : ℤ) (S : FullBlockMat d) (Q : TriadicCube d) (j : ℕ) : AEMeasurable (fun (a : RegCoeffField d) => descendantsAverageFluctuationMatrixWithNormalizer hP hStruct center S Q j a) P

theorem HCPolySupport.Book.Ch05.Section56.aemeasurable_descendantsAverageFluctuationOperatorNormSqWithNormalizer {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (center : ℤ) (S : FullBlockMat d) (Q : TriadicCube d) (j : ℕ) : AEMeasurable (fun (a : RegCoeffField d) => descendantsAverageFluctuationOperatorNormSqWithNormalizer hP hStruct center S Q j a) P

theorem HCPolySupport.Book.Ch05.Section56.integrable_descendantsAverageFluctuationOperatorNormSqWithNormalizer_from_P4_of_stationary {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) (m n k : ℕ) (hk : k ≤ n) (S : FullBlockMat d) : MeasureTheory.Integrable (descendantsAverageFluctuationOperatorNormSqWithNormalizer hP hStruct (↑m) S (originCube d ↑n) (n - k)) P

theorem HCPolySupport.Book.Ch05.Section56.memLp_two_blockJTraceAverageWithNormalizers_from_P4_of_stationary {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) (_m n k : ℕ) (_hk : k ≤ n) (S T : FullBlockMat d) : MeasureTheory.MemLp (blockJTraceAverageWithNormalizers S T (originCube d ↑n) (n - k)) 2 P

theorem HCPolySupport.Book.Ch05.Section56.integrable_blockJTraceAverageSqWithNormalizers_from_P4_of_stationary {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) (m n k : ℕ) (hk : k ≤ n) (S T : FullBlockMat d) : MeasureTheory.Integrable (blockJTraceAverageSqWithNormalizers S T (originCube d ↑n) (n - k)) P

theorem HCPolySupport.Book.Ch05.Section56.fullBlockFluctuationNormSq_integral_le_two_childMean_add_eight_JTraceAverageSq {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) (m n k : ℕ) (hk : k ≤ n) (S T : FullBlockMat d) : ∫ (a : RegCoeffField d), fullBlockFluctuationOperatorNormSqAtScaleWithNormalizer hP hStruct (↑m) S (originCube d ↑n) a ∂P ≤ 2 * ∫ (a : RegCoeffField d), descendantsAverageFluctuationOperatorNormSqWithNormalizer hP hStruct (↑m) S (originCube d ↑n) (n - k) a ∂P + 8 * ∫ (a : RegCoeffField d), blockJTraceAverageSqWithNormalizers S T (originCube d ↑n) (n - k) a ∂P

Integrated Section 5.6 variance estimate with quadratic J error and arbitrary deterministic normalizers. The manuscript specialization is S = B^{-1/2} and T = B^{1/2}.