Conditional f-divergence #
noncomputable def
ProbabilityTheory.condFDiv
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
(f : ℝ → ℝ)
(κ : ProbabilityTheory.Kernel α β)
(η : ProbabilityTheory.Kernel α β)
(μ : MeasureTheory.Measure α)
:
Conditional f-divergence.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
ProbabilityTheory.condFDiv_of_not_ae_finite
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : MeasureTheory.Measure α}
{κ : ProbabilityTheory.Kernel α β}
{η : ProbabilityTheory.Kernel α β}
{f : ℝ → ℝ}
(h : ¬∀ᵐ (a : α) ∂μ, ProbabilityTheory.fDiv f (κ a) (η a) ≠ ⊤)
:
ProbabilityTheory.condFDiv f κ η μ = ⊤
@[simp]
theorem
ProbabilityTheory.condFDiv_of_not_ae_integrable
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : MeasureTheory.Measure α}
{κ : ProbabilityTheory.Kernel α β}
{η : ProbabilityTheory.Kernel α β}
{f : ℝ → ℝ}
[ProbabilityTheory.IsFiniteKernel κ]
[ProbabilityTheory.IsFiniteKernel η]
(h : ¬∀ᵐ (a : α) ∂μ, MeasureTheory.Integrable (fun (x : β) => f ((κ a).rnDeriv (η a) x).toReal) (η a))
:
ProbabilityTheory.condFDiv f κ η μ = ⊤
@[simp]
theorem
ProbabilityTheory.condFDiv_of_not_ae_ac
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : MeasureTheory.Measure α}
{κ : ProbabilityTheory.Kernel α β}
{η : ProbabilityTheory.Kernel α β}
{f : ℝ → ℝ}
[ProbabilityTheory.IsFiniteKernel κ]
[ProbabilityTheory.IsFiniteKernel η]
(h_top : derivAtTop f = ⊤)
(h : ¬∀ᵐ (a : α) ∂μ, (κ a).AbsolutelyContinuous (η a))
:
ProbabilityTheory.condFDiv f κ η μ = ⊤
@[simp]
theorem
ProbabilityTheory.condFDiv_of_not_integrable
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : MeasureTheory.Measure α}
{κ : ProbabilityTheory.Kernel α β}
{η : ProbabilityTheory.Kernel α β}
{f : ℝ → ℝ}
(hf : ¬MeasureTheory.Integrable (fun (x : α) => (ProbabilityTheory.fDiv f (κ x) (η x)).toReal) μ)
:
ProbabilityTheory.condFDiv f κ η μ = ⊤
@[simp]
theorem
ProbabilityTheory.condFDiv_of_not_integrable'
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : MeasureTheory.Measure α}
{κ : ProbabilityTheory.Kernel α β}
{η : ProbabilityTheory.Kernel α β}
{f : ℝ → ℝ}
[MeasurableSpace.CountableOrCountablyGenerated α β]
[MeasureTheory.IsFiniteMeasure μ]
[ProbabilityTheory.IsFiniteKernel κ]
[ProbabilityTheory.IsFiniteKernel η]
(h_cvx : ConvexOn ℝ (Set.Ici 0) f)
(hf : ¬MeasureTheory.Integrable (fun (a : α) => ∫ (b : β), f ((κ a).rnDeriv (η a) b).toReal ∂η a) μ)
:
ProbabilityTheory.condFDiv f κ η μ = ⊤
theorem
ProbabilityTheory.condFDiv_eq'
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : MeasureTheory.Measure α}
{κ : ProbabilityTheory.Kernel α β}
{η : ProbabilityTheory.Kernel α β}
{f : ℝ → ℝ}
(hf_ae : ∀ᵐ (a : α) ∂μ, ProbabilityTheory.fDiv f (κ a) (η a) ≠ ⊤)
(hf : MeasureTheory.Integrable (fun (x : α) => (ProbabilityTheory.fDiv f (κ x) (η x)).toReal) μ)
:
ProbabilityTheory.condFDiv f κ η μ = ↑(∫ (x : α), (fun (x : α) => (ProbabilityTheory.fDiv f (κ x) (η x)).toReal) x ∂μ)
theorem
ProbabilityTheory.condFDiv_ne_top_iff
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : MeasureTheory.Measure α}
{κ : ProbabilityTheory.Kernel α β}
{η : ProbabilityTheory.Kernel α β}
{f : ℝ → ℝ}
[MeasurableSpace.CountableOrCountablyGenerated α β]
[MeasureTheory.IsFiniteMeasure μ]
[ProbabilityTheory.IsFiniteKernel κ]
[ProbabilityTheory.IsFiniteKernel η]
(h_cvx : ConvexOn ℝ (Set.Ici 0) f)
:
ProbabilityTheory.condFDiv f κ η μ ≠ ⊤ ↔ (∀ᵐ (a : α) ∂μ, MeasureTheory.Integrable (fun (x : β) => f ((κ a).rnDeriv (η a) x).toReal) (η a)) ∧ MeasureTheory.Integrable (fun (a : α) => ∫ (b : β), f ((κ a).rnDeriv (η a) b).toReal ∂η a) μ ∧ (derivAtTop f = ⊤ → ∀ᵐ (a : α) ∂μ, (κ a).AbsolutelyContinuous (η a))
theorem
ProbabilityTheory.condFDiv_eq_top_iff
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : MeasureTheory.Measure α}
{κ : ProbabilityTheory.Kernel α β}
{η : ProbabilityTheory.Kernel α β}
{f : ℝ → ℝ}
[MeasurableSpace.CountableOrCountablyGenerated α β]
[MeasureTheory.IsFiniteMeasure μ]
[ProbabilityTheory.IsFiniteKernel κ]
[ProbabilityTheory.IsFiniteKernel η]
(h_cvx : ConvexOn ℝ (Set.Ici 0) f)
:
ProbabilityTheory.condFDiv f κ η μ = ⊤ ↔ (¬∀ᵐ (a : α) ∂μ, MeasureTheory.Integrable (fun (x : β) => f ((κ a).rnDeriv (η a) x).toReal) (η a)) ∨ ¬MeasureTheory.Integrable (fun (a : α) => ∫ (b : β), f ((κ a).rnDeriv (η a) b).toReal ∂η a) μ ∨ derivAtTop f = ⊤ ∧ ¬∀ᵐ (a : α) ∂μ, (κ a).AbsolutelyContinuous (η a)
theorem
ProbabilityTheory.condFDiv_eq
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : MeasureTheory.Measure α}
{κ : ProbabilityTheory.Kernel α β}
{η : ProbabilityTheory.Kernel α β}
{f : ℝ → ℝ}
[MeasurableSpace.CountableOrCountablyGenerated α β]
[MeasureTheory.IsFiniteMeasure μ]
[ProbabilityTheory.IsFiniteKernel κ]
[ProbabilityTheory.IsFiniteKernel η]
(h_cvx : ConvexOn ℝ (Set.Ici 0) f)
(hf_ae : ∀ᵐ (a : α) ∂μ, MeasureTheory.Integrable (fun (x : β) => f ((κ a).rnDeriv (η a) x).toReal) (η a))
(hf : MeasureTheory.Integrable (fun (a : α) => ∫ (b : β), f ((κ a).rnDeriv (η a) b).toReal ∂η a) μ)
(h_deriv : derivAtTop f = ⊤ → ∀ᵐ (a : α) ∂μ, (κ a).AbsolutelyContinuous (η a))
:
ProbabilityTheory.condFDiv f κ η μ = ↑(∫ (x : α), (fun (x : α) => (ProbabilityTheory.fDiv f (κ x) (η x)).toReal) x ∂μ)
theorem
ProbabilityTheory.condFDiv_ne_top_iff'
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : MeasureTheory.Measure α}
{κ : ProbabilityTheory.Kernel α β}
{η : ProbabilityTheory.Kernel α β}
{f : ℝ → ℝ}
[MeasurableSpace.CountableOrCountablyGenerated α β]
[MeasureTheory.IsFiniteMeasure μ]
[ProbabilityTheory.IsFiniteKernel κ]
[ProbabilityTheory.IsFiniteKernel η]
(h_cvx : ConvexOn ℝ (Set.Ici 0) f)
:
ProbabilityTheory.condFDiv f κ η μ ≠ ⊤ ↔ ProbabilityTheory.condFDiv f κ η μ = ↑(∫ (x : α), (fun (x : α) => (ProbabilityTheory.fDiv f (κ x) (η x)).toReal) x ∂μ)
theorem
ProbabilityTheory.condFDiv_eq_add
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : MeasureTheory.Measure α}
{κ : ProbabilityTheory.Kernel α β}
{η : ProbabilityTheory.Kernel α β}
{f : ℝ → ℝ}
[MeasurableSpace.CountableOrCountablyGenerated α β]
[MeasureTheory.IsFiniteMeasure μ]
[ProbabilityTheory.IsFiniteKernel κ]
[ProbabilityTheory.IsFiniteKernel η]
(h_cvx : ConvexOn ℝ (Set.Ici 0) f)
(hf_ae : ∀ᵐ (a : α) ∂μ, MeasureTheory.Integrable (fun (x : β) => f ((κ a).rnDeriv (η a) x).toReal) (η a))
(hf : MeasureTheory.Integrable (fun (a : α) => ∫ (b : β), f ((κ a).rnDeriv (η a) b).toReal ∂η a) μ)
(h_deriv : derivAtTop f = ⊤ → ∀ᵐ (a : α) ∂μ, (κ a).AbsolutelyContinuous (η a))
:
ProbabilityTheory.condFDiv f κ η μ = ↑(∫ (x : α), (fun (a : α) => ∫ (y : β), f ((κ a).rnDeriv (η a) y).toReal ∂η a) x ∂μ) + ↑(derivAtTop f).toReal * ↑(∫ (x : α), (fun (a : α) => (((κ a).singularPart (η a)) Set.univ).toReal) x ∂μ)
theorem
ProbabilityTheory.condFDiv_of_derivAtTop_eq_top
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : MeasureTheory.Measure α}
{κ : ProbabilityTheory.Kernel α β}
{η : ProbabilityTheory.Kernel α β}
{f : ℝ → ℝ}
[MeasurableSpace.CountableOrCountablyGenerated α β]
[MeasureTheory.IsFiniteMeasure μ]
[ProbabilityTheory.IsFiniteKernel κ]
[ProbabilityTheory.IsFiniteKernel η]
(h_cvx : ConvexOn ℝ (Set.Ici 0) f)
(hf_ae : ∀ᵐ (a : α) ∂μ, MeasureTheory.Integrable (fun (x : β) => f ((κ a).rnDeriv (η a) x).toReal) (η a))
(hf : MeasureTheory.Integrable (fun (a : α) => ∫ (b : β), f ((κ a).rnDeriv (η a) b).toReal ∂η a) μ)
(h_top : derivAtTop f = ⊤)
(h_ac : ∀ᵐ (a : α) ∂μ, (κ a).AbsolutelyContinuous (η a))
:
ProbabilityTheory.condFDiv f κ η μ = ↑(∫ (x : α), (fun (a : α) => ∫ (y : β), f ((κ a).rnDeriv (η a) y).toReal ∂η a) x ∂μ)
@[simp]
theorem
ProbabilityTheory.condFDiv_self
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{f : ℝ → ℝ}
(κ : ProbabilityTheory.Kernel α β)
(μ : MeasureTheory.Measure α)
(hf_one : f 1 = 0)
[ProbabilityTheory.IsFiniteKernel κ]
:
ProbabilityTheory.condFDiv f κ κ μ = 0
@[simp]
theorem
ProbabilityTheory.condFDiv_zero_left
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : MeasureTheory.Measure α}
{η : ProbabilityTheory.Kernel α β}
{f : ℝ → ℝ}
[MeasureTheory.IsFiniteMeasure μ]
[ProbabilityTheory.IsFiniteKernel η]
:
ProbabilityTheory.condFDiv f 0 η μ = ↑(f 0) * ↑(∫ (a : α), ((η a) Set.univ).toReal ∂μ)
theorem
ProbabilityTheory.condFDiv_zero_left'
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : MeasureTheory.Measure α}
{η : ProbabilityTheory.Kernel α β}
{f : ℝ → ℝ}
[MeasureTheory.IsProbabilityMeasure μ]
[ProbabilityTheory.IsMarkovKernel η]
:
ProbabilityTheory.condFDiv f 0 η μ = ↑(f 0)
@[simp]
theorem
ProbabilityTheory.condFDiv_zero_measure
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{κ : ProbabilityTheory.Kernel α β}
{η : ProbabilityTheory.Kernel α β}
{f : ℝ → ℝ}
:
ProbabilityTheory.condFDiv f κ η 0 = 0
@[simp]
theorem
ProbabilityTheory.condFDiv_of_isEmpty_left
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : MeasureTheory.Measure α}
{κ : ProbabilityTheory.Kernel α β}
{η : ProbabilityTheory.Kernel α β}
{f : ℝ → ℝ}
[IsEmpty α]
:
ProbabilityTheory.condFDiv f κ η μ = 0
@[simp]
theorem
ProbabilityTheory.condFDiv_of_isEmpty_right
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : MeasureTheory.Measure α}
{κ : ProbabilityTheory.Kernel α β}
{η : ProbabilityTheory.Kernel α β}
{f : ℝ → ℝ}
[IsEmpty β]
[ProbabilityTheory.IsFiniteKernel κ]
(hf_one : f 1 = 0)
:
ProbabilityTheory.condFDiv f κ η μ = 0
theorem
ProbabilityTheory.condFDiv_ne_bot
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{f : ℝ → ℝ}
(κ : ProbabilityTheory.Kernel α β)
(η : ProbabilityTheory.Kernel α β)
(μ : MeasureTheory.Measure α)
:
ProbabilityTheory.condFDiv f κ η μ ≠ ⊥
theorem
ProbabilityTheory.condFDiv_nonneg
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : MeasureTheory.Measure α}
{κ : ProbabilityTheory.Kernel α β}
{η : ProbabilityTheory.Kernel α β}
{f : ℝ → ℝ}
[ProbabilityTheory.IsMarkovKernel κ]
[ProbabilityTheory.IsMarkovKernel η]
(hf_cvx : ConvexOn ℝ (Set.Ici 0) f)
(hf_cont : ContinuousOn f (Set.Ici 0))
(hf_one : f 1 = 0)
:
0 ≤ ProbabilityTheory.condFDiv f κ η μ
theorem
ProbabilityTheory.condFDiv_const'
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α}
{f : ℝ → ℝ}
{ξ : MeasureTheory.Measure β}
[MeasureTheory.IsFiniteMeasure ξ]
(h_ne_bot : ProbabilityTheory.fDiv f μ ν ≠ ⊥)
:
ProbabilityTheory.condFDiv f (ProbabilityTheory.Kernel.const β μ) (ProbabilityTheory.Kernel.const β ν) ξ = ProbabilityTheory.fDiv f μ ν * ↑(ξ Set.univ)
@[simp]
theorem
ProbabilityTheory.condFDiv_const
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α}
{f : ℝ → ℝ}
{ξ : MeasureTheory.Measure β}
[MeasureTheory.IsFiniteMeasure ξ]
[MeasureTheory.IsFiniteMeasure μ]
(h_cvx : ConvexOn ℝ (Set.Ici 0) f)
:
ProbabilityTheory.condFDiv f (ProbabilityTheory.Kernel.const β μ) (ProbabilityTheory.Kernel.const β ν) ξ = ProbabilityTheory.fDiv f μ ν * ↑(ξ Set.univ)
We show that the integrability of the functions used in fDiv f (μ ⊗ₘ κ) (μ ⊗ₘ η)
and in condFDiv f κ η μ are equivalent.
theorem
ProbabilityTheory.condFDiv_ne_top_iff_fDiv_compProd_ne_top
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : MeasureTheory.Measure α}
{κ : ProbabilityTheory.Kernel α β}
{η : ProbabilityTheory.Kernel α β}
{f : ℝ → ℝ}
[MeasurableSpace.CountableOrCountablyGenerated α β]
[MeasureTheory.IsFiniteMeasure μ]
[ProbabilityTheory.IsFiniteKernel κ]
[∀ (a : α), NeZero (κ a)]
[ProbabilityTheory.IsFiniteKernel η]
(hf : MeasureTheory.StronglyMeasurable f)
(h_cvx : ConvexOn ℝ (Set.Ici 0) f)
:
ProbabilityTheory.condFDiv f κ η μ ≠ ⊤ ↔ ProbabilityTheory.fDiv f (μ.compProd κ) (μ.compProd η) ≠ ⊤
theorem
ProbabilityTheory.condFDiv_eq_top_iff_fDiv_compProd_eq_top
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : MeasureTheory.Measure α}
{κ : ProbabilityTheory.Kernel α β}
{η : ProbabilityTheory.Kernel α β}
{f : ℝ → ℝ}
[MeasurableSpace.CountableOrCountablyGenerated α β]
[MeasureTheory.IsFiniteMeasure μ]
[ProbabilityTheory.IsFiniteKernel κ]
[∀ (a : α), NeZero (κ a)]
[ProbabilityTheory.IsFiniteKernel η]
(hf : MeasureTheory.StronglyMeasurable f)
(h_cvx : ConvexOn ℝ (Set.Ici 0) f)
:
ProbabilityTheory.condFDiv f κ η μ = ⊤ ↔ ProbabilityTheory.fDiv f (μ.compProd κ) (μ.compProd η) = ⊤
theorem
ProbabilityTheory.fDiv_compProd_left
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{f : ℝ → ℝ}
[MeasurableSpace.CountableOrCountablyGenerated α β]
(μ : MeasureTheory.Measure α)
[MeasureTheory.IsFiniteMeasure μ]
(κ : ProbabilityTheory.Kernel α β)
(η : ProbabilityTheory.Kernel α β)
[ProbabilityTheory.IsFiniteKernel κ]
[∀ (a : α), NeZero (κ a)]
[ProbabilityTheory.IsFiniteKernel η]
(hf : MeasureTheory.StronglyMeasurable f)
(h_cvx : ConvexOn ℝ (Set.Ici 0) f)
:
ProbabilityTheory.fDiv f (μ.compProd κ) (μ.compProd η) = ProbabilityTheory.condFDiv f κ η μ
For f-divergences, the divergence between two composition-products with same first measure is equal to the conditional divergence.
theorem
ProbabilityTheory.fDiv_comp_left_le
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{f : ℝ → ℝ}
[Nonempty α]
[StandardBorelSpace α]
[MeasurableSpace.CountableOrCountablyGenerated α β]
(μ : MeasureTheory.Measure α)
[MeasureTheory.IsFiniteMeasure μ]
(κ : ProbabilityTheory.Kernel α β)
(η : ProbabilityTheory.Kernel α β)
[ProbabilityTheory.IsFiniteKernel κ]
[∀ (a : α), NeZero (κ a)]
[ProbabilityTheory.IsFiniteKernel η]
(hf : MeasureTheory.StronglyMeasurable f)
(hf_cvx : ConvexOn ℝ (Set.Ici 0) f)
(hf_cont : ContinuousOn f (Set.Ici 0))
:
ProbabilityTheory.fDiv f (μ.bind ⇑κ) (μ.bind ⇑η) ≤ ProbabilityTheory.condFDiv f κ η μ