High-contrast homogenization: Provider.Quenched.SmallContrastSlotValue

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

The variance slot in recursion shape

The last purely algebraic step of the slot instantiation: the value that entry_lagged_variance_supply_of_block_split delivers is put into the shape vsrcSeq + cV·F(j_b) that weakValueSharpMajorant_le_three_group_summed_at_level consumes, and its source part is put into the shallow-leg shape c₁·3^{-e(J-j)} + c₂·3^{-(J-j)} that slot_source_sum_split_sharp consumes, with e = d/2 ≥ 1.

The three named constants:

• supplyMsc — the supply's law constant (the only place a source moment survives), Msc = (2d)^{1/2}·κ₂·2(𝔪₁(K)·bC·3^{g(G+1)})·√(𝔪₂(K));
• slotSourceValue d Csub Msc m = √(2d)·(18·Csub·3^{-dm/2}·Msc + 288·3^{-m}) — the per-leg source, carrying all the decay in the lag m = p - j_b;
• slotBaseCoefficient d = 580·√(2d) — the coefficient of the base-scale excess F(j_b), dimension-only.

noncomputable def HCPolySupport.HighContrast.Quenched.supplyMsc {d : ℕ} (Cd g : ℝ) (mAl : Mat d) (Gacc : ℕ) (E : BlockMat d) (K : ℝ) : ℝ

The supply's law constant: the only surviving source moment.

Equations

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

noncomputable def HCPolySupport.HighContrast.Quenched.slotSourceValue (d : ℕ) (Csub Msc : ℝ) (m : ℕ) : ℝ

The per-leg source value of the variance slot, at lag m = p - j_b.

Equations

• HCPolySupport.HighContrast.Quenched.slotSourceValue d Csub Msc m = √(2 * ↑d) * (18 * (Csub * ↑(3 ^ (d * m)) ^ (-2⁻¹) * Msc) + 576 * (1 / 2 * 3 ^ (-↑m)))

noncomputable def HCPolySupport.HighContrast.Quenched.slotBaseCoefficient (d : ℕ) : ℝ

The base-scale coefficient of the variance slot.

Equations

• HCPolySupport.HighContrast.Quenched.slotBaseCoefficient d = √(2 * ↑d) * 580

theorem HCPolySupport.HighContrast.Quenched.slotBaseCoefficient_nonneg (d : ℕ) : 0 ≤ slotBaseCoefficient d

theorem HCPolySupport.HighContrast.Quenched.supply_value_slot_bound (d : ℕ) {Csub Msc Y c : ℝ} {m : ℕ} (hc0 : 0 ≤ c) (hc1 : c ≤ 1) (hcY : c ≤ 4 * Y) (hCsub : 0 ≤ Csub) (hMsc : 0 ≤ Msc) (hY0 : 0 ≤ Y) : √(2 * ↑d) * 1 * ((2 + 4 * (1 + c) ^ 2) * (Csub * ↑(3 ^ (d * m)) ^ (-2⁻¹) * Msc) + 4 * (1 + c) ^ 2 * (36 * (Y + 1 / 2 * 3 ^ (-↑m))) + c) ≤ slotSourceValue d Csub Msc m + slotBaseCoefficient d * Y

The supply value in slot shape. This is supply_value_bound instantiated at the supply's own pieces.

theorem HCPolySupport.HighContrast.Quenched.cast_three_pow_rpow (d m : ℕ) : ↑(3 ^ (d * m)) ^ (-2⁻¹) = 3 ^ (-(↑d / 2) * ↑m)

The subdivision power in real-exponent form.

theorem HCPolySupport.HighContrast.Quenched.slotSourceValue_eq (d : ℕ) (Csub Msc : ℝ) (m : ℕ) : slotSourceValue d Csub Msc m = √(2 * ↑d) * 18 * Csub * Msc * 3 ^ (-(↑d / 2) * ↑m) + √(2 * ↑d) * 288 * 3 ^ (-1 * ↑m)

The per-leg source in shallow-leg shape. This is the form slot_source_sum_split_sharp consumes, at e = d/2.

theorem HCPolySupport.HighContrast.Quenched.slotSourceValue_nonneg (d : ℕ) {Csub Msc : ℝ} (hCsub : 0 ≤ Csub) (hMsc : 0 ≤ Msc) (m : ℕ) : 0 ≤ slotSourceValue d Csub Msc m