High-contrast homogenization: Provider.Quenched.SmallContrastSupplyPack

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

The account supply pack

The variance, mean and drop clauses of the isotropic-variance account core body, at the families the one-step family delivers and at the rate pack's window and depth.

The three source constants are defined as their bounds, so the clauses that connect them to the entry slot are le_rfl:

vsum n  := slotVsumSharp d Csub Msc delta (rateDepth n)
vmsrc n := conv * slotSourceSeq d Csub Msc delta (rateDepth n) 0
bsrc n  := the bad expression at (badMomentMajorantScaled …) and rateWindow n
cVsum   := slotCVsum d          cVm := cVmConstant d conv

and the clauses that connect them to the account are's two producers, applied one generation at a time. Nothing here is an estimate; every line is a re-indexing of a bound.

The variance slots

theorem HCPolySupport.HighContrast.Quenched.supply_hVsum {d : ℕ} [NeZero d] (hd : 2 ≤ d) {Csub Msc delta : ℝ} (hCsub : 0 ≤ Csub) (hMsc : 0 ≤ Msc) (hdelta : 0 ≤ delta) {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] {l : ℤ} {q : Mat d} (hgrid : IsRoundedGrid l q) (hfin : ∀ (k : ℤ), HasFiniteAdaptedMean P q k) (N₀ : ℕ) (jb J Hw : ℕ → ℕ) (n : ℕ) : ∑ j ∈ Finset.range (Hw n + 1), 3 ^ (-(1 / 2) * ↑j) * (slotFamilyValue d Csub Msc delta (hatExcess P q N₀ (jb n)) (J n) j + slotFamilyValue d Csub Msc delta (hatExcess P q N₀ (jb n)) (J n) 0) ≤ slotVsumSharp d Csub Msc delta (J n) + slotCVsum d * hatExcess P q N₀ (jb n)

hVsum: the weighted slot sum against the source constant and the base coefficient, one generation at a time.

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

hVmeanle: the mean slot against its own source constant, definitionally.

The drop channel

theorem HCPolySupport.HighContrast.Quenched.supply_hDrnn {d : ℕ} [NeZero d] (P : MeasureTheory.Measure (CoeffSpace d)) [MeasureTheory.IsProbabilityMeasure P] (lAl : ℤ) {cF : ℝ} (hcF : 0 ≤ cF) (mAl : Mat d) {E F : BlockMat d} (hbS : 0 ≤ blockSize E F) (hstat : IsStationaryLaw P) (hgrid : IsRoundedGrid lAl (roundedGrid lAl mAl)) (hfin : ∀ (k : ℤ), HasFiniteAdaptedMean P (roundedGrid lAl mAl) k) {N₀ : ℕ} (hlN : lAl ≤ ↑N₀) (n j : ℕ) : 0 ≤ meanDrop2ValueIsotropy P lAl cF mAl E F (↑N₀ + ↑n) (min j n)

hDrnn, at the truncated family: nonnegative at every lag, which is what hrec_line_of_slots_isotropy_sharp_at_jb_at_level_src demands.

theorem HCPolySupport.HighContrast.Quenched.supply_hDrdelta {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (lAl : ℤ) (cF : ℝ) (mAl : Mat d) (E F : BlockMat d) {N₀ : ℕ} {delta0 delta : ℝ} (hFnn : ∀ (m : ℕ), 0 ≤ hatExcess P (roundedGrid lAl mAl) N₀ m) (hfloor : ∀ (m : ℕ), hatExcess P (roundedGrid lAl mAl) N₀ m ≤ delta0) (hdc0 : 0 ≤ dropConstantIsotropy cF E F) (hchoice : dropConstantIsotropy cF E F * delta0 ≤ delta) (n j : ℕ) : meanDrop2ValueIsotropy P lAl cF mAl E F (↑N₀ + ↑n) (min j n) ≤ delta

hDrdelta, at the truncated family.

theorem HCPolySupport.HighContrast.Quenched.supply_hDrdrop {d : ℕ} [NeZero d] (P : MeasureTheory.Measure (CoeffSpace d)) [MeasureTheory.IsProbabilityMeasure P] (lAl : ℤ) (cF : ℝ) (mAl : Mat d) (E F : BlockMat d) {N₀ : ℕ} {cD : ℝ} (hcD : dropConstantIsotropy cF E F ≤ cD) (hstat : IsStationaryLaw P) (hgrid : IsRoundedGrid lAl (roundedGrid lAl mAl)) (hfin : ∀ (k : ℤ), HasFiniteAdaptedMean P (roundedGrid lAl mAl) k) (hlN : lAl ≤ ↑N₀) (n j : ℕ) (hj : j ≤ n) : meanDrop2ValueIsotropy P lAl cF mAl E F (↑N₀ + ↑n) (min j n) ≤ cD * (hatExcess P (roundedGrid lAl mAl) N₀ (n - j) - hatExcess P (roundedGrid lAl mAl) N₀ n)

hDrdrop, at the truncated family: the cap is the identity of, read at the truncated lag.