Coarse-graining support:

Support.Book.Ch05.Theorems.Section56.SmallContrastAssembly.MatrixAverageGeometric

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

noncomputable def HCPolySupport.Book.Ch05.Section56.SmallContrastAssembly.refinedVarianceBasicBudgetSmallContrastConstParams {d : ℕ} (params : QuantitativeCoarseGrainedEllipticityParams d) : ℝ

Parameter-only version of the small-contrast basic refined variance budget.

Equations

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

noncomputable def HCPolySupport.Book.Ch05.Section56.SmallContrastAssembly.normalizedQuadraticProbeAverageUniformRootSqConstParams {d : ℕ} (params : QuantitativeCoarseGrainedEllipticityParams d) : ℝ

Parameter-only version of the uniform one-probe root-square constant.

Equations

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

noncomputable def HCPolySupport.Book.Ch05.Section56.SmallContrastAssembly.normalizedMatrixAverageGeometricConstParams {d : ℕ} (params : QuantitativeCoarseGrainedEllipticityParams d) : ℝ

Parameter-only constant for the compressed matrix-average geometric estimate.

Equations

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

@[simp]

theorem HCPolySupport.Book.Ch05.Section56.SmallContrastAssembly.refinedVarianceBasicBudgetSmallContrastConstParams_eq_of_P4 {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP4 : QuantitativeCoarseGrainedEllipticity P) : refinedVarianceBasicBudgetSmallContrastConstParams hP4.params = refinedVarianceBasicBudgetSmallContrastConst hP4

@[simp]

theorem HCPolySupport.Book.Ch05.Section56.SmallContrastAssembly.normalizedQuadraticProbeAverageUniformRootSqConstParams_eq_of_P4 {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP4 : QuantitativeCoarseGrainedEllipticity P) : normalizedQuadraticProbeAverageUniformRootSqConstParams hP4.params = normalizedQuadraticProbeAverageUniformRootSqConst hP4

@[simp]

theorem HCPolySupport.Book.Ch05.Section56.SmallContrastAssembly.normalizedMatrixAverageGeometricConstParams_eq_of_P4 {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP4 : QuantitativeCoarseGrainedEllipticity P) : normalizedMatrixAverageGeometricConstParams hP4.params = normalizedMatrixAverageGeometricConst hP4

theorem HCPolySupport.Book.Ch05.Section56.SmallContrastAssembly.descendantsAtScale_originCube_nat_card_inv_eq_rpow (d child parent : ℕ) (hchild_parent : child ≤ parent) : (↑(descendantsAtScale (originCube d ↑parent) ↑child).card)⁻¹ = Real.rpow 3 (-↑d * ↑(parent - child))

theorem HCPolySupport.Book.Ch05.Section56.SmallContrastAssembly.descendantsAverageNormalizedFluctuationOperatorNormSq_integral_le_geometric_of_smallContrast {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) (hsmall : widetildeThetaAtScale P 0 hP4 ≤ 2) {child parent : ℕ} (hchild_parent : child ≤ parent) : ∫ (a : RegCoeffField d), descendantsAverageNormalizedFluctuationOperatorNormSq hP hStruct (↑child) (originCube d ↑parent) (parent - child) a ∂P ≤ normalizedMatrixAverageGeometricConst hP4 * Real.rpow 3 (-↑d * ↑(parent - child))

theorem HCPolySupport.Book.Ch05.Section56.SmallContrastAssembly.descendantsAverageNormalizedFluctuationOperatorNormSq_homogenizationScale {d : ℕ} [NeZero d] (params : QuantitativeCoarseGrainedEllipticityParams d) : ∃ (C : ℝ), 0 < C ∧ ∀ {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P), hP4.params = params → widetildeThetaAtScale P 0 hP4 ≤ 2 → ∀ {child parent : ℕ}, child ≤ parent → ∫ (a : RegCoeffField d), descendantsAverageNormalizedFluctuationOperatorNormSq hP hStruct (↑child) (originCube d ↑parent) (parent - child) a ∂P ≤ C * Real.rpow 3 (-↑d * ↑(parent - child))

Manuscript-style small-contrast matrix-average estimate.

The constant is chosen before the law P; it depends only on the quantitative ellipticity parameters and the dimension.