High-contrast homogenization: Provider.Quenched.SmallContrastSlotAlgebraAtLevel #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
The summed three-group split at a released threshold pair #
The summed split with the bad-event majorant read at a free threshold pair.
The pinned form is this at (1 / 2, 1), definitionally. As in the unsummed
split the majorant is an opaque summand of both the hypothesis and the base,
so the proof is the pinned one term for term.
theorem
HCPolySupport.HighContrast.Quenched.weakValueSharpMajorant_le_three_group_summed_at_level
{d : ℕ}
{M L rho : ℝ}
{Hw : ℕ}
{V : ℕ → ℝ}
{V0 : ℝ}
{Dr : ℕ → ℝ}
{Vmean : ℝ}
{F : ℕ → ℝ}
{n jb : ℕ}
{vsum cVsum vmsrc cVm bsrc cD delta alpha bmaj beta lev : ℝ}
(hFmono : ∀ (p q : ℕ), p ≤ q → F q ≤ F p)
(hM0 : 0 ≤ M)
(hrho1 : rho < 1)
(halpha0 : 0 < alpha)
(halphaHalf : alpha ≤ 1 / 2)
(hrhoAlpha : 1 / 2 - rho / 2 = alpha)
(hHw : Hw + 1 ≤ n)
(hcD0 : 0 ≤ cD)
(hdelta0 : 0 ≤ delta)
(hVsum : ∑ j ∈ Finset.range (Hw + 1), 3 ^ (-(1 / 2) * ↑j) * (V j + V0) ≤ vsum + cVsum * F jb)
(hVmean : Vmean ≤ vmsrc + cVm * F jb)
(hDr0 : ∀ (j : ℕ), 0 ≤ Dr j)
(hDrdelta : ∀ j ∈ Finset.range (Hw + 1), Dr j ≤ delta)
(hDr : ∀ j ∈ Finset.range (Hw + 1), Dr j ≤ cD * (F (n - j) - F n))
(hbad :
√2 * √(L + 1) * Response.profileBadMajorantAt 4 bmaj beta lev + √2 * 3 ^ (-((1 - rho) / 2) * ↑Hw) * √(L + 1) ≤ bsrc)
:
∃ (w : ℝ),
0 ≤ w ∧ 16 * M * √L * (∑ j ∈ Finset.range (Hw + 1), 3 ^ (-(1 / 2) * ↑j) * (V j + V0 + Dr j) + ∑ j ∈ Finset.range (Hw + 1), 3 ^ (-(1 / 2 - rho / 2) * ↑j) * √(2 * ↑d * Dr j)) + 16 * M / (2 * ((1 - rho) / 2)) * (√2 * √(L + 1) * Response.profileBadMajorantAt 4 bmaj beta lev + √2 * 3 ^ (-((1 - rho) / 2) * ↑Hw) * √(L + 1)) + Response.constantSeminormCoefficient * (M * √7 * Vmean) ≤ weakSourceGroupSummed M L rho vsum vmsrc bsrc + weakBaseCoefficientSummed M L cVsum cVm * F jb + w ∧ w ^ 2 ≤ weakDropConstant M L alpha cD delta * iterationDropSum (3 ^ (-alpha)) F n
The summed three-group split at a released threshold pair.