Coarse-graining support:

Support.Book.Ch05.Theorems.Section56.SmallContrastAlgebraicDecay.Recurrence

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

theorem HCPolySupport.Book.Ch05.Section56.SmallContrastAlgebraicDecay.scalar_contraction_of_drop_bound {C Fm Fk S : ℝ} (hC : 0 < C) (hS : 0 ≤ S) (h : 1 / 4 * Fm ≤ C * (Fk - Fm + S)) : have θ := 4 * C / (1 + 4 * C); Fm ≤ θ * Fk + S

Absorb the negative multiple of F_m in the manuscript scalar recursion.

theorem HCPolySupport.Book.Ch05.Section56.SmallContrastAlgebraicDecay.scalar_contraction_recursion_from_assembly {d : ℕ} [NeZero d] (params : QuantitativeCoarseGrainedEllipticityParams d) : ∃ (C : ℝ) (θ : ℝ), 0 < C ∧ 0 < θ ∧ θ < 1 ∧ ∀ {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier 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 → C ≤ ↑(m - k) → have β := Section53.JUpperBoundCoarseFluctuations.section53CoarseFluctuationBeta hP4; thetaAtScale hP hStruct ↑m - 1 ≤ θ * (thetaAtScale hP hStruct ↑k - 1) + Real.rpow 3 (-β * ↑m) + Real.rpow 3 (-↑d * ↑(k - ell)) + (thetaAtScale hP hStruct ↑ell - 1) ^ 2

The scalar recurrence obtained from Lemma l.small.contrast.assembly.

The constant is selected before the probability law; the only scale hypotheses are the manuscript window ell < k < m and the required coarse gap.