High-contrast homogenization: Provider.Quenched.NormalizedMinimalScale

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

Normalization of a quenched minimal scale

This file turns the abstract triadic minimal scale into the normalized random mixing scale used by the random-source endgame. In addition to the closed stretched-exponential tail, it retains domination by the same raw scale and the corresponding almost-everywhere all-later certificate.

theorem HCPolySupport.HighContrast.Quenched.exists_normalized_quenchedMinimalScale_of_badTailEvent_bound {Ω : Type u_1} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure P] {N0 : ℕ} {Bad : ℕ → Set Ω} {B eta : ℝ} (hBad : ∀ (n : ℕ), MeasurableSet (Bad n)) (heta : 0 < eta) (hB : 1 ≤ B) (htail : ∀ (N : ℕ), N0 ≤ N → P.real (Book.Ch05.Section57.badTailEvent Bad N) ≤ Real.exp (-(Real.rpow 3 ↑(N - N0) / B) ^ eta)) : ∃ (Rmix : Ω → ℝ), Measurable Rmix ∧ (∀ (ω : Ω), 1 ≤ Rmix ω) ∧ (∀ (t : ℝ), 1 ≤ t → P.real {ω : Ω | 2 * t ≤ Rmix ω} ≤ Real.exp (-t ^ eta)) ∧ (∀ (ω : Ω), Book.Ch05.Section57.quenchedMinimalScale N0 Bad ω ≤ 3 * 3 ^ N0 * B * Rmix ω) ∧ ∀ᵐ (ω : Ω) ∂P, ∀ (m : ℕ), 3 * 3 ^ N0 * B * Rmix ω ≤ 3 ^ m → ω ∉ Bad m

Normalize an abstract triadic minimal scale while retaining its all-later certificate. The factor two converts the closed tail event for the normalized scale into the strict event used by IsBigOWith.