Coarse-graining support:

Support.Book.Ch05.Theorems.Section56.SmallContrastAssembly.WeightedGeometricSummation

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

Weighted geometric summations for the Section 5.6 assembly step

These are the deterministic summation estimates used to convert the beta-weighted scale-by-scale bounds in the small-contrast iteration into the manuscript-style geometric tail at the bottom scale.

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

Constant for summing the spatial decay tail 3^{-d r}.

Equations

• HCPolySupport.Book.Ch05.Section56.SmallContrastAssembly.weightedScaleDecaySumConst d = (HCPolySupport.geometricDiscount (↑d) 1)⁻¹

noncomputable def HCPolySupport.Book.Ch05.Section56.SmallContrastAssembly.weightedBetaSumConst (β : ℝ) : ℝ

Constant for summing the beta weights attached to the coarse-fluctuation iteration.

Equations

• HCPolySupport.Book.Ch05.Section56.SmallContrastAssembly.weightedBetaSumConst β = (HCPolySupport.geometricDiscount β 1)⁻¹

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

Parameter-only beta-weight summation constant.

Equations

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

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

Parameter-only constant for the deterministic tau-sum compression.

Equations

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

theorem HCPolySupport.Book.Ch05.Section56.SmallContrastAssembly.weightedScaleDecaySumConst_pos {d : ℕ} [NeZero d] : 0 < weightedScaleDecaySumConst d

theorem HCPolySupport.Book.Ch05.Section56.SmallContrastAssembly.weightedScaleDecaySumConst_nonneg {d : ℕ} [NeZero d] : 0 ≤ weightedScaleDecaySumConst d

theorem HCPolySupport.Book.Ch05.Section56.SmallContrastAssembly.weightedBetaSumConst_pos {β : ℝ} (hβ : 0 < β) : 0 < weightedBetaSumConst β

theorem HCPolySupport.Book.Ch05.Section56.SmallContrastAssembly.weightedBetaSumConst_nonneg {β : ℝ} (hβ : 0 < β) : 0 ≤ weightedBetaSumConst β

theorem HCPolySupport.Book.Ch05.Section56.SmallContrastAssembly.weightedBetaSumConstParams_pos {d : ℕ} (params : QuantitativeCoarseGrainedEllipticityParams d) : 0 < weightedBetaSumConstParams params

theorem HCPolySupport.Book.Ch05.Section56.SmallContrastAssembly.coarseFluctuationTauSumConstParams_pos {d : ℕ} (params : QuantitativeCoarseGrainedEllipticityParams d) : 0 < coarseFluctuationTauSumConstParams params

theorem HCPolySupport.Book.Ch05.Section56.SmallContrastAssembly.sum_Icc_shifted_rpow_decay_le_inv_geometricDiscount {α : ℝ} (hα : 0 < α) (k m : ℕ) : ∑ j ∈ Finset.Icc (k + 1) m, Real.rpow 3 (-α * ↑(j - k)) ≤ (geometricDiscount α 1)⁻¹

A shifted finite tail of 3^{-α r} is bounded by the full geometric series.

theorem HCPolySupport.Book.Ch05.Section56.SmallContrastAssembly.sum_Icc_shifted_varianceWeight_le_inv_geometricDiscount {β : ℝ} (hβ : 0 < β) (k m : ℕ) : ∑ j ∈ Finset.Icc (k + 1) m, Section54.VarianceBoundGoodScale.varianceWeight β m j ≤ weightedBetaSumConst β

The shifted beta-weight sum over j = k + 1, ..., m is bounded by the full beta geometric tail.

theorem HCPolySupport.Book.Ch05.Section56.SmallContrastAssembly.sum_Icc_varianceWeight_mul_scaleDecay_le_const {β : ℝ} (hβ_nonneg : 0 ≤ β) {d : ℕ} [NeZero d] {ell k m : ℕ} (hellk : ell ≤ k) : ∑ j ∈ Finset.Icc (k + 1) m, Section54.VarianceBoundGoodScale.varianceWeight β m j * Real.rpow 3 (-↑d * ↑(j - ell)) ≤ weightedScaleDecaySumConst d * Real.rpow 3 (-↑d * ↑(k - ell))

The spatially decaying term in the fluctuation budget sums to the bottom scale 3^{-d(k-ell)} up to a dimension-only constant.

theorem HCPolySupport.Book.Ch05.Section56.SmallContrastAssembly.sum_Icc_varianceWeight_mul_geometric_add_const_le {β A B : ℝ} (hβ : 0 < β) {d : ℕ} [NeZero d] {ell k m : ℕ} (hellk : ell ≤ k) (hA_nonneg : 0 ≤ A) (hB_nonneg : 0 ≤ B) : ∑ j ∈ Finset.Icc (k + 1) m, Section54.VarianceBoundGoodScale.varianceWeight β m j * (A * Real.rpow 3 (-↑d * ↑(j - ell)) + B) ≤ A * weightedScaleDecaySumConst d * Real.rpow 3 (-↑d * ↑(k - ell)) + weightedBetaSumConst β * B

Weighted summation of a geometric contribution plus a nonnegative constant contribution.

theorem HCPolySupport.Book.Ch05.Section56.SmallContrastAssembly.coarseFluctuationTauSumAtScale_le_const_tauAtScale_of_params {d : ℕ} [NeZero d] (params : QuantitativeCoarseGrainedEllipticityParams d) {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hstat : Ch04.RestrictionStationaryLaw P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) (hparams : hP4.params = params) {k m : ℕ} (hkm : k ≤ m) (e : Vec d) : have p_e := specialPAtScale hP hStruct (↑m) e; have q_e := specialQAtScale hP hStruct (↑m) e; Section53.JUpperBoundCoarseFluctuations.coarseFluctuationTauSumAtScale hP hStruct hP4 k m e ≤ coarseFluctuationTauSumConstParams params * tauAtScale P (↑m) (↑k) p_e q_e

Parameter-dependent version of the deterministic tau-sum compression. The constant depends on the quantitative ellipticity package, not on the law.