OAI/MeasureTheory/DyadicAvoidance/ExposureUnionBound.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem310.ExposureUnionBound.measure_le_of_finite_exposure line 17

   Source documentation

   Averaging conditional bounds over a finite exposure does not introduce a factor for the number of possible exposure values. The event itself need not be measurable, since the proof uses only outer-measure subadditivity.

   theorem measure_le_of_finite_exposure
       {Ω : Type u_Ω} {A : Type u_A} [MeasurableSpace Ω] [Fintype A]
       (μ : Measure Ω) [IsProbabilityMeasure μ]
       (f : Ω → A) (hf : ∀ a, MeasurableSet {ω | f ω = a})
       (E : Set Ω) (good : Set A) (badBound goodBound : ENNReal)
       (hbad : μ {ω | f ω ∉ good} ≤ badBound)
       (hgood : ∀ a ∈ good,
         μ (E ∩ {ω | f ω = a}) ≤ goodBound * μ {ω | f ω = a}) :
       μ E ≤ badBound + goodBound := by
   …

2. theorem OAI.Problem310.ExposureUnionBound.measure_inter_le_of_finite_cover line 54

   Source documentation

   A finite family of trial failures yields a mass-weighted bound on one exposure atom. This formulation avoids dividing by the atom probability.

   theorem measure_inter_le_of_finite_cover
       {Ω : Type u_Ω} {I : Type u_I} [MeasurableSpace Ω]
       (μ : Measure Ω) (E atom : Set Ω) (R : Finset I) (F : I → Set Ω)
       (q : ENNReal)
       (hcover : E ∩ atom ⊆ ⋃ i ∈ R, F i ∩ atom)
       (htrial : ∀ i ∈ R, μ (F i ∩ atom) ≤ q * μ atom) :
       μ (E ∩ atom) ≤ (R.card : ENNReal) * q * μ atom := by
   …

3. theorem OAI.Problem310.ExposureUnionBound.measure_le_two_mul_of_exposure_covers line 72

   Source documentation

   The raw-failure estimate: an exceptional exposure has mass at most p, and on every other exposure a finite union bound has conditional mass at most p. The final estimate is 2*p, irrespective of the number of atoms.

   theorem measure_le_two_mul_of_exposure_covers
       {Ω : Type u_Ω} {A : Type u_A} {I : Type u_I} [MeasurableSpace Ω] [Fintype A]
       (μ : Measure Ω) [IsProbabilityMeasure μ]
       (f : Ω → A) (hf : ∀ a, MeasurableSet {ω | f ω = a})
       (E : Set Ω) (good : Set A) (R : A → Finset I)
       (F : A → I → Set Ω) (q : A → ENNReal) (p : ENNReal)
       (hbad : μ {ω | f ω ∉ good} ≤ p)
       (hcover : ∀ a ∈ good,
         E ∩ {ω | f ω = a} ⊆ ⋃ i ∈ R a, F a i ∩ {ω | f ω = a})
       (htrial : ∀ a ∈ good, ∀ i ∈ R a,
         μ (F a i ∩ {ω | f ω = a}) ≤ q a * μ {ω | f ω = a})
       (hbudget : ∀ a ∈ good, ((R a).card : ENNReal) * q a ≤ p) :
   …