Coarse-graining support: Support.Book.Ch05.Theorems.Section57.MinimalScaleTail

Imported from the Apache-2.0 CoarseGraining development at commit c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.

Quantitative minimal scale from bad-tail events

This file contains the abstract minimal-scale construction used by Theorem t.homogenization.quenched. The construction is paired with a tail-event inclusion, so the stochastic integrability of the scale is proved from quantitative bounds on badTailEvent.

def HCPolySupport.Book.Ch05.Section57.goodTailFrom {Ω : Type u_1} (Bad : ℕ → Set Ω) (M : ℕ) (ω : Ω) : Prop

Above-scale good event for an abstract family of bad events.

Equations

• HCPolySupport.Book.Ch05.Section57.goodTailFrom Bad M ω = ∀ (K : ℕ), M ≤ K → ω ∉ Bad K

def HCPolySupport.Book.Ch05.Section57.hasGoodTailFrom {Ω : Type u_1} (N0 : ℕ) (Bad : ℕ → Set Ω) (ω : Ω) : Prop

The sample has a deterministic scale, not below N0, above which all bad events are absent.

Equations

• HCPolySupport.Book.Ch05.Section57.hasGoodTailFrom N0 Bad ω = ∃ (M : ℕ), N0 ≤ M ∧ HCPolySupport.Book.Ch05.Section57.goodTailFrom Bad M ω

noncomputable def HCPolySupport.Book.Ch05.Section57.quenchedMinimalScaleIndex {Ω : Type u_1} (N0 : ℕ) (Bad : ℕ → Set Ω) (ω : Ω) : ℕ

The first scale not below N0 above which all bad events are absent. On the exceptional set where no such scale exists, the value is N0; the pointwise estimate is only used on hasGoodTailFrom, while the tail estimate below remains valid for the total function.

Equations

• HCPolySupport.Book.Ch05.Section57.quenchedMinimalScaleIndex N0 Bad ω = if h : HCPolySupport.Book.Ch05.Section57.hasGoodTailFrom N0 Bad ω then Nat.find h else N0

noncomputable def HCPolySupport.Book.Ch05.Section57.quenchedMinimalScale {Ω : Type u_1} (N0 : ℕ) (Bad : ℕ → Set Ω) (ω : Ω) : ℝ

The triadic random minimal scale associated with quenchedMinimalScaleIndex.

Equations

• HCPolySupport.Book.Ch05.Section57.quenchedMinimalScale N0 Bad ω = 3 ^ HCPolySupport.Book.Ch05.Section57.quenchedMinimalScaleIndex N0 Bad ω

theorem HCPolySupport.Book.Ch05.Section57.one_le_quenchedMinimalScale {Ω : Type u_1} (N0 : ℕ) (Bad : ℕ → Set Ω) (ω : Ω) : 1 ≤ quenchedMinimalScale N0 Bad ω

theorem HCPolySupport.Book.Ch05.Section57.quenchedMinimalScaleIndex_spec {Ω : Type u_1} {N0 : ℕ} {Bad : ℕ → Set Ω} {ω : Ω} (hgood : hasGoodTailFrom N0 Bad ω) : N0 ≤ quenchedMinimalScaleIndex N0 Bad ω ∧ goodTailFrom Bad (quenchedMinimalScaleIndex N0 Bad ω) ω

theorem HCPolySupport.Book.Ch05.Section57.quenchedMinimalScaleIndex_le_of_goodTail {Ω : Type u_1} {N0 : ℕ} {Bad : ℕ → Set Ω} {ω : Ω} {M : ℕ} (hN0M : N0 ≤ M) (hM : goodTailFrom Bad M ω) : quenchedMinimalScaleIndex N0 Bad ω ≤ M

theorem HCPolySupport.Book.Ch05.Section57.mem_badTailEvent_of_lt_quenchedMinimalScaleIndex {Ω : Type u_1} {N0 : ℕ} {Bad : ℕ → Set Ω} {ω : Ω} {N : ℕ} (hN0N : N0 ≤ N) (hN : N < quenchedMinimalScaleIndex N0 Bad ω) : ω ∈ badTailEvent Bad N

theorem HCPolySupport.Book.Ch05.Section57.quenchedMinimalScaleIndex_tail_subset_badTailEvent {Ω : Type u_1} {N0 : ℕ} {Bad : ℕ → Set Ω} {N : ℕ} (hN0N : N0 ≤ N) : {ω : Ω | N < quenchedMinimalScaleIndex N0 Bad ω} ⊆ badTailEvent Bad N

theorem HCPolySupport.Book.Ch05.Section57.not_hasGoodTailFrom_subset_badTailEvent {Ω : Type u_1} {N0 : ℕ} {Bad : ℕ → Set Ω} {N : ℕ} (hN0N : N0 ≤ N) : {ω : Ω | ¬hasGoodTailFrom N0 Bad ω} ⊆ badTailEvent Bad N

theorem HCPolySupport.Book.Ch05.Section57.measureReal_not_hasGoodTailFrom_eq_zero {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {N0 : ℕ} {Bad : ℕ → Set Ω} (hsmall : ∀ (ε : ℝ), 0 < ε → ∃ (N : ℕ), N0 ≤ N ∧ μ.real (badTailEvent Bad N) ≤ ε) : μ.real {ω : Ω | ¬hasGoodTailFrom N0 Bad ω} = 0

Quantitative bad-tail bounds imply that the exceptional set with no good tail has measure zero. The hypothesis is deliberately an epsilon formulation: downstream files can supply it from any explicit geometric or stretched-exponential bad-tail estimate.

theorem HCPolySupport.Book.Ch05.Section57.ae_hasGoodTailFrom {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {N0 : ℕ} {Bad : ℕ → Set Ω} (hsmall : ∀ (ε : ℝ), 0 < ε → ∃ (N : ℕ), N0 ≤ N ∧ μ.real (badTailEvent Bad N) ≤ ε) : ∀ᵐ (ω : Ω) ∂μ, hasGoodTailFrom N0 Bad ω

theorem HCPolySupport.Book.Ch05.Section57.rpow_three_log_div_log_eq {x : ℝ} (hx : 0 < x) : Real.rpow 3 (Real.log x / Real.log 3) = x

theorem HCPolySupport.Book.Ch05.Section57.rpow_three_natCeil_log_div_log_le_three_mul {x : ℝ} (hx : 1 ≤ x) : Real.rpow 3 ↑⌈Real.log x / Real.log 3⌉₊ ≤ 3 * x

theorem HCPolySupport.Book.Ch05.Section57.le_rpow_three_natCeil_log_div_log {x : ℝ} (hx : 1 ≤ x) : x ≤ Real.rpow 3 ↑⌈Real.log x / Real.log 3⌉₊

theorem HCPolySupport.Book.Ch05.Section57.isBigOWith_quenchedMinimalScale_of_badTailEvent_bound {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {N0 : ℕ} {Bad : ℕ → Set Ω} {B η : ℝ} (hη_pos : 0 < η) (hB : 1 ≤ B) (htail : ∀ (N : ℕ), N0 ≤ N → μ.real (badTailEvent Bad N) ≤ Real.exp (-(Real.rpow 3 ↑(N - N0) / B) ^ η)) : IndependentSums.IsBigOWith μ (IndependentSums.gammaSigma η) (quenchedMinimalScale N0 Bad) (3 * 3 ^ N0 * B)

Discrete bad-tail bounds imply the continuous Γ_η tail of the triadic minimal scale. The factor 3 is the triadic rounding loss.

theorem HCPolySupport.Book.Ch05.Section57.isBigO_quenchedMinimalScale_of_badTailEvent_bound {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {N0 : ℕ} {Bad : ℕ → Set Ω} {B η : ℝ} (hη_pos : 0 < η) (hB : 1 ≤ B) (htail : ∀ (N : ℕ), N0 ≤ N → μ.real (badTailEvent Bad N) ≤ Real.exp (-(Real.rpow 3 ↑(N - N0) / B) ^ η)) : IndependentSums.IsBigO μ (IndependentSums.gammaSigma η) (quenchedMinimalScale N0 Bad) (3 * 3 ^ N0 * B)

theorem HCPolySupport.Book.Ch05.Section57.not_mem_bad_of_quenchedMinimalScaleIndex_le {Ω : Type u_1} {N0 : ℕ} {Bad : ℕ → Set Ω} {ω : Ω} (hgood : hasGoodTailFrom N0 Bad ω) {N K : ℕ} (hidxN : quenchedMinimalScaleIndex N0 Bad ω ≤ N) (hNK : N ≤ K) : ω ∉ Bad K

theorem HCPolySupport.Book.Ch05.Section57.quenchedMinimalScaleIndex_le_of_scale_le_pow {Ω : Type u_1} {N0 : ℕ} {Bad : ℕ → Set Ω} {ω : Ω} {m : ℕ} (hscale : quenchedMinimalScale N0 Bad ω ≤ 3 ^ m) : quenchedMinimalScaleIndex N0 Bad ω ≤ m

theorem HCPolySupport.Book.Ch05.Section57.rpow_three_div_quenchedMinimalScale_eq_index {Ω : Type u_1} {N0 : ℕ} {Bad : ℕ → Set Ω} {ω : Ω} {m : ℕ} {α : ℝ} (hscale : quenchedMinimalScale N0 Bad ω ≤ 3 ^ m) : (3 ^ m / quenchedMinimalScale N0 Bad ω) ^ (-α) = 3 ^ (-α * ↑(m - quenchedMinimalScaleIndex N0 Bad ω))

theorem HCPolySupport.Book.Ch05.Section57.le_of_not_mem_badScaleEvent {Ω : Type u_1} {H : ℕ → ℕ → Ω → ℝ} {t α : ℝ} {N m n : ℕ} {ω : Ω} (hnot : ω ∉ badScaleEvent H t α N) (hnm : n < m) (hNm : N ≤ m) : 3 ^ (-t * ↑(m - n)) * H m n ω ≤ 3 ^ (-α * ↑(m - N))

theorem HCPolySupport.Book.Ch05.Section57.badScaleEvent_estimate_above_quenchedMinimalScale {Ω : Type u_1} {N0 : ℕ} {H : ℕ → ℕ → Ω → ℝ} {t α : ℝ} {ω : Ω} (hgood : hasGoodTailFrom N0 (badScaleEvent H t α) ω) {m n : ℕ} (hscale : quenchedMinimalScale N0 (badScaleEvent H t α) ω ≤ 3 ^ m) (hnm : n < m) : 3 ^ (-t * ↑(m - n)) * H m n ω ≤ (3 ^ m / quenchedMinimalScale N0 (badScaleEvent H t α) ω) ^ (-α)

Above the constructed scale, absence of the corresponding bad-scale event gives the discounted estimate for the abstract observable H.