High-contrast homogenization: Provider.Quenched.SmallContrastHatDecay

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

The hatted decay hhat

The drive-through from the drop-history recursion to the exact input the corrected tilt transfer consumes.

The iteration decay is stated for an abstract nonincreasing sequence. Here it is instantiated at

F j := d · (hatΘ^q_{N₀ + j} − 1),

whose two structural hypotheses are theorems of the construction (one_le_adaptedHattedContrast_of_rounded for nonnegativity, adaptedHattedContrast_le for monotonicity), and the conclusion is turned into the literal hhat clause of the corrected tilt transfer, at the corrected intermediate scale correctedTiltScale n₀ m = ⌊m/2⌋ + n₀ of the midpoint-scale identity, taken at n₀ := N₀.

The rate κ = α/(320A) and the prefactor B = (12(α+10A)/α)·δ are the iteration lemma's own; the passage n ↦ correctedTiltScale N₀ m costs nothing because ⌊m/2⌋ ≥ correctedTiltScale N₀ m − 2N₀ — the parity defect is absorbed on the exponent side, not in the prefactor.

noncomputable def HCPolySupport.HighContrast.Quenched.hatExcess {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (q : Mat d) (N₀ j : ℕ) : ℝ

The hatted excess sequence based at a generation N₀.

Equations

• HCPolySupport.HighContrast.Quenched.hatExcess P q N₀ j = ↑d * (HCPolySupport.HighContrast.Quenched.adaptedHattedContrast P q (↑N₀ + ↑j) - 1)

theorem HCPolySupport.HighContrast.Quenched.hatExcess_nonneg {d : ℕ} [NeZero d] {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] {l : ℤ} {q : Mat d} (hgrid : IsRoundedGrid l q) (hfin : ∀ (k : ℤ), HasFiniteAdaptedMean P q k) (N₀ j : ℕ) : 0 ≤ hatExcess P q N₀ j

The hatted excess sequence is nonnegative.

theorem HCPolySupport.HighContrast.Quenched.hatExcess_antitone {d : ℕ} [NeZero d] {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] (hstat : IsStationaryLaw P) {l : ℤ} {q : Mat d} (hgrid : IsRoundedGrid l q) (hfin : ∀ (k : ℤ), HasFiniteAdaptedMean P q k) {N₀ : ℕ} (hlN : l ≤ ↑N₀) {p j : ℕ} (hpj : p ≤ j) : hatExcess P q N₀ j ≤ hatExcess P q N₀ p

The hatted excess sequence is nonincreasing.