High-contrast homogenization: Provider.Quenched.StoppingGeneration

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

The generation map of a family of quenched stopping radii

The annealed-to-quenched endgame replaces a family of stopping radii by the number of generations one has to step back from an outer generation before a stopping radius already fits inside the cube of that generation, with a fallback index when no replay succeeds. This file fixes that generation map together with its fallback value and proves the two facts the quantitative estimate needs: below the generation map every admissible offset overshoots, and the event that the generation map is large is either contained in a single overshoot event or empty.

def HCPolySupport.HighContrast.Quenched.IsStoppingCandidate {Ω : Type u_1} (nstar : ℕ) (R : ℕ → Ω → ℝ) (m : ℕ) (ω : Ω) (q : ℕ) : Prop

A candidate offset for the generation map: the offset does not step below the base generation, and the stopping radius at the stepped-back generation already fits inside the cube of the outer generation.

Equations

• HCPolySupport.HighContrast.Quenched.IsStoppingCandidate nstar R m ω q = (q ≤ m - nstar ∧ R (m - q) ω ≤ 3 ^ m)

noncomputable def HCPolySupport.HighContrast.Quenched.stoppingGeneration {Ω : Type u_1} (nstar qfb : ℕ) (R : ℕ → Ω → ℝ) (m : ℕ) (ω : Ω) : ℕ

The generation map N(m): the least candidate offset when one exists, and the fallback offset m - n_* + q_fb otherwise.

Equations

• One or more equations did not get rendered due to their size.

theorem HCPolySupport.HighContrast.Quenched.stoppingGeneration_le {Ω : Type u_1} (nstar qfb : ℕ) (R : ℕ → Ω → ℝ) (m : ℕ) (ω : Ω) : stoppingGeneration nstar qfb R m ω ≤ m - nstar + qfb

The generation map never exceeds its fallback value.

theorem HCPolySupport.HighContrast.Quenched.lt_of_lt_stoppingGeneration {Ω : Type u_1} {nstar qfb : ℕ} {R : ℕ → Ω → ℝ} {m : ℕ} {ω : Ω} {q : ℕ} (hq : q ≤ m - nstar) (hlt : q < stoppingGeneration nstar qfb R m ω) : 3 ^ m < R (m - q) ω

Every admissible offset strictly below the generation map overshoots the cube of the outer generation.

theorem HCPolySupport.HighContrast.Quenched.measureReal_stoppingGeneration_gt_le {Ω : Type u_1} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] {nstar qfb b : ℕ} {R : ℕ → Ω → ℝ} {bnd : ℕ → ℝ} (hbnd : ∀ (q : ℕ), 0 ≤ bnd q) (hR : ∀ (n q : ℕ), nstar ≤ n → P.real {ω : Ω | 3 ^ (n + q + b) < R n ω} ≤ bnd q) (m q : ℕ) : P.real {ω : Ω | q + (qfb + b) < stoppingGeneration nstar qfb R m ω} ≤ bnd q

The shifted upper-tail event of the generation map inherits the overshoot bound of a single stopping radius; beyond the fallback range it is empty.