Documentation

LeanPool.HighContrastHomogenization.Provider.Quenched.SmallContrastFusionStep

High-contrast homogenization: Provider.Quenched.SmallContrastFusionStep #

Imported from the Apache-2.0 HighContrastHomogenization development at commit 7a13dbcd8d6609264a713373f5c69ceeac870472.

The fusion's ∀ n binder body #

the corresponding argument step 3. Inside the fusion's ∀ n ≥ n_s binder, the account's hatted one-step conclusion at the generation t = N₀ + n has to become one line of the drop-history recursion for the sequence F j = hatExcess P q N₀ j. This file is that line, isolated as a lemma so the outer assembly can apply it without carrying the algebra.

The identifications are definitional: hatExcess P q N₀ n is d(Θ̂_{N₀+n} − 1), and the account's lagged scale s = t − H is N₀ + (n − H), so one_step_to_scalar_step_isotropy (the scalar conversion) yields directly in the shape per_generation_hrec_at_recursionAlpha_sharp_at_jb_src consumes. Nothing else happens here; the three coefficients are dropCoefficient, quadCoefficient and weakCoefficient of the corresponding argument.

theorem HCPolySupport.HighContrast.Quenched.dropCoefficient_nonneg (d : ℕ) {Cpre eta : ℝ} (hCpre : 0 ≤ Cpre) (heta : 0 < eta) :
0 ≤ dropCoefficient d Cpre eta