High-contrast homogenization: Provider.Quenched.SmallContrastEntryRate

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

The entry estimate at a common rate

The three legs of SmallContrastEntryRateParts are put on one decay rate and assembled into the hentry hypothesis of hrec_line_of_slots_isotropy_sharp_at_jb_at_level_src, consumed through the rate-form entry exponent.

The constant. weakSourceGroupSummed is linear with nonnegative coefficients in its three source slots, so the source group evaluated at the three legs' constants is the entry constant:

C_src = entrySourceConstant M L g C_v C_m C_b,

and the entry estimate runs at C_src ^ 2 because the rate-form entry exponent consumes the square.

The rate bookkeeping. Each leg decays at rate beta in a common decay index N, so the square decays at 2·beta. The rate-form entry exponent asks for 3^{-(N₁ + 2·beta·n)}, so the caller must supply N₁ + 2·beta·n ≤ 2·beta·N. With N = n_s + n this is N₁ ≤ 2·beta·n_s: the delayed start must exceed the entry delay inflated by 1/(2·beta), not the entry delay itself. The delayed-start shift is that step.

The source group scales

theorem HCPolySupport.HighContrast.Quenched.weakSourceGroupSummed_le_scaled {M L rho vsum vmsrc bsrc Cv Cm Cb w : ℝ} (hM0 : 0 ≤ M) (hrho1 : rho < 1) (hv : vsum ≤ Cv * w) (hm : vmsrc ≤ Cm * w) (hb : bsrc ≤ Cb * w) : weakSourceGroupSummed M L rho vsum vmsrc bsrc ≤ weakSourceGroupSummed M L rho Cv Cm Cb * w

The source group scales with its three slots. It is linear with nonnegative coefficients in vsum, vmsrc, bsrc.

The entry constant and the squared estimate

The hentry producer

The two established legs at the common rate

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

theorem HCPolySupport.HighContrast.Quenched.vsum_leg_le {d : ℕ} (hd : 2 ≤ d) {Csub Msc delta : ℝ} (hCsub : 0 ≤ Csub) (hMsc : 0 ≤ Msc) (hdelta : 0 ≤ delta) {beta : ℝ} {J N : ℕ} (hrate : beta * ↑N ≤ 1 / 2 * ↑J) : slotVsumSharp d Csub Msc delta J ≤ vsumSourceConstant d Csub Msc delta * 3 ^ (-beta * ↑N)

The variance leg at the common rate. beta·N ≤ J/2 is the rate condition: at J ≈ n/4 and beta = recursionAlpha g ≤ 1/8 it is N ≤ n.