High-contrast homogenization: Provider.Quenched.SmallContrastWeakValueBasePar

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

The weak base with both group coefficients as parameters

weakValueBaseIsotropyAtPar releases the bad group's threshold pair but leaves both group coefficients pinned at sixteen. That is the wrong interface once the split level moves: the recent group's coefficient and the maximum group's are both functions of the level, and a base whose pinned-level equation is definitional cannot express a coefficient that changes off the pin.

This file carries both as parameters. The two invariants are still rfl: at (16, 16) the parametrized base is weakValueBaseIsotropyAtPar, and at (16, 16, 1/2, 1) it is weakValueBaseIsotropyAtPar.

noncomputable def HCPolySupport.HighContrast.Quenched.weakValueBaseIsotropyAtPar {d : ℕ} (cfirst cmax M L rho : ℝ) (Hw : ℕ) (bmaj beta lev : ℝ) (V : ℕ → ℝ) (V0 : ℝ) (Dr : ℕ → ℝ) (Vmean : ℝ) : ℝ

The metric-free weak base with both group coefficients free.

Equations

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

theorem HCPolySupport.HighContrast.Quenched.weakValueBaseIsotropyAtPar_nonneg {d : ℕ} {cfirst cmax M L rho : ℝ} {Hw : ℕ} {bmaj beta lev : ℝ} {V : ℕ → ℝ} {V0 : ℝ} {Dr : ℕ → ℝ} {Vmean : ℝ} (hcfirst : 0 ≤ cfirst) (hcmax : 0 ≤ cmax) (hM0 : 0 ≤ M) (hrho1 : rho < 1) (hbmaj : 0 ≤ bmaj) (hbeta : 0 ≤ beta) (hV : ∀ (j : ℕ), 0 ≤ V j) (hV0 : 0 ≤ V0) (hDr : ∀ (j : ℕ), 0 ≤ Dr j) (hVmean : 0 ≤ Vmean) : 0 ≤ weakValueBaseIsotropyAtPar cfirst cmax M L rho Hw bmaj beta lev V V0 Dr Vmean

Nonnegativity, at free coefficients.