Documentation

LeanPool.HighContrastHomogenization.Provider.Quenched.SmallContrastSupplyPorts

High-contrast homogenization: Provider.Quenched.SmallContrastSupplyPorts #

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

Supply lemmas at the isotropy carriers #

Three supply lemmas are stated for meanDrop2ValueIsotropy and the isotropic mean-slot conversion, together with the congruence needed by the fused core.

The congruence, and why it is needed. hrec_line_of_slots_isotropy_sharp_at_jb_at_level_src takes hDrnn : ∀ j, 0 ≤ Dr j unconditionally in the lag, while the drop family is nonnegative only where the hatted contrast is monotone, i.e. for t - j at or above the grid base. The two are reconciled without touching either: the weak value depends on Dr only through Finset.range (Hw + 1) (the drop-family congruence below), so the fused core may use the truncated family fun j => Dr (min j n), which is nonnegative everywhere and agrees with the original family on the whole window, since Hw n + 1 ≤ n.

The two families are identified on the finite window by two Finset.sum_congr arguments.

The drop channel at the isotropy carrier #

source
noncomputable def HCPolySupport.HighContrast.Quenched.dropConstantIsotropy {d : ℕ} (cF : ℝ) (E F : BlockMat d) :
ℝ

The drop constant at a parametrized normalizer. The inflation scalar and the normalizing block are explicit parameters.

Equations
Instances For
    source
    theorem HCPolySupport.HighContrast.Quenched.dropConstantIsotropy_nonneg {d : ℕ} {cF : ℝ} (hcF : 0 ≤ cF) {E F : BlockMat d} (hbS : 0 ≤ blockSize E F) :
    0 ≤ dropConstantIsotropy cF E F
    source
    theorem HCPolySupport.HighContrast.Quenched.meanDrop2ValueIsotropy_eq_dropConstantIsotropy_mul {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (lAl : ℤ) (cF : ℝ) (mAl : Mat d) (E F : BlockMat d) (N₀ n j : ℕ) (hj : j ≤ n) :
    meanDrop2ValueIsotropy P lAl cF mAl E F (↑N₀ + ↑n) j = dropConstantIsotropy cF E F * (hatExcess P (roundedGrid lAl mAl) N₀ (n - j) - hatExcess P (roundedGrid lAl mAl) N₀ n)

    The drop cap is an identity, at the isotropy carrier too.

    source
    theorem HCPolySupport.HighContrast.Quenched.hDrdelta_of_floor_isotropy {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 : ℕ) (hj : j ≤ n) :
    meanDrop2ValueIsotropy P lAl cF mAl E F (↑N₀ + ↑n) j ≤ delta

    The hDrdelta inequality at the isotropy carrier follows arithmetically from the preceding identity.

    source
    theorem HCPolySupport.HighContrast.Quenched.meanDrop2ValueIsotropy_nonneg {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (lAl : ℤ) {cF : ℝ} (hcF : 0 ≤ cF) (mAl : Mat d) {E F : BlockMat d} (hbS : 0 ≤ blockSize E F) {N₀ : ℕ} (hFmono : ∀ (p m : ℕ), p ≤ m → hatExcess P (roundedGrid lAl mAl) N₀ m ≤ hatExcess P (roundedGrid lAl mAl) N₀ p) (n j : ℕ) (hj : j ≤ n) :
    0 ≤ meanDrop2ValueIsotropy P lAl cF mAl E F (↑N₀ + ↑n) j

    The drop family is nonnegative where the hatted contrast is monotone.

    The mean slot at the isotropy conversion #

    The lag congruence #

    source
    theorem HCPolySupport.HighContrast.Quenched.truncated_drop_agrees {Dr : ℕ → ℝ} {Hw n : ℕ} (hHw : Hw + 1 ≤ n) (j : ℕ) :
    j ∈ Finset.range (Hw + 1) → Dr (min j n) = Dr j

    The truncated drop family. Nonnegative at every lag, and equal to the one-step family's own on the whole window Finset.range (Hw + 1) whenever Hw + 1 ≤ n.