High-contrast homogenization: Provider.Quenched.SmallContrastSplitSupplyAtLevel #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
The hWsplit/hwsq positions at a released threshold pair #
The summed split at the paired exponents with the drop bound read at the
recursion rate, with the bad-event majorant at a free threshold pair. The
pinned form is this at (1 / 2, 1), definitionally.
theorem
HCPolySupport.HighContrast.Quenched.split_at_recursionAlpha_at_level
{d : ℕ}
{M L : ℝ}
{Hw : ℕ}
{V : ℕ → ℝ}
{V0 : ℝ}
{Dr : ℕ → ℝ}
{Vmean : ℝ}
{F : ℕ → ℝ}
{n jb : ℕ}
{vsum cVsum vmsrc cVm bsrc cD delta g bmaj beta lev : ℝ}
(hFmono : ∀ (p q : ℕ), p ≤ q → F q ≤ F p)
(hM0 : 0 ≤ M)
(hg0 : 0 ≤ g)
(hg1 : g < 1)
(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 - contrastRho g) / 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 - contrastRho g / 2) * ↑j) * √(2 * ↑d * Dr j)) + 16 * M / (2 * ((1 - contrastRho g) / 2)) * (√2 * √(L + 1) * Response.profileBadMajorantAt 4 bmaj beta lev + √2 * 3 ^ (-((1 - contrastRho g) / 2) * ↑Hw) * √(L + 1)) + Response.constantSeminormCoefficient * (M * √7 * Vmean) ≤ weakSourceGroupSummed M L (contrastRho g) vsum vmsrc bsrc + weakBaseCoefficientSummed M L cVsum cVm * F jb + w ∧ w ^ 2 ≤ weakDropConstant M L (contrastAlpha g) cD delta * iterationDropSum (3 ^ (-recursionAlpha g)) F n
The hWsplit/hwsq positions at a released threshold pair.