High-contrast homogenization: Provider.Quenched.SmallContrastSupplyPortsAtLevel #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
The released sharp weak value's drop-family port #
The released value, like the pinned one, reads the drop family only inside the window, so the account may hand the fused core a truncated family and the two agree. The threshold pair and the three coefficients play no part.
theorem
HCPolySupport.HighContrast.Quenched.weakValueBoundSharpIsotropyAt_congr_Dr
{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 Dr' : ℕ → ℝ}
(h : ∀ j ∈ Finset.range (Hw + 1), Dr j = Dr' j)
(Vmean : ℝ)
:
weakValueBoundSharpIsotropyAt cfirst cmax ctail P m0 h0 F L n rho Hw bmaj beta lev t l V V0 Dr Vmean = weakValueBoundSharpIsotropyAt cfirst cmax ctail P m0 h0 F L n rho Hw bmaj beta lev t l V V0 Dr' Vmean
The released sharp weak value depends on the drop family only inside the window.