Coarse-graining support:

Support.Book.Ch05.Theorems.Section56.SmallContrastAssembly.MatrixAverageEstimate

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

theorem HCPolySupport.Book.Ch05.Section56.SmallContrastAssembly.fullBlockQuadratic_add {d : ℕ} (M N : FullBlockMat d) (q : FullBlockVec d) : Section54.VarianceBoundGoodScale.fullBlockQuadratic (M + N) q = Section54.VarianceBoundGoodScale.fullBlockQuadratic M q + Section54.VarianceBoundGoodScale.fullBlockQuadratic N q

theorem HCPolySupport.Book.Ch05.Section56.SmallContrastAssembly.fullBlockQuadratic_smul {d : ℕ} (c : ℝ) (M : FullBlockMat d) (q : FullBlockVec d) : Section54.VarianceBoundGoodScale.fullBlockQuadratic (c • M) q = c * Section54.VarianceBoundGoodScale.fullBlockQuadratic M q

def HCPolySupport.Book.Ch05.Section56.SmallContrastAssembly.fullBlockQuadraticLinearMap {d : ℕ} (q : FullBlockVec d) : FullBlockMat d →ₗ[ℝ] ℝ

Linear functional evaluating a full block matrix at a fixed quadratic probe vector.

Equations

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

theorem HCPolySupport.Book.Ch05.Section56.SmallContrastAssembly.fullBlockQuadratic_descendantsAverageFullBlockMat {d : ℕ} (Q : TriadicCube d) (j : ℕ) (F : TriadicCube d → FullBlockMat d) (q : FullBlockVec d) : Section54.VarianceBoundGoodScale.fullBlockQuadratic (descendantsAverageFullBlockMat Q j F) q = descendantsAverage Q j fun (R : TriadicCube d) => Section54.VarianceBoundGoodScale.fullBlockQuadratic (F R) q

theorem HCPolySupport.Book.Ch05.Section56.SmallContrastAssembly.integral_origin_fullBlockNormalizedQuadraticObservable_self_eq_dotProduct {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) (m : ℕ) (q : FullBlockVec d) : ∫ (a : RegCoeffField d), Section54.VarianceBoundGoodScale.normalizedQuadraticObservable hP hStruct (↑m) q (cubeSet (originCube d ↑m)) a.toFun ∂P = q ⬝ᵥ q

theorem HCPolySupport.Book.Ch05.Section56.SmallContrastAssembly.descendantMean_fullBlockQuadratic_eq_centeredMean {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) {child parent : ℕ} (hchild_parent : child ≤ parent) (q : FullBlockVec d) (a : RegCoeffField d) : Section54.VarianceBoundGoodScale.fullBlockQuadratic (descendantsAverageNormalizedFluctuationMatrix hP hStruct (↑child) (originCube d ↑parent) (parent - child) a) q = Ch04.restrictionCenteredDescendantAverage P (↑child) (↑parent) (Section54.VarianceBoundGoodScale.fullBlockNormalizedQuadraticObservableR hP hStruct (↑child) q) a

theorem HCPolySupport.Book.Ch05.Section56.SmallContrastAssembly.aemeasurable_fullBlockNormalizedQuadraticObservable_cubeSet_of_P4 {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (center : ℤ) (q : FullBlockVec d) (Q : TriadicCube d) : AEMeasurable (fun (a : RegCoeffField d) => Section54.VarianceBoundGoodScale.normalizedQuadraticObservable hP hStruct center q (cubeSet Q) a.toFun) P

theorem HCPolySupport.Book.Ch05.Section56.SmallContrastAssembly.aemeasurable_fullBlockNormalizedQuadraticObservable_descendants_of_P4 {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (center : ℤ) (q : FullBlockVec d) (Q : TriadicCube d) (n : ℤ) (R : TriadicCube d) : R ∈ descendantsAtScale Q n → AEMeasurable (fun (a : RegCoeffField d) => Section54.VarianceBoundGoodScale.normalizedQuadraticObservable hP hStruct center q (cubeSet R) a.toFun) P

noncomputable def HCPolySupport.Book.Ch05.Section56.SmallContrastAssembly.normalizedQuadraticProbeAverageRootBound {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (child parent : ℕ) (q : FullBlockVec d) : ℝ

Rosenthal root bound for averaged centered normalized quadratic probes, using the second moment at the child scale and the descendant count.

Equations

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

theorem HCPolySupport.Book.Ch05.Section56.SmallContrastAssembly.fullBlockNormalizedQuadraticObservable_centeredOrigin_sq_integrable_at_self {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) (child : ℕ) (q : FullBlockVec d) : MeasureTheory.Integrable (fun (a : RegCoeffField d) => |Ch04.restrictionCenteredOriginObservable P (↑child) (Section54.VarianceBoundGoodScale.fullBlockNormalizedQuadraticObservableR hP hStruct (↑child) q) a| ^ 2) P

theorem HCPolySupport.Book.Ch05.Section56.SmallContrastAssembly.fullBlockQuadratic_descendantsAverageNormalizedFluctuationMatrix_sq_integrable {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) {child parent : ℕ} (hchild_parent : child ≤ parent) (q : FullBlockVec d) : MeasureTheory.Integrable (fun (a : RegCoeffField d) => Section54.VarianceBoundGoodScale.fullBlockQuadratic (descendantsAverageNormalizedFluctuationMatrix hP hStruct (↑child) (originCube d ↑parent) (parent - child) a) q ^ 2) P

theorem HCPolySupport.Book.Ch05.Section56.SmallContrastAssembly.fullBlockQuadratic_descendantsAverageNormalizedFluctuationMatrix_integral_sq_le {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) {child parent : ℕ} (hchild_parent : child ≤ parent) (q : FullBlockVec d) : ∫ (a : RegCoeffField d), Section54.VarianceBoundGoodScale.fullBlockQuadratic (descendantsAverageNormalizedFluctuationMatrix hP hStruct (↑child) (originCube d ↑parent) (parent - child) a) q ^ 2 ∂P ≤ normalizedQuadraticProbeAverageRootBound hP hStruct child parent q ^ 2

theorem HCPolySupport.Book.Ch05.Section56.SmallContrastAssembly.descendantsAverageNormalizedFluctuationMatrix_isSymm_ae {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (center : ℤ) (Q : TriadicCube d) (j : ℕ) : ∀ᵐ (a : RegCoeffField d) ∂P, Matrix.IsSymm (descendantsAverageNormalizedFluctuationMatrix hP hStruct center Q j a)

theorem HCPolySupport.Book.Ch05.Section56.SmallContrastAssembly.descendantsAverageNormalizedFluctuationOperatorNormSq_le_probeSqBudget_ae {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (center : ℤ) (Q : TriadicCube d) (j : ℕ) : (fun (a : RegCoeffField d) => descendantsAverageNormalizedFluctuationOperatorNormSq hP hStruct center Q j a) ≤ᵐ[P] fun (a : RegCoeffField d) => ↑(Fintype.card (BlockCoord d)) ^ 2 * Section54.VarianceBoundGoodScale.fullBlockProbeSqBudget (descendantsAverageNormalizedFluctuationMatrix hP hStruct center Q j a)

noncomputable def HCPolySupport.Book.Ch05.Section56.SmallContrastAssembly.normalizedMatrixAverageProbeRootBudget {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (child parent : ℕ) : ℝ

Matrix average budget assembled from squared root bounds for coordinate, sum, and difference probes.

Equations

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

theorem HCPolySupport.Book.Ch05.Section56.SmallContrastAssembly.descendantsAverageNormalizedFluctuationOperatorNormSq_integral_le_probeRootBudget {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) {child parent : ℕ} (hchild_parent : child ≤ parent) : ∫ (a : RegCoeffField d), descendantsAverageNormalizedFluctuationOperatorNormSq hP hStruct (↑child) (originCube d ↑parent) (parent - child) a ∂P ≤ normalizedMatrixAverageProbeRootBudget hP hStruct child parent