f-Divergences

Main definitions

• FooBar

Main statements

• fooBar_unique

Notation

Implementation details

theorem ProbabilityTheory.lintegral_measure_prod_mk_left {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → Set β → ENNReal} (hf : ∀ (a : α), f a ∅ = 0) {s : Set α} (hs : MeasurableSet s) (t : Set β) : ∫⁻ (a : α), f a (Prod.mk a ⁻¹' s ×ˢ t) ∂μ = ∫⁻ (a : α) in s, f a t ∂μ

theorem ProbabilityTheory.setLIntegral_rnDeriv_mul_withDensity {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} [MeasurableSpace.CountableOrCountablyGenerated α β] (μ : MeasureTheory.Measure α) (ν : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] (κ : ProbabilityTheory.Kernel α β) (η : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsFiniteKernel κ] [ProbabilityTheory.IsFiniteKernel η] {s : Set α} (hs : MeasurableSet s) {t : Set β} (ht : MeasurableSet t) : ∫⁻ (a : α) in s, μ.rnDeriv ν a * ((η.withDensity (κ.rnDeriv η)) a) t ∂ν = ((ν.compProd η).withDensity ((μ.compProd κ).rnDeriv (ν.compProd η))) (s ×ˢ t)

theorem ProbabilityTheory.lintegral_rnDeriv_mul_withDensity {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} [MeasurableSpace.CountableOrCountablyGenerated α β] (μ : MeasureTheory.Measure α) (ν : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] (κ : ProbabilityTheory.Kernel α β) (η : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsFiniteKernel κ] [ProbabilityTheory.IsFiniteKernel η] {t : Set β} (ht : MeasurableSet t) : ∫⁻ (a : α), μ.rnDeriv ν a * ((η.withDensity (κ.rnDeriv η)) a) t ∂ν = ((ν.compProd η).withDensity ((μ.compProd κ).rnDeriv (ν.compProd η))) (Set.univ ×ˢ t)

theorem ProbabilityTheory.setLIntegral_rnDeriv_mul_singularPart {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} [MeasurableSpace.CountableOrCountablyGenerated α β] (μ : MeasureTheory.Measure α) (ν : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] (κ : ProbabilityTheory.Kernel α β) (η : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsFiniteKernel κ] [ProbabilityTheory.IsFiniteKernel η] {s : Set α} (hs : MeasurableSet s) {t : Set β} (ht : MeasurableSet t) : ∫⁻ (a : α) in s, μ.rnDeriv ν a * ((κ a).singularPart (η a)) t ∂ν = (((ν.withDensity (μ.rnDeriv ν)).compProd κ).singularPart (ν.compProd η)) (s ×ˢ t)

theorem ProbabilityTheory.lintegral_rnDeriv_mul_singularPart {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} [MeasurableSpace.CountableOrCountablyGenerated α β] (μ : MeasureTheory.Measure α) (ν : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] (κ : ProbabilityTheory.Kernel α β) (η : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsFiniteKernel κ] [ProbabilityTheory.IsFiniteKernel η] {t : Set β} (ht : MeasurableSet t) : ∫⁻ (a : α), μ.rnDeriv ν a * ((κ a).singularPart (η a)) t ∂ν = (((ν.withDensity (μ.rnDeriv ν)).compProd κ).singularPart (ν.compProd η)) (Set.univ ×ˢ t)

theorem ProbabilityTheory.setLIntegral_withDensity {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} [MeasurableSpace.CountableOrCountablyGenerated α β] (μ : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure μ] (κ : ProbabilityTheory.Kernel α β) (η : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsFiniteKernel κ] [ProbabilityTheory.IsFiniteKernel η] {s : Set α} (hs : MeasurableSet s) {t : Set β} (ht : MeasurableSet t) : ∫⁻ (a : α) in s, ((η.withDensity (κ.rnDeriv η)) a) t ∂μ = ((μ.compProd η).withDensity ((μ.compProd κ).rnDeriv (μ.compProd η))) (s ×ˢ t)

theorem ProbabilityTheory.setLIntegral_singularPart {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} [MeasurableSpace.CountableOrCountablyGenerated α β] (μ : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure μ] (κ : ProbabilityTheory.Kernel α β) (η : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsFiniteKernel κ] [ProbabilityTheory.IsFiniteKernel η] {s : Set α} (hs : MeasurableSet s) {t : Set β} (ht : MeasurableSet t) : ∫⁻ (a : α) in s, ((κ a).singularPart (η a)) t ∂μ = ((μ.compProd κ).singularPart (μ.compProd η)) (s ×ˢ t)

theorem ProbabilityTheory.lintegral_withDensity {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} [MeasurableSpace.CountableOrCountablyGenerated α β] (μ : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure μ] (κ : ProbabilityTheory.Kernel α β) (η : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsFiniteKernel κ] [ProbabilityTheory.IsFiniteKernel η] {s : Set β} (hs : MeasurableSet s) : ∫⁻ (a : α), ((η.withDensity (κ.rnDeriv η)) a) s ∂μ = ((μ.compProd η).withDensity ((μ.compProd κ).rnDeriv (μ.compProd η))) (Set.univ ×ˢ s)

theorem ProbabilityTheory.lintegral_singularPart {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} [MeasurableSpace.CountableOrCountablyGenerated α β] (μ : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure μ] (κ : ProbabilityTheory.Kernel α β) (η : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsFiniteKernel κ] [ProbabilityTheory.IsFiniteKernel η] {s : Set β} (hs : MeasurableSet s) : ∫⁻ (a : α), ((κ a).singularPart (η a)) s ∂μ = ((μ.compProd κ).singularPart (μ.compProd η)) (Set.univ ×ˢ s)

theorem ProbabilityTheory.integrable_rnDeriv_mul_withDensity {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} [MeasurableSpace.CountableOrCountablyGenerated α β] (μ : MeasureTheory.Measure α) (ν : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] (κ : ProbabilityTheory.Kernel α β) (η : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsFiniteKernel κ] [ProbabilityTheory.IsFiniteKernel η] : MeasureTheory.Integrable (fun (x : α) => (μ.rnDeriv ν x).toReal * (((η.withDensity (κ.rnDeriv η)) x) Set.univ).toReal) ν

theorem ProbabilityTheory.integrable_rnDeriv_mul_singularPart {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} [MeasurableSpace.CountableOrCountablyGenerated α β] (μ : MeasureTheory.Measure α) (ν : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] (κ : ProbabilityTheory.Kernel α β) (η : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsFiniteKernel κ] [ProbabilityTheory.IsFiniteKernel η] : MeasureTheory.Integrable (fun (x : α) => (μ.rnDeriv ν x).toReal * (((κ x).singularPart (η x)) Set.univ).toReal) ν

theorem ProbabilityTheory.integrable_singularPart {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α} {κ : ProbabilityTheory.Kernel α β} {η : ProbabilityTheory.Kernel α β} [MeasurableSpace.CountableOrCountablyGenerated α β] [MeasureTheory.IsFiniteMeasure μ] [ProbabilityTheory.IsFiniteKernel κ] [ProbabilityTheory.IsFiniteKernel η] : MeasureTheory.Integrable (fun (x : α) => (((κ x).singularPart (η x)) Set.univ).toReal) μ

theorem ProbabilityTheory.setIntegral_rnDeriv_mul_withDensity {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} [MeasurableSpace.CountableOrCountablyGenerated α β] (μ : MeasureTheory.Measure α) (ν : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] (κ : ProbabilityTheory.Kernel α β) (η : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsFiniteKernel κ] [ProbabilityTheory.IsFiniteKernel η] {s : Set α} (hs : MeasurableSet s) {t : Set β} (ht : MeasurableSet t) : ∫ (a : α) in s, (μ.rnDeriv ν a).toReal * (((η.withDensity (κ.rnDeriv η)) a) t).toReal ∂ν = (((ν.compProd η).withDensity ((μ.compProd κ).rnDeriv (ν.compProd η))) (s ×ˢ t)).toReal

theorem ProbabilityTheory.integral_rnDeriv_mul_withDensity {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} [MeasurableSpace.CountableOrCountablyGenerated α β] (μ : MeasureTheory.Measure α) (ν : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] (κ : ProbabilityTheory.Kernel α β) (η : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsFiniteKernel κ] [ProbabilityTheory.IsFiniteKernel η] {t : Set β} (ht : MeasurableSet t) : ∫ (a : α), (μ.rnDeriv ν a).toReal * (((η.withDensity (κ.rnDeriv η)) a) t).toReal ∂ν = (((ν.compProd η).withDensity ((μ.compProd κ).rnDeriv (ν.compProd η))) (Set.univ ×ˢ t)).toReal

theorem ProbabilityTheory.setIntegral_rnDeriv_mul_singularPart {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} [MeasurableSpace.CountableOrCountablyGenerated α β] (μ : MeasureTheory.Measure α) (ν : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] (κ : ProbabilityTheory.Kernel α β) (η : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsFiniteKernel κ] [ProbabilityTheory.IsFiniteKernel η] {s : Set α} (hs : MeasurableSet s) {t : Set β} (ht : MeasurableSet t) : ∫ (a : α) in s, (μ.rnDeriv ν a).toReal * (((κ a).singularPart (η a)) t).toReal ∂ν = ((((ν.withDensity (μ.rnDeriv ν)).compProd κ).singularPart (ν.compProd η)) (s ×ˢ t)).toReal

theorem ProbabilityTheory.integral_rnDeriv_mul_singularPart {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} [MeasurableSpace.CountableOrCountablyGenerated α β] (μ : MeasureTheory.Measure α) (ν : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] (κ : ProbabilityTheory.Kernel α β) (η : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsFiniteKernel κ] [ProbabilityTheory.IsFiniteKernel η] {t : Set β} (ht : MeasurableSet t) : ∫ (a : α), (μ.rnDeriv ν a).toReal * (((κ a).singularPart (η a)) t).toReal ∂ν = ((((ν.withDensity (μ.rnDeriv ν)).compProd κ).singularPart (ν.compProd η)) (Set.univ ×ˢ t)).toReal

theorem ProbabilityTheory.setIntegral_singularPart {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} [MeasurableSpace.CountableOrCountablyGenerated α β] (μ : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure μ] (κ : ProbabilityTheory.Kernel α β) (η : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsFiniteKernel κ] [ProbabilityTheory.IsFiniteKernel η] {s : Set α} (hs : MeasurableSet s) {t : Set β} (ht : MeasurableSet t) : ∫ (a : α) in s, (((κ a).singularPart (η a)) t).toReal ∂μ = (((μ.compProd κ).singularPart (μ.compProd η)) (s ×ˢ t)).toReal

theorem ProbabilityTheory.integral_singularPart {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} [MeasurableSpace.CountableOrCountablyGenerated α β] (μ : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure μ] (κ : ProbabilityTheory.Kernel α β) (η : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsFiniteKernel κ] [ProbabilityTheory.IsFiniteKernel η] {s : Set β} (hs : MeasurableSet s) : ∫ (a : α), (((κ a).singularPart (η a)) s).toReal ∂μ = (((μ.compProd κ).singularPart (μ.compProd η)) (Set.univ ×ˢ s)).toReal

theorem ProbabilityTheory.Integrable.Kernel {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α} {κ : ProbabilityTheory.Kernel α β} [ProbabilityTheory.IsFiniteKernel κ] [MeasureTheory.IsFiniteMeasure μ] (s : Set β) (hs : MeasurableSet s) : MeasureTheory.Integrable (fun (x : α) => ((κ x) s).toReal) μ

theorem ProbabilityTheory.Measure.rnDeriv_measure_compProd_Kernel_withDensity {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} [MeasurableSpace.CountableOrCountablyGenerated α β] (μ : MeasureTheory.Measure α) (ν : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] (κ : ProbabilityTheory.Kernel α β) (η : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsFiniteKernel κ] [ProbabilityTheory.IsFiniteKernel η] : (μ.compProd (η.withDensity (κ.rnDeriv η))).rnDeriv (ν.compProd η) =ᵐ[ν.compProd η] (μ.compProd κ).rnDeriv (ν.compProd η)