High-contrast homogenization: Provider.Quenched.SmallContrastSourceGroupNonneg

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

The source group is nonnegative at nonnegative legs

Two sign facts the entry-slot clause consumes and that no earlier module needed: the sharp summed source constant is nonnegative, and so is the summed source group at nonnegative legs. Both are immediate from the shapes of their own definitions; they are recorded here so the entry-slot clause discharges them rather than carrying them.

theorem HCPolySupport.HighContrast.Quenched.slotVsumSharp_nonneg (d : ℕ) {Csub Msc delta : ℝ} (hCsub : 0 ≤ Csub) (hMsc : 0 ≤ Msc) (hdelta : 0 ≤ delta) (J : ℕ) : 0 ≤ slotVsumSharp d Csub Msc delta J

The sharp summed source constant is nonnegative.

theorem HCPolySupport.HighContrast.Quenched.weakSourceGroupSummed_nonneg {M L rho vsum vmsrc bsrc : ℝ} (hM : 0 ≤ M) (hrho1 : rho < 1) (hvsum : 0 ≤ vsum) (hvmsrc : 0 ≤ vmsrc) (hbsrc : 0 ≤ bsrc) : 0 ≤ weakSourceGroupSummed M L rho vsum vmsrc bsrc

The summed source group is nonnegative at nonnegative legs.