Coarse-graining support:

Support.Book.Ch05.Theorems.Section56.SmallContrastAssembly.TraceAverageEstimate

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

noncomputable def HCPolySupport.Book.Ch05.Section56.SmallContrastAssembly.normalizedTraceJAverageGeometricConst {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP4 : QuantitativeCoarseGrainedEllipticity P) : ℝ

Constant multiplying the geometric matrix-average contribution in the concrete trace-J square estimate.

Equations

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

noncomputable def HCPolySupport.Book.Ch05.Section56.SmallContrastAssembly.normalizedTraceJAverageThetaConst (d : ℕ) : ℝ

Constant multiplying (Theta_m - 1)^2 in the concrete trace-J square estimate.

Equations

• HCPolySupport.Book.Ch05.Section56.SmallContrastAssembly.normalizedTraceJAverageThetaConst d = 2 * ↑(Fintype.card (HCPolySupport.BlockCoord d)) ^ 2

theorem HCPolySupport.Book.Ch05.Section56.SmallContrastAssembly.normalizedBlockJTraceAverage_eq_trace_fluctuation_add_theta_gap {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) {child parent : ℕ} {a : RegCoeffField d} (ha : Ch04.AELocallyUniformlyEllipticField a) : have Q := originCube d ↑parent; have j := parent - child; have M := descendantsAverageNormalizedFluctuationMatrix hP hStruct (↑child) Q j a; have θ := thetaAtScale hP hStruct ↑child; normalizedBlockJTraceAverage hP hStruct (↑child) Q j a = (1 + θ) / 2 * Ch02.fullBlockTrace M + ↑(Fintype.card (BlockCoord d)) / 2 * (θ - 1)

theorem HCPolySupport.Book.Ch05.Section56.SmallContrastAssembly.normalizedBlockJTraceAverageSq_le_matrix_average_add_thetaSq {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 : ℕ} {a : RegCoeffField d} (ha : Ch04.AELocallyUniformlyEllipticField a) : normalizedBlockJTraceAverageSq hP hStruct (↑child) (originCube d ↑parent) (parent - child) a ≤ 8 * ↑(Fintype.card (BlockCoord d)) ^ 2 * descendantsAverageNormalizedFluctuationOperatorNormSq hP hStruct (↑child) (originCube d ↑parent) (parent - child) a + normalizedTraceJAverageThetaConst d * (thetaAtScale hP hStruct ↑child - 1) ^ 2

theorem HCPolySupport.Book.Ch05.Section56.SmallContrastAssembly.normalizedBlockJTraceAverageSq_integral_le_geometric_add_thetaSq_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), normalizedBlockJTraceAverageSq hP hStruct (↑child) (originCube d ↑parent) (parent - child) a ∂P ≤ normalizedTraceJAverageGeometricConst hP4 * Real.rpow 3 (-↑d * ↑(parent - child)) + normalizedTraceJAverageThetaConst d * (thetaAtScale hP hStruct ↑child - 1) ^ 2