Conditional Rényi divergence #
Main definitions #
FooBar
Main statements #
fooBar_unique
Notation #
Implementation details #
theorem
ProbabilityTheory.integrable_rpow_rnDeriv_compProd_right_iff
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{a : ℝ}
[MeasurableSpace.CountableOrCountablyGenerated α β]
(ha_pos : 0 < a)
(ha_one : a ≠ 1)
(κ : ProbabilityTheory.Kernel α β)
(η : ProbabilityTheory.Kernel α β)
(μ : MeasureTheory.Measure α)
[ProbabilityTheory.IsFiniteKernel κ]
[ProbabilityTheory.IsFiniteKernel η]
[MeasureTheory.IsFiniteMeasure μ]
(h_ac : 1 ≤ a → ∀ᵐ (x : α) ∂μ, (κ x).AbsolutelyContinuous (η x))
:
MeasureTheory.Integrable (fun (x : α × β) => ((μ.compProd κ).rnDeriv (μ.compProd η) x).toReal ^ a) (μ.compProd η) ↔ (∀ᵐ (x : α) ∂μ, MeasureTheory.Integrable (fun (b : β) => ((κ x).rnDeriv (η x) b).toReal ^ a) (η x)) ∧ MeasureTheory.Integrable (fun (x : α) => ∫ (b : β), ((κ x).rnDeriv (η x) b).toReal ^ a ∂η x) μ
noncomputable def
ProbabilityTheory.condRenyiDiv
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
(a : ℝ)
(κ : ProbabilityTheory.Kernel α β)
(η : ProbabilityTheory.Kernel α β)
(μ : MeasureTheory.Measure α)
:
Rényi divergence between two kernels κ and η conditional to a measure μ.
It is defined as Rₐ(κ, η | μ) := Rₐ(μ ⊗ₘ κ, μ ⊗ₘ η).
Equations
- ProbabilityTheory.condRenyiDiv a κ η μ = ProbabilityTheory.renyiDiv a (μ.compProd κ) (μ.compProd η)
Instances For
theorem
ProbabilityTheory.condRenyiDiv_zero
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
(κ : ProbabilityTheory.Kernel α β)
(η : ProbabilityTheory.Kernel α β)
(μ : MeasureTheory.Measure α)
[ProbabilityTheory.IsFiniteKernel κ]
[ProbabilityTheory.IsFiniteKernel η]
[MeasureTheory.IsFiniteMeasure μ]
:
ProbabilityTheory.condRenyiDiv 0 κ η μ = -((μ.compProd η) {x : α × β | 0 < (μ.compProd κ).rnDeriv (μ.compProd η) x}).log
@[simp]
theorem
ProbabilityTheory.condRenyiDiv_one
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
[MeasurableSpace.CountableOrCountablyGenerated α β]
(κ : ProbabilityTheory.Kernel α β)
(η : ProbabilityTheory.Kernel α β)
(μ : MeasureTheory.Measure α)
[ProbabilityTheory.IsFiniteKernel κ]
[∀ (x : α), NeZero (κ x)]
[ProbabilityTheory.IsFiniteKernel η]
[MeasureTheory.IsFiniteMeasure μ]
:
ProbabilityTheory.condRenyiDiv 1 κ η μ = ProbabilityTheory.condKL κ η μ
theorem
ProbabilityTheory.condRenyiDiv_eq_top_iff_of_one_lt
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{a : ℝ}
[MeasurableSpace.CountableOrCountablyGenerated α β]
(ha : 1 < a)
(κ : ProbabilityTheory.Kernel α β)
(η : ProbabilityTheory.Kernel α β)
(μ : MeasureTheory.Measure α)
[ProbabilityTheory.IsFiniteKernel κ]
[ProbabilityTheory.IsFiniteKernel η]
[MeasureTheory.IsFiniteMeasure μ]
:
ProbabilityTheory.condRenyiDiv a κ η μ = ⊤ ↔ (¬∀ᵐ (x : α) ∂μ, MeasureTheory.Integrable (fun (b : β) => ((κ x).rnDeriv (η x) b).toReal ^ a) (η x)) ∨ ¬MeasureTheory.Integrable (fun (x : α) => ∫ (b : β), ((κ x).rnDeriv (η x) b).toReal ^ a ∂η x) μ ∨ ¬∀ᵐ (x : α) ∂μ, (κ x).AbsolutelyContinuous (η x)
theorem
ProbabilityTheory.condRenyiDiv_ne_top_iff_of_one_lt
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{a : ℝ}
[MeasurableSpace.CountableOrCountablyGenerated α β]
(ha : 1 < a)
(κ : ProbabilityTheory.Kernel α β)
(η : ProbabilityTheory.Kernel α β)
(μ : MeasureTheory.Measure α)
[ProbabilityTheory.IsFiniteKernel κ]
[ProbabilityTheory.IsFiniteKernel η]
[MeasureTheory.IsFiniteMeasure μ]
:
ProbabilityTheory.condRenyiDiv a κ η μ ≠ ⊤ ↔ (∀ᵐ (x : α) ∂μ, MeasureTheory.Integrable (fun (b : β) => ((κ x).rnDeriv (η x) b).toReal ^ a) (η x)) ∧ MeasureTheory.Integrable (fun (x : α) => ∫ (b : β), ((κ x).rnDeriv (η x) b).toReal ^ a ∂η x) μ ∧ ∀ᵐ (x : α) ∂μ, (κ x).AbsolutelyContinuous (η x)
theorem
ProbabilityTheory.condRenyiDiv_eq_top_iff_of_lt_one
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{a : ℝ}
[MeasurableSpace.CountableOrCountablyGenerated α β]
(ha_nonneg : 0 ≤ a)
(ha : a < 1)
(κ : ProbabilityTheory.Kernel α β)
(η : ProbabilityTheory.Kernel α β)
(μ : MeasureTheory.Measure α)
[ProbabilityTheory.IsFiniteKernel κ]
[ProbabilityTheory.IsFiniteKernel η]
[MeasureTheory.IsFiniteMeasure μ]
:
ProbabilityTheory.condRenyiDiv a κ η μ = ⊤ ↔ ∀ᵐ (a : α) ∂μ, (κ a).MutuallySingular (η a)
theorem
ProbabilityTheory.condRenyiDiv_of_not_ae_integrable_of_one_lt
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : MeasureTheory.Measure α}
{κ : ProbabilityTheory.Kernel α β}
{η : ProbabilityTheory.Kernel α β}
{a : ℝ}
[MeasurableSpace.CountableOrCountablyGenerated α β]
(ha : 1 < a)
[ProbabilityTheory.IsFiniteKernel κ]
[ProbabilityTheory.IsFiniteKernel η]
[MeasureTheory.IsFiniteMeasure μ]
(h_int : ¬∀ᵐ (x : α) ∂μ, MeasureTheory.Integrable (fun (b : β) => ((κ x).rnDeriv (η x) b).toReal ^ a) (η x))
:
ProbabilityTheory.condRenyiDiv a κ η μ = ⊤
theorem
ProbabilityTheory.condRenyiDiv_of_not_integrable_of_one_lt
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : MeasureTheory.Measure α}
{κ : ProbabilityTheory.Kernel α β}
{η : ProbabilityTheory.Kernel α β}
{a : ℝ}
[MeasurableSpace.CountableOrCountablyGenerated α β]
(ha : 1 < a)
[ProbabilityTheory.IsFiniteKernel κ]
[ProbabilityTheory.IsFiniteKernel η]
[MeasureTheory.IsFiniteMeasure μ]
(h_int : ¬MeasureTheory.Integrable (fun (x : α) => ∫ (b : β), ((κ x).rnDeriv (η x) b).toReal ^ a ∂η x) μ)
:
ProbabilityTheory.condRenyiDiv a κ η μ = ⊤
theorem
ProbabilityTheory.condRenyiDiv_of_not_ac_of_one_lt
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : MeasureTheory.Measure α}
{κ : ProbabilityTheory.Kernel α β}
{η : ProbabilityTheory.Kernel α β}
{a : ℝ}
[MeasurableSpace.CountableOrCountablyGenerated α β]
(ha : 1 < a)
[ProbabilityTheory.IsFiniteKernel κ]
[ProbabilityTheory.IsFiniteKernel η]
[MeasureTheory.IsFiniteMeasure μ]
(h_ac : ¬∀ᵐ (x : α) ∂μ, (κ x).AbsolutelyContinuous (η x))
:
ProbabilityTheory.condRenyiDiv a κ η μ = ⊤
theorem
ProbabilityTheory.condRenyiDiv_of_mutuallySingular_of_lt_one
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : MeasureTheory.Measure α}
{κ : ProbabilityTheory.Kernel α β}
{η : ProbabilityTheory.Kernel α β}
{a : ℝ}
[MeasurableSpace.CountableOrCountablyGenerated α β]
(ha_nonneg : 0 ≤ a)
(ha : a < 1)
[ProbabilityTheory.IsFiniteKernel κ]
[ProbabilityTheory.IsFiniteKernel η]
[MeasureTheory.IsFiniteMeasure μ]
(h_ms : ∀ᵐ (x : α) ∂μ, (κ x).MutuallySingular (η x))
:
ProbabilityTheory.condRenyiDiv a κ η μ = ⊤
theorem
ProbabilityTheory.condRenyiDiv_of_ne_zero
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{a : ℝ}
[MeasurableSpace.CountableOrCountablyGenerated α β]
(ha_nonneg : 0 ≤ a)
(ha_ne_one : a ≠ 1)
(κ : ProbabilityTheory.Kernel α β)
(η : ProbabilityTheory.Kernel α β)
(μ : MeasureTheory.Measure α)
[ProbabilityTheory.IsFiniteKernel κ]
[∀ (x : α), NeZero (κ x)]
[ProbabilityTheory.IsFiniteKernel η]
[MeasureTheory.IsFiniteMeasure μ]
:
ProbabilityTheory.condRenyiDiv a κ η μ = ↑(a - 1)⁻¹ * (↑((μ.compProd η) Set.univ) + (↑a - 1) * ProbabilityTheory.condHellingerDiv a κ η μ).toENNReal.log
theorem
ProbabilityTheory.renyiDiv_comp_left_le
{α : Type u_1}
{mα : MeasurableSpace α}
{a : ℝ}
{β : Type u_4}
{mβ : MeasurableSpace β}
[Nonempty α]
[StandardBorelSpace α]
(ha_pos : 0 < a)
(μ : MeasureTheory.Measure α)
[MeasureTheory.IsFiniteMeasure μ]
(κ : ProbabilityTheory.Kernel α β)
(η : ProbabilityTheory.Kernel α β)
[ProbabilityTheory.IsFiniteKernel κ]
[ProbabilityTheory.IsFiniteKernel η]
:
ProbabilityTheory.renyiDiv a (μ.bind ⇑κ) (μ.bind ⇑η) ≤ ProbabilityTheory.condRenyiDiv a κ η μ