Documentation

LeanPool.HighContrastHomogenization.Support.Book.Ch05.Theorems.Section56.SmallContrastAlgebraicDecay.ScalarRecursion

Coarse-graining support: #

Support.Book.Ch05.Theorems.Section56.SmallContrastAlgebraicDecay.ScalarRecursion

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

Scalar reductions for Proposition p.small.contrast.algebraic.decay #

This file extracts the manuscript scalar recursion ingredients from the Section 5.6 assembly estimate. In particular, the additivity defect for the special vectors at scale m is controlled by the drop of Theta from k to m.

source
theorem HCPolySupport.Book.Ch05.Section56.SmallContrastAlgebraicDecay.widetildeThetaAtScale_zero_le_two_of_sub_one_le_delta {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} {hP4 : QuantitativeCoarseGrainedEllipticity P} {delta : ℝ} (hdelta_le_one : delta ≤ 1) (hsmall : widetildeThetaAtScale P 0 hP4 - 1 ≤ delta) :
widetildeThetaAtScale P 0 hP4 ≤ 2

If \widetilde\Theta_0 - 1 is at most a parameter not exceeding one, then \widetilde\Theta_0 ≤ 2.

source
theorem HCPolySupport.Book.Ch05.Section56.SmallContrastAlgebraicDecay.thetaAtScale_le_delta_of_widetildeAtZero {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) {delta : ℝ} (hsmall : widetildeThetaAtScale P 0 hP4 - 1 ≤ delta) (m : ℕ) :
thetaAtScale hP hStruct ↑m - 1 ≤ delta

Smallness at scale zero propagates to all scalar contrasts.

source
theorem HCPolySupport.Book.Ch05.Section56.SmallContrastAlgebraicDecay.half_sum_sub_le_product_drop {r x y : ℝ} (hr : 1 ≤ r) (hx : r ≤ x) (hy : r ≤ y) :
1 / 2 * (x - r) + 1 / 2 * (y - r) ≤ x * y - r ^ 2

A real-variable form of the special-vector tau drop.

source
theorem HCPolySupport.Book.Ch05.Section56.SmallContrastAlgebraicDecay.tauAtScale_special_le_thetaAtScale_sub {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) {k m : ℕ} (hkm : k ≤ m) (e : Vec d) (he : vecNormSq e = 1) :
have p_e := specialPAtScale hP hStruct (↑m) e; have q_e := specialQAtScale hP hStruct (↑m) e; tauAtScale P (↑m) (↑k) p_e q_e ≤ thetaAtScale hP hStruct ↑k - thetaAtScale hP hStruct ↑m

The special-vector additivity defect is controlled by the scalar contrast drop between scales k and m.