High-contrast homogenization: Provider.Quenched.MinimalScaleMeasurability

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

Measurability of the abstract quenched minimal scale

The abstract Chapter 5 stopping construction supplies the first generation after which no bad event occurs, but its public API does not record measurability. This file proves measurability directly from measurability of the individual bad events. No additional stopping-scale definition is introduced.

theorem HCPolySupport.HighContrast.Quenched.measurableSet_goodTailFrom {Ω : Type u_1} [MeasurableSpace Ω] {Bad : ℕ → Set Ω} (hBad : ∀ (n : ℕ), MeasurableSet (Bad n)) (m : ℕ) : MeasurableSet {ω : Ω | Book.Ch05.Section57.goodTailFrom Bad m ω}

The event that every bad event from a fixed generation onward is absent is measurable when every individual bad event is measurable.

theorem HCPolySupport.HighContrast.Quenched.measurableSet_hasGoodTailFrom {Ω : Type u_1} [MeasurableSpace Ω] {Bad : ℕ → Set Ω} (hBad : ∀ (n : ℕ), MeasurableSet (Bad n)) (n₀ : ℕ) : MeasurableSet {ω : Ω | Book.Ch05.Section57.hasGoodTailFrom n₀ Bad ω}

The event that some generation starts an all-good tail is measurable when every individual bad event is measurable.

theorem HCPolySupport.HighContrast.Quenched.measurable_quenchedMinimalScaleIndex {Ω : Type u_1} [MeasurableSpace Ω] {Bad : ℕ → Set Ω} (hBad : ∀ (n : ℕ), MeasurableSet (Bad n)) (n₀ : ℕ) : Measurable (Book.Ch05.Section57.quenchedMinimalScaleIndex n₀ Bad)

The abstract quenched minimal-scale index is measurable when its bad events are measurable.

theorem HCPolySupport.HighContrast.Quenched.measurable_quenchedMinimalScale {Ω : Type u_1} [MeasurableSpace Ω] {Bad : ℕ → Set Ω} (hBad : ∀ (n : ℕ), MeasurableSet (Bad n)) (n₀ : ℕ) : Measurable (Book.Ch05.Section57.quenchedMinimalScale n₀ Bad)

The abstract triadic quenched minimal scale is measurable when its bad events are measurable.