High-contrast homogenization: Provider.Quenched.SmallContrastWeakValueIsoAtLevel

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

The sharp weak value at a released split level

The parallel copy of weakValueBoundSharpIsotropyAt with the three coefficients the released weak-norm chain produces — the recent group's, the maximum group's and the window tail's — and the bad-event majorant at a free threshold pair. At (16, 16, √2) and (1 / 2, 1) it is the pinned value on the nose.

The second declaration is the metric-factor comparison at the released carriers. It absorbs the released window-tail coefficient into the maximum group's, which is what lets the parametrized base keep its pinned tail: a ctail above √2 is paid for by multiplying the maximum group's coefficient by it, and the bad slot only gains.

noncomputable def HCPolySupport.HighContrast.Quenched.weakValueBoundSharpIsotropyAt {d : ℕ} (cfirst cmax ctail : ℝ) (P : MeasureTheory.Measure (CoeffSpace d)) (m0 h0 : Mat d) (F : BlockMat d) (L : ℝ) (n : Mat d) (rho : ℝ) (Hw : ℕ) (bmaj beta lev : ℝ) (t l : ℤ) (V : ℕ → ℝ) (V0 : ℝ) (Dr : ℕ → ℝ) (Vmean : ℝ) : ℝ

The sharp weak value at a released split level. Three free coefficients and a free threshold pair.

Equations

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

theorem HCPolySupport.HighContrast.Quenched.weakValueBoundSharpIsotropyAt_le_baseIsotropyAtPar_sq {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} {m0 h0 n : Mat d} {Eref : BlockMat d} {cfirst cmax ctail L M rho bmaj beta lev : ℝ} {Hw : ℕ} {t l : ℤ} {V : ℕ → ℝ} {V0 : ℝ} {Dr : ℕ → ℝ} {Vmean : ℝ} (hcfirst : 0 ≤ cfirst) (hcmax : 0 ≤ cmax) (hctail : √2 ≤ ctail) (hrho1 : rho < 1) (hV : ∀ (j : ℕ), 0 ≤ V j) (hV0 : 0 ≤ V0) (hDr : ∀ (j : ℕ), 0 ≤ Dr j) (hVmean : 0 ≤ Vmean) (hbmaj : 0 ≤ bmaj) (hbeta : 0 ≤ beta) (hMF2 : Response.diagonalWeakMetricFactor m0 (Response.skewBlockCongr h0 Eref) ≤ M) (hMFmean : Response.diagonalWeakMetricFactor m0 (Response.skewBlockCongr h0 (adaptedMean P (roundedGrid l n) t)) ≤ M) : weakValueBoundSharpIsotropyAt cfirst cmax ctail P m0 h0 Eref L n rho Hw bmaj beta lev t l V V0 Dr Vmean ≤ weakValueBaseIsotropyAtPar cfirst (cmax * ctail) M L rho Hw bmaj beta lev V V0 Dr Vmean ^ 2

The sharp weak value is monotone in the metric factors, at a released split level. The window tail's coefficient is absorbed into the maximum group's, so the parametrized base is read at its pinned tail.