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

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

Finite supremum tail bounds without logarithmic scale inflation

The no-loss minimal-scale proof uses finite union bounds directly at the probability level. This avoids first packaging a finite maximum as an O_{\Gamma} random variable with a logarithmic scale factor, which is the source of the non-note-facing exponent loss in the discarded route.

theorem HCPolySupport.Book.Ch05.Section57.finiteSupTail_subset_iUnion {Ω : Type u_1} {ι : Type u_2} {s : Finset ι} (hs : s.Nonempty) {X : ι → Ω → ℝ} {T : ℝ} : {ω : Ω | T < s.sup' hs fun (i : ι) => X i ω} ⊆ ⋃ (i : ↥s), {ω : Ω | T < X (↑i) ω}

A finite supremum tail is contained in the union of the individual tails.

theorem HCPolySupport.Book.Ch05.Section57.measureReal_finiteSupTail_le_sum {Ω : Type u_1} {ι : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {s : Finset ι} (hs : s.Nonempty) {X : ι → Ω → ℝ} {T : ℝ} : μ.real {ω : Ω | T < s.sup' hs fun (i : ι) => X i ω} ≤ ∑ i : ↥s, μ.real {ω : Ω | T < X (↑i) ω}

Union-bound tail estimate for a finite supremum.

theorem HCPolySupport.Book.Ch05.Section57.measureReal_finiteSupTail_le_card_mul {Ω : Type u_1} {ι : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {s : Finset ι} (hs : s.Nonempty) {X : ι → Ω → ℝ} {T R : ℝ} (hR : ∀ i ∈ s, μ.real {ω : Ω | T < X i ω} ≤ R) : μ.real {ω : Ω | T < s.sup' hs fun (i : ι) => X i ω} ≤ ↑s.card * R

Common-tail version of measureReal_finiteSupTail_le_sum.

theorem HCPolySupport.Book.Ch05.Section57.measureReal_finiteSup_sub_const_tail_le_card_mul_exp {Ω : Type u_1} {ι : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {s : Finset ι} (hs : s.Nonempty) {X : ι → Ω → ℝ} {c A lam σ : ℝ} (hlam : 1 ≤ lam) (hX : ∀ i ∈ s, IndependentSums.IsBigOWith μ (IndependentSums.gammaSigma σ) (fun (ω : Ω) => X i ω - c) A) : μ.real {ω : Ω | c + A * lam < s.sup' hs fun (i : ι) => X i ω} ≤ ↑s.card * Real.exp (-lam ^ σ)

A finite supremum of centered Γσ variables has a probability-level union bound with the cardinality as a prefactor. No logarithmic scale factor is introduced.

theorem HCPolySupport.Book.Ch05.Section57.measureReal_finiteSup_tail_le_card_mul_exp_of_isBigO {Ω : Type u_1} {ι : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {s : Finset ι} (hs : s.Nonempty) {X : ι → Ω → ℝ} {A lam σ : ℝ} (hlam : 1 ≤ lam) (hX : ∀ i ∈ s, IndependentSums.IsBigO μ (IndependentSums.gammaSigma σ) (X i) A) : μ.real {ω : Ω | A * lam < s.sup' hs fun (i : ι) => X i ω} ≤ ↑s.card * Real.exp (-lam ^ σ)

Symmetric-tail version of measureReal_finiteSup_sub_const_tail_le_card_mul_exp. It keeps the finite maximum as a probability-level cardinality prefactor.