Change of measure inequalities involving Rényi divergences

Main definitions

• FooBar

Main statements

• fooBar_unique

theorem ProbabilityTheory.measure_llr_gt_renyiDiv_le_exp {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] {a : ℝ} (ha : 0 < a) (c : ℝ) (h : ProbabilityTheory.renyiDiv (1 + a) μ ν ≠ ⊤) : (μ {x : α | (ProbabilityTheory.renyiDiv (1 + a) μ ν).toReal + c < MeasureTheory.llr μ ν x}).toReal ≤ Real.exp (-a * c)

theorem ProbabilityTheory.measure_sub_le_measure_mul_exp_renyiDiv {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] (s : Set α) {a : ℝ} (ha : 0 < a) (c : ℝ) (h : ProbabilityTheory.renyiDiv (1 + a) μ ν ≠ ⊤) : (μ s).toReal - Real.exp (-a * c) ≤ (ν s).toReal * Real.exp ((ProbabilityTheory.renyiDiv (1 + a) μ ν).toReal + c)

theorem ProbabilityTheory.one_sub_exp_le_add_measure_mul_exp_max_renyiDiv {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} {ν' : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsFiniteMeasure ν] [MeasureTheory.IsFiniteMeasure ν'] (s : Set α) {a : ℝ} (ha : 0 < a) (c : ℝ) (hν : ProbabilityTheory.renyiDiv (1 + a) μ ν ≠ ⊤) (hν' : ProbabilityTheory.renyiDiv (1 + a) μ ν' ≠ ⊤) : 1 - 2 * Real.exp (-a * c) ≤ ((ν s).toReal + (ν' sᶜ).toReal) * Real.exp (max (ProbabilityTheory.renyiDiv (1 + a) μ ν).toReal (ProbabilityTheory.renyiDiv (1 + a) μ ν').toReal + c)

theorem ProbabilityTheory.exp_neg_max_renyiDiv_le_add_measure {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} {ν' : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsFiniteMeasure ν] [MeasureTheory.IsFiniteMeasure ν'] (s : Set α) {a : ℝ} (ha : 0 < a) (hν : ProbabilityTheory.renyiDiv (1 + a) μ ν ≠ ⊤) (hν' : ProbabilityTheory.renyiDiv (1 + a) μ ν' ≠ ⊤) : 2⁻¹ * Real.exp (-max (ProbabilityTheory.renyiDiv (1 + a) μ ν).toReal (ProbabilityTheory.renyiDiv (1 + a) μ ν').toReal - Real.log 4 / a) ≤ (ν s).toReal + (ν' sᶜ).toReal