Coarse-graining support:

Support.Book.Ch05.Theorems.Section56.SmallContrastAssembly.FluctuationSumEstimate

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

The unconditional fluctuation-sum estimate for Section 5.6

This file proves the analytic estimate which feeds the final constant selection in FinalAssembly.lean: the m-centered full-block fluctuation sum is bounded by the bottom-scale geometric decay and the square of the small-contrast excess at scale ell.

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

Parameter-only version of the trace-J geometric constant.

Equations

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

@[simp]

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

theorem HCPolySupport.Book.Ch05.Section56.SmallContrastAssembly.normalizedMatrixAverageGeometricConst_nonneg {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP4 : QuantitativeCoarseGrainedEllipticity P) : 0 ≤ normalizedMatrixAverageGeometricConst hP4

theorem HCPolySupport.Book.Ch05.Section56.SmallContrastAssembly.normalizedTraceJAverageGeometricConst_nonneg {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP4 : QuantitativeCoarseGrainedEllipticity P) : 0 ≤ normalizedTraceJAverageGeometricConst hP4

theorem HCPolySupport.Book.Ch05.Section56.SmallContrastAssembly.normalizedTraceJAverageThetaConst_nonneg (d : ℕ) : 0 ≤ normalizedTraceJAverageThetaConst d

theorem HCPolySupport.Book.Ch05.Section56.SmallContrastAssembly.fullBlockNormalizedFluctuationOperatorNormSqAtScale_le_center_ell {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) (hsmall : widetildeThetaAtScale P 0 hP4 ≤ 2) {ell m : ℕ} (hellm : ell ≤ m) (Q : TriadicCube d) (a : RegCoeffField d) : Ch04.fullBlockNormalizedFluctuationOperatorNormSqAtScale hP hStruct (↑m) Q a ≤ 32 * Ch04.fullBlockNormalizedFluctuationOperatorNormSqAtScale hP hStruct (↑ell) Q a + 2 * (thetaAtScale hP hStruct ↑ell - 1) ^ 2

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

The geometric coefficient in the one-scale fluctuation estimate.

Equations

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

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

The contrast-square coefficient in the one-scale fluctuation estimate.

Equations

• HCPolySupport.Book.Ch05.Section56.SmallContrastAssembly.fluctuationOneScaleThetaConst d = 32 * (8 * HCPolySupport.Book.Ch05.Section56.SmallContrastAssembly.normalizedTraceJAverageThetaConst d) + 2

theorem HCPolySupport.Book.Ch05.Section56.SmallContrastAssembly.fluctuationOneScaleGeometricConst_nonneg {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP4 : QuantitativeCoarseGrainedEllipticity P) : 0 ≤ fluctuationOneScaleGeometricConst hP4

theorem HCPolySupport.Book.Ch05.Section56.SmallContrastAssembly.fluctuationOneScaleThetaConst_nonneg (d : ℕ) : 0 ≤ fluctuationOneScaleThetaConst d

theorem HCPolySupport.Book.Ch05.Section56.SmallContrastAssembly.fullBlockNormalizedFluctuationOperatorNormSqAtScale_integral_le_geometric_add_theta {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) (hsmall : widetildeThetaAtScale P 0 hP4 ≤ 2) {ell j m : ℕ} (hellj : ell ≤ j) (hjm : j ≤ m) : ∫ (a : RegCoeffField d), Ch04.fullBlockNormalizedFluctuationOperatorNormSqAtScale hP hStruct (↑m) (originCube d ↑j) a ∂P ≤ fluctuationOneScaleGeometricConst hP4 * Real.rpow 3 (-↑d * ↑(j - ell)) + fluctuationOneScaleThetaConst d * (thetaAtScale hP hStruct ↑ell - 1) ^ 2

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

Parameter-only version of the one-scale geometric fluctuation constant.

Equations

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

@[simp]

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

theorem HCPolySupport.Book.Ch05.Section56.SmallContrastAssembly.coarseFluctuationFullBlockSumAtScale_eq_nat_Icc {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) (k m : ℕ) : have β := Section53.JUpperBoundCoarseFluctuations.section53CoarseFluctuationBeta hP4; Section53.JUpperBoundCoarseFluctuations.coarseFluctuationFullBlockSumAtScale hP hStruct hP4 k m = ∑ j ∈ Finset.Icc (k + 1) m, Section54.VarianceBoundGoodScale.varianceWeight β m j * ∫ (a : RegCoeffField d), Ch04.fullBlockNormalizedFluctuationOperatorNormSqAtScale hP hStruct (↑m) (originCube d ↑j) a ∂P

theorem HCPolySupport.Book.Ch05.Section56.SmallContrastAssembly.coarseFluctuationFullBlockSumAtScale_le_assembly_fluctuation_bound {d : ℕ} [NeZero d] (params : QuantitativeCoarseGrainedEllipticityParams d) : ∃ (Ktau : ℝ) (Kgeom : ℝ) (Ktheta : ℝ), ∀ {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P), Ch04.RestrictionStationaryLaw P → ∀ (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P), hP4.params = params → widetildeThetaAtScale P 0 hP4 ≤ 2 → ∀ (e : Vec d), vecNormSq e = 1 → ∀ {ell k m : ℕ}, ell < k → k < m → have p_e := specialPAtScale hP hStruct (↑m) e; have q_e := specialQAtScale hP hStruct (↑m) e; Section53.JUpperBoundCoarseFluctuations.coarseFluctuationFullBlockSumAtScale hP hStruct hP4 k m ≤ Ktau * tauAtScale P (↑m) (↑k) p_e q_e + Kgeom * Real.rpow 3 (-↑d * ↑(k - ell)) + Ktheta * (thetaAtScale hP hStruct ↑ell - 1) ^ 2

The unconditional parameter-uniform estimate for the coarse fluctuation sum used in the Section 5.6 assembly lemma.