Change of measure inequalities

Main definitions

• FooBar

Main statements

• fooBar_unique

TODO

The lemma names in this file are bad.

theorem ProbabilityTheory.setLIntegral_nnnorm_exp_neg_llr_le {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} [MeasureTheory.SigmaFinite ν] [MeasureTheory.SigmaFinite μ] (hμν : μ.AbsolutelyContinuous ν) (s : Set α) : ∫⁻ (a : α) in s, ↑‖Real.exp (-MeasureTheory.llr μ ν a)‖₊ ∂μ ≤ ν s

theorem ProbabilityTheory.integrableOn_exp_neg_llr {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} {s : Set α} [MeasureTheory.SigmaFinite ν] [MeasureTheory.SigmaFinite μ] (hμν : μ.AbsolutelyContinuous ν) (hνs : ν s ≠ ⊤) : MeasureTheory.IntegrableOn (fun (x : α) => Real.exp (-MeasureTheory.llr μ ν x)) s μ

theorem ProbabilityTheory.setIntegral_exp_neg_llr_le {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} {s : Set α} [MeasureTheory.SigmaFinite ν] [MeasureTheory.SigmaFinite μ] (hμν : μ.AbsolutelyContinuous ν) (hνs : ν s ≠ ⊤) : ∫ (x : α) in s, Real.exp (-MeasureTheory.llr μ ν x) ∂μ ≤ (ν s).toReal

theorem ProbabilityTheory.measure_sub_le_measure_mul_exp {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} [MeasureTheory.SigmaFinite μ] [MeasureTheory.IsFiniteMeasure ν] (hμν : μ.AbsolutelyContinuous ν) (s : Set α) (c : ℝ) (hμc : μ {x : α | c < MeasureTheory.llr μ ν x} ≠ ⊤) : (μ s).toReal - (μ {x : α | c < MeasureTheory.llr μ ν x}).toReal ≤ (ν s).toReal * Real.exp c

theorem ProbabilityTheory.measure_sub_le_measure_mul_exp' {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] (hμν : μ.AbsolutelyContinuous ν) (s : Set α) (c : ℝ) (hμc : μ {x : α | c < MeasureTheory.llr μ ν x} ≠ ⊤) : μ s - μ {x : α | c < MeasureTheory.llr μ ν x} ≤ ν s * ENNReal.ofReal (Real.exp c)

theorem ProbabilityTheory.one_sub_le_add_measure_mul_exp {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} {ν' : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure ν] [MeasureTheory.IsFiniteMeasure ν'] [MeasureTheory.IsProbabilityMeasure μ] (hμν : μ.AbsolutelyContinuous ν) (hμν' : μ.AbsolutelyContinuous ν') (s : Set α) (c : ℝ) (c' : ℝ) : 1 - (μ {x : α | c < MeasureTheory.llr μ ν x}).toReal - (μ {x : α | c' < MeasureTheory.llr μ ν' x}).toReal ≤ (ν s).toReal * Real.exp c + (ν' sᶜ).toReal * Real.exp c'

theorem ProbabilityTheory.one_sub_le_add_measure_mul_exp' {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} {ν' : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure ν] [MeasureTheory.IsFiniteMeasure ν'] [MeasureTheory.IsProbabilityMeasure μ] (hμν : μ.AbsolutelyContinuous ν) (hμν' : μ.AbsolutelyContinuous ν') (s : Set α) (c : ℝ) (c' : ℝ) : 1 - (μ {x : α | c < MeasureTheory.llr μ ν x}).toReal - (μ {x : α | c' < MeasureTheory.llr μ ν' x}).toReal ≤ ((ν s).toReal + (ν' sᶜ).toReal) * Real.exp (max c c')