High-contrast homogenization: Provider.Quenched.SmallContrastEntryRateMean

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

The mean slot's source, and hentry at named constants

the corresponding argument.1 left one hole: hVmeanle : Vmean ≤ vmsrc + cVm · F j_b was consumed everywhere and produced nowhere. This file closes it from the construction's own mean-slot machinery and instantiates the leg-bound entry estimate so that hentry stands fully discharged at named constants.

Where Vmean comes from. entry_supply_mean_slot_bound_at (the cited theorem) converts the reference-normalized terminal scale variance into the mean-normalized one:

scaleVariance P q (adaptedMean P q t) t ≤ ofReal (meanSlotConversion C_d g m_Al G_acc 𝐄 · V₀),

i.e. Vmean ≤ conv · V₀ with conv = meanSlotConversion …. The slot family already bounds V₀ — it is slotFamilyValue d Csub Msc delta F(j_b) J 0, which is by definition slotSourceSeq … J 0 + slotBaseCoefficient d · F(j_b). So the mean slot splits into a source part and a base part with no new estimate, only the conversion factor:

vmsrc = conv · slotSourceSeq d Csub Msc delta J 0, cVm = conv · slotBaseCoefficient d.

Its decay is the same 3^{-J/2} as the variance leg, because slotSourceSeq … J 0 = slotSourceValue d Csub Msc J.

The hVmeanle hypothesis

theorem HCPolySupport.HighContrast.Quenched.hVmeanle_of_conversion {conv V0 v0src cv0 Fjb Vmean : ℝ} (hconv0 : 0 ≤ conv) (hVmean : Vmean ≤ conv * V0) (hV0 : V0 ≤ v0src + cv0 * Fjb) : Vmean ≤ conv * v0src + conv * cv0 * Fjb

The conversion splits the mean slot. Any bound Vmean ≤ conv · V₀ with V₀ in source-plus-base shape gives hVmeanle's shape.

noncomputable def HCPolySupport.HighContrast.Quenched.cVmConstant (d : ℕ) (conv : ℝ) : ℝ

The mean slot's base coefficient.

Equations

• HCPolySupport.HighContrast.Quenched.cVmConstant d conv = conv * HCPolySupport.HighContrast.Quenched.slotBaseCoefficient d

theorem HCPolySupport.HighContrast.Quenched.hVmeanle_of_slot_family {d : ℕ} {conv Csub Msc delta Fjb Vmean : ℝ} {J : ℕ} (hconv0 : 0 ≤ conv) (hVmean : Vmean ≤ conv * slotFamilyValue d Csub Msc delta Fjb J 0) : Vmean ≤ conv * slotSourceSeq d Csub Msc delta J 0 + cVmConstant d conv * Fjb

hVmeanle at the slot family. The V₀ bound is definitional, so this is the conversion step alone.

The mean leg at the common rate

hentry at the construction's own three constants