High-contrast homogenization: Provider.Quenched.SmallContrastSlotFamily

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

The depth-indexed variance slot family

Step 4 of, first half: the family V : ℕ → ℝ that exists_account_one_step_entry_of_block_at_level consumes at every depth j ≤ H_w, assembled from the two regimes of-13.2, and its summed bound — the hVsum hypothesis of weakValueSharpMajorant_le_three_group_summed_at_level.

At the depth split J = t - j_b:

• j ≤ J (shallow): the leg's scale p = t - j satisfies p ≥ j_b, so the lagged supply is read at the base j_b, giving slotSourceValue d Csub Msc (J - j) + slotBaseCoefficient d · F(j_b);
• j > J (deep): the supply is read at the leg's own scale, giving the constant slotSourceValue d Csub Msc 0 + slotBaseCoefficient d · δ.

Summing against the weight 3^{-j/2} through slot_source_sum_split_sharp gives

vsum = (H_w+1)·(c₁+c₂+c₃)·3^{-J/2} + halfGeom·v₀, cVsum = halfGeom·(slotBaseCoefficient d + c₀),

with c₁ = √(2d)·18·Csub·Msc, c₂ = √(2d)·288 and c₃ the deep constant. The source part decays in the generation through J = ⌈n/4⌉, which is what's obstruction required and's rate α = (1-g)/8 absorbs.

theorem HCPolySupport.HighContrast.Quenched.linWeight_sum_le (Hw : ℕ) : ∑ j ∈ Finset.range (Hw + 1), linWeight j ≤ halfGeom

The total linear weight is below the geometric constant.

noncomputable def HCPolySupport.HighContrast.Quenched.deepSlotConstant (d : ℕ) (Csub Msc delta : ℝ) : ℝ

The deep-leg constant of the slot family.

Equations

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

noncomputable def HCPolySupport.HighContrast.Quenched.slotSourceSeq (d : ℕ) (Csub Msc delta : ℝ) (J j : ℕ) : ℝ

The source part of the slot family at depth j, split at J.

Equations

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

theorem HCPolySupport.HighContrast.Quenched.slotSourceSeq_nonneg (d : ℕ) {Csub Msc delta : ℝ} (hCsub : 0 ≤ Csub) (hMsc : 0 ≤ Msc) (hdelta : 0 ≤ delta) (J j : ℕ) : 0 ≤ slotSourceSeq d Csub Msc delta J j

theorem HCPolySupport.HighContrast.Quenched.slot_sum_with_base {Hw : ℕ} {V vs : ℕ → ℝ} {cV Fjb V0 v0src cv0 vsrcSum : ℝ} (hcV : 0 ≤ cV) (hFjb : 0 ≤ Fjb) (hVj : ∀ j ∈ Finset.range (Hw + 1), V j ≤ vs j + cV * Fjb) (hV0 : V0 ≤ v0src + cv0 * Fjb) (hv0 : 0 ≤ v0src) (hcv0 : 0 ≤ cv0) (hvsSum : ∑ j ∈ Finset.range (Hw + 1), linWeight j * vs j ≤ vsrcSum) : ∑ j ∈ Finset.range (Hw + 1), linWeight j * (V j + V0) ≤ vsrcSum + halfGeom * v0src + halfGeom * (cV + cv0) * Fjb

The hVsum hypothesis of the summed split. Every slot bounded by its source part plus a common multiple of the base excess gives the summed bound with the two explicit constants.