Conditional Hellinger divergence

Main definitions

• FooBar

Main statements

• fooBar_unique

Notation

Implementation details

theorem ProbabilityTheory.hellingerDiv_ae_ne_top_iff' {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α} {a : ℝ} (κ : ProbabilityTheory.Kernel α β) (η : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsFiniteKernel κ] [ProbabilityTheory.IsFiniteKernel η] : (∀ᵐ (x : α) ∂μ, ProbabilityTheory.hellingerDiv a (κ x) (η x) ≠ ⊤) ↔ (∀ᵐ (x : α) ∂μ, MeasureTheory.Integrable (fun (b : β) => ProbabilityTheory.hellingerFun a ((κ x).rnDeriv (η x) b).toReal) (η x)) ∧ (1 ≤ a → ∀ᵐ (x : α) ∂μ, (κ x).AbsolutelyContinuous (η x))

theorem ProbabilityTheory.hellingerDiv_ae_ne_top_iff {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α} {a : ℝ} (ha_ne_one : a ≠ 1) (κ : ProbabilityTheory.Kernel α β) (η : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsFiniteKernel κ] [ProbabilityTheory.IsFiniteKernel η] : (∀ᵐ (x : α) ∂μ, ProbabilityTheory.hellingerDiv a (κ x) (η x) ≠ ⊤) ↔ (∀ᵐ (x : α) ∂μ, MeasureTheory.Integrable (fun (b : β) => ((κ x).rnDeriv (η x) b).toReal ^ a) (η x)) ∧ (1 ≤ a → ∀ᵐ (x : α) ∂μ, (κ x).AbsolutelyContinuous (η x))

theorem ProbabilityTheory.hellingerDiv_ae_ne_top_iff_of_lt_one' {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α} {a : ℝ} (ha : a < 1) (κ : ProbabilityTheory.Kernel α β) (η : ProbabilityTheory.Kernel α β) : (∀ᵐ (x : α) ∂μ, ProbabilityTheory.hellingerDiv a (κ x) (η x) ≠ ⊤) ↔ ∀ᵐ (x : α) ∂μ, MeasureTheory.Integrable (fun (b : β) => ProbabilityTheory.hellingerFun a ((κ x).rnDeriv (η x) b).toReal) (η x)

theorem ProbabilityTheory.hellingerDiv_ae_ne_top_iff_of_lt_one {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α} {a : ℝ} (ha : a < 1) (κ : ProbabilityTheory.Kernel α β) (η : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsFiniteKernel η] : (∀ᵐ (x : α) ∂μ, ProbabilityTheory.hellingerDiv a (κ x) (η x) ≠ ⊤) ↔ ∀ᵐ (x : α) ∂μ, MeasureTheory.Integrable (fun (b : β) => ((κ x).rnDeriv (η x) b).toReal ^ a) (η x)

theorem ProbabilityTheory.integrable_hellingerDiv_iff {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α} {κ : ProbabilityTheory.Kernel α β} {η : ProbabilityTheory.Kernel α β} {a : ℝ} (h_int : ∀ᵐ (x : α) ∂μ, MeasureTheory.Integrable (fun (b : β) => ProbabilityTheory.hellingerFun a ((κ x).rnDeriv (η x) b).toReal) (η x)) (h_ac : 1 ≤ a → ∀ᵐ (x : α) ∂μ, (κ x).AbsolutelyContinuous (η x)) : MeasureTheory.Integrable (fun (x : α) => (ProbabilityTheory.hellingerDiv a (κ x) (η x)).toReal) μ ↔ MeasureTheory.Integrable (fun (x : α) => ∫ (b : β), ProbabilityTheory.hellingerFun a ((κ x).rnDeriv (η x) b).toReal ∂η x) μ

Use this version only for the case 1 < a or when one of the kernels is not finite, otherwise use integrable_hellingerDiv_iff_of_lt_one, as it is strictly more general.

theorem ProbabilityTheory.integrable_hellingerDiv_iff_of_lt_one {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α} {κ : ProbabilityTheory.Kernel α β} {η : ProbabilityTheory.Kernel α β} {a : ℝ} (ha_nonneg : 0 ≤ a) (ha : a < 1) [ProbabilityTheory.IsFiniteKernel κ] [ProbabilityTheory.IsFiniteKernel η] : MeasureTheory.Integrable (fun (x : α) => (ProbabilityTheory.hellingerDiv a (κ x) (η x)).toReal) μ ↔ MeasureTheory.Integrable (fun (x : α) => ∫ (b : β), ProbabilityTheory.hellingerFun a ((κ x).rnDeriv (η x) b).toReal ∂η x) μ

theorem ProbabilityTheory.integrable_hellingerDiv_iff' {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α} {κ : ProbabilityTheory.Kernel α β} {η : ProbabilityTheory.Kernel α β} {a : ℝ} (ha_pos : 0 < a) (ha_ne_one : a ≠ 1) [MeasureTheory.IsFiniteMeasure μ] [ProbabilityTheory.IsFiniteKernel κ] [ProbabilityTheory.IsFiniteKernel η] (h_int : ∀ᵐ (x : α) ∂μ, MeasureTheory.Integrable (fun (b : β) => ((κ x).rnDeriv (η x) b).toReal ^ a) (η x)) (h_ac : 1 ≤ a → ∀ᵐ (x : α) ∂μ, (κ x).AbsolutelyContinuous (η x)) : MeasureTheory.Integrable (fun (x : α) => (ProbabilityTheory.hellingerDiv a (κ x) (η x)).toReal) μ ↔ MeasureTheory.Integrable (fun (x : α) => ∫ (b : β), ((κ x).rnDeriv (η x) b).toReal ^ a ∂η x) μ

theorem ProbabilityTheory.integrable_hellingerDiv_zero {α : 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 : α) => (ProbabilityTheory.hellingerDiv 0 (κ x) (η x)).toReal) μ

theorem ProbabilityTheory.integrable_hellingerDiv_iff'_of_lt_one {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α} {κ : ProbabilityTheory.Kernel α β} {η : ProbabilityTheory.Kernel α β} {a : ℝ} (ha_pos : 0 < a) (ha : a < 1) [MeasureTheory.IsFiniteMeasure μ] [ProbabilityTheory.IsFiniteKernel κ] [ProbabilityTheory.IsFiniteKernel η] : MeasureTheory.Integrable (fun (x : α) => (ProbabilityTheory.hellingerDiv a (κ x) (η x)).toReal) μ ↔ MeasureTheory.Integrable (fun (x : α) => ∫ (b : β), ((κ x).rnDeriv (η x) b).toReal ^ a ∂η x) μ

noncomputable def ProbabilityTheory.condHellingerDiv {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (a : ℝ) (κ : ProbabilityTheory.Kernel α β) (η : ProbabilityTheory.Kernel α β) (μ : MeasureTheory.Measure α) : EReal

Conditional Hellinger divergence of order a.

Equations

• ProbabilityTheory.condHellingerDiv a κ η μ = ProbabilityTheory.condFDiv (ProbabilityTheory.hellingerFun a) κ η μ

There are multiple combinations of hypotheses that give rise to slightly different versions of the following lemmas. The ones we will consider as a normal form are when we assume that μ, κ and η are all finite and a ∈ (0, 1) ∪ (1, +∞).

Consider the following conditions:

1. condHellingerDiv a κ η μ ≠ ⊤
2. condHellingerDiv a κ η μ = ∫ x, (hellingerDiv a (κ x) (η x)).toReal ∂μ 3.a ∀ᵐ x ∂μ, Integrable (fun b ↦ ((∂κ x/∂η x) b).toReal ^ a) (η x) (h_int) 3.b ∀ᵐ x ∂μ, (κ x) ≪ (η x) (h_ac) 3.c Integrable (fun x ↦ ∫ b, ((∂κ x/∂η x) b).toReal ^ a ∂η x) μ (h_int')
3. condHellingerDiv a κ η μ = (a - 1)⁻¹ * ∫ x, ∫ b, ((∂κ x/∂η x) b).toReal ^ a ∂η x ∂μ - (a - 1)⁻¹ * ((μ ⊗ₘ η) .univ).toReal

Then the following hold:

• 1. ↔ 2. (condHellingerDiv_eq_integral_iff_ne_top)
• if 1 < a:
  • 1. ↔ 3.a ∧ 3.b ∧ 3.c (condHellingerDiv_ne_top_iff_of_one_lt)
  • 2. ↔ 3.a ∧ 3.b ∧ 3.c (condHellingerDiv_eq_integral_iff_of_one_lt)
  • 3.a ∧ 3.b ∧ 3.c → 4. (condHellingerDiv_eq_integral'_of_one_lt)
• if a < 1:
  • 1. ↔ 3.c (condHellingerDiv_ne_top_iff_of_lt_one')
  • 2. ↔ 3.c (condHellingerDiv_eq_integral_iff_of_lt_one)
  • 3.c → 4. (condHellingerDiv_eq_integral'_of_lt_one)

The implications 4. → 1./2./3. are not explicitely stated but, if needed, it should be immediate to prove 4. → 1. and then have all the other implications for free.

theorem ProbabilityTheory.condHellingerDiv_one {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α} {κ : ProbabilityTheory.Kernel α β} {η : ProbabilityTheory.Kernel α β} [ProbabilityTheory.IsFiniteKernel κ] [ProbabilityTheory.IsFiniteKernel η] : ProbabilityTheory.condHellingerDiv 1 κ η μ = ProbabilityTheory.condKL κ η μ

theorem ProbabilityTheory.condHellingerDiv_of_not_ae_finite {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α} {κ : ProbabilityTheory.Kernel α β} {η : ProbabilityTheory.Kernel α β} {a : ℝ} (h_ae : ¬∀ᵐ (x : α) ∂μ, ProbabilityTheory.hellingerDiv a (κ x) (η x) ≠ ⊤) : ProbabilityTheory.condHellingerDiv a κ η μ = ⊤

theorem ProbabilityTheory.condHellingerDiv_of_not_ae_integrable' {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α} {κ : ProbabilityTheory.Kernel α β} {η : ProbabilityTheory.Kernel α β} {a : ℝ} [ProbabilityTheory.IsFiniteKernel κ] [ProbabilityTheory.IsFiniteKernel η] (h_int : ¬∀ᵐ (x : α) ∂μ, MeasureTheory.Integrable (fun (b : β) => ProbabilityTheory.hellingerFun a ((κ x).rnDeriv (η x) b).toReal) (η x)) : ProbabilityTheory.condHellingerDiv a κ η μ = ⊤

theorem ProbabilityTheory.condHellingerDiv_of_not_ae_integrable {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α} {κ : ProbabilityTheory.Kernel α β} {η : ProbabilityTheory.Kernel α β} {a : ℝ} (ha_ne_one : a ≠ 1) [ProbabilityTheory.IsFiniteKernel κ] [ProbabilityTheory.IsFiniteKernel η] (h_int : ¬∀ᵐ (x : α) ∂μ, MeasureTheory.Integrable (fun (b : β) => ((κ x).rnDeriv (η x) b).toReal ^ a) (η x)) : ProbabilityTheory.condHellingerDiv a κ η μ = ⊤

theorem ProbabilityTheory.condHellingerDiv_of_not_ae_integrable_of_lt_one {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α} {κ : ProbabilityTheory.Kernel α β} {η : ProbabilityTheory.Kernel α β} {a : ℝ} (ha : a < 1) (h_int : ¬∀ᵐ (x : α) ∂μ, MeasureTheory.Integrable (fun (b : β) => ProbabilityTheory.hellingerFun a ((κ x).rnDeriv (η x) b).toReal) (η x)) : ProbabilityTheory.condHellingerDiv a κ η μ = ⊤

theorem ProbabilityTheory.condHellingerDiv_of_not_ae_ac_of_one_le {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α} {κ : ProbabilityTheory.Kernel α β} {η : ProbabilityTheory.Kernel α β} {a : ℝ} (ha : 1 ≤ a) [ProbabilityTheory.IsFiniteKernel κ] [ProbabilityTheory.IsFiniteKernel η] (h_ac : ¬∀ᵐ (x : α) ∂μ, (κ x).AbsolutelyContinuous (η x)) : ProbabilityTheory.condHellingerDiv a κ η μ = ⊤

theorem ProbabilityTheory.condHellingerDiv_of_not_integrable {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α} {κ : ProbabilityTheory.Kernel α β} {η : ProbabilityTheory.Kernel α β} {a : ℝ} (h_int : ¬MeasureTheory.Integrable (fun (x : α) => (ProbabilityTheory.hellingerDiv a (κ x) (η x)).toReal) μ) : ProbabilityTheory.condHellingerDiv a κ η μ = ⊤

theorem ProbabilityTheory.condHellingerDiv_of_not_integrable' {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α} {κ : ProbabilityTheory.Kernel α β} {η : ProbabilityTheory.Kernel α β} {a : ℝ} (ha_nonneg : 0 ≤ a) (ha_ne_one : a ≠ 1) [MeasureTheory.IsFiniteMeasure μ] [ProbabilityTheory.IsFiniteKernel κ] [ProbabilityTheory.IsFiniteKernel η] (h_int' : ¬MeasureTheory.Integrable (fun (x : α) => ∫ (b : β), ((κ x).rnDeriv (η x) b).toReal ^ a ∂η x) μ) : ProbabilityTheory.condHellingerDiv a κ η μ = ⊤

theorem ProbabilityTheory.condHellingerDiv_of_ae_finite_of_integrable {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α} {κ : ProbabilityTheory.Kernel α β} {η : ProbabilityTheory.Kernel α β} {a : ℝ} (h_ae : ∀ᵐ (x : α) ∂μ, ProbabilityTheory.hellingerDiv a (κ x) (η x) ≠ ⊤) (h_int2 : MeasureTheory.Integrable (fun (x : α) => (ProbabilityTheory.hellingerDiv a (κ x) (η x)).toReal) μ) : ProbabilityTheory.condHellingerDiv a κ η μ = ↑(∫ (x : α), (ProbabilityTheory.hellingerDiv a (κ x) (η x)).toReal ∂μ)

theorem ProbabilityTheory.condHellingerDiv_of_ae_integrable_of_ae_ac_of_integrable {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α} {κ : ProbabilityTheory.Kernel α β} {η : ProbabilityTheory.Kernel α β} {a : ℝ} [ProbabilityTheory.IsFiniteKernel κ] [ProbabilityTheory.IsFiniteKernel η] (h_int : ∀ᵐ (x : α) ∂μ, MeasureTheory.Integrable (fun (b : β) => ProbabilityTheory.hellingerFun a ((κ x).rnDeriv (η x) b).toReal) (η x)) (h_ac : 1 ≤ a → ∀ᵐ (x : α) ∂μ, (κ x).AbsolutelyContinuous (η x)) (h_int2 : MeasureTheory.Integrable (fun (x : α) => (ProbabilityTheory.hellingerDiv a (κ x) (η x)).toReal) μ) : ProbabilityTheory.condHellingerDiv a κ η μ = ↑(∫ (x : α), (ProbabilityTheory.hellingerDiv a (κ x) (η x)).toReal ∂μ)

theorem ProbabilityTheory.condHellingerDiv_zero_eq {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α} {κ : ProbabilityTheory.Kernel α β} {η : ProbabilityTheory.Kernel α β} [MeasurableSpace.CountableOrCountablyGenerated α β] [MeasureTheory.IsFiniteMeasure μ] [ProbabilityTheory.IsFiniteKernel κ] [ProbabilityTheory.IsFiniteKernel η] : ProbabilityTheory.condHellingerDiv 0 κ η μ = ↑(∫ (x : α), (ProbabilityTheory.hellingerDiv 0 (κ x) (η x)).toReal ∂μ)

theorem ProbabilityTheory.condHellingerDiv_zero_of_ae_integrable_of_integrable {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α} {κ : ProbabilityTheory.Kernel α β} {η : ProbabilityTheory.Kernel α β} [ProbabilityTheory.IsFiniteKernel κ] [ProbabilityTheory.IsFiniteKernel η] (h_int2 : MeasureTheory.Integrable (fun (x : α) => (ProbabilityTheory.hellingerDiv 0 (κ x) (η x)).toReal) μ) : ProbabilityTheory.condHellingerDiv 0 κ η μ = ↑(∫ (x : α), (ProbabilityTheory.hellingerDiv 0 (κ x) (η x)).toReal ∂μ)

theorem ProbabilityTheory.condHellingerDiv_of_ae_integrable_of_ae_ac_of_integrable' {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α} {κ : ProbabilityTheory.Kernel α β} {η : ProbabilityTheory.Kernel α β} {a : ℝ} (ha_pos : 0 < a) (ha_ne_one : a ≠ 1) [MeasureTheory.IsFiniteMeasure μ] [ProbabilityTheory.IsFiniteKernel κ] [ProbabilityTheory.IsFiniteKernel η] (h_int : ∀ᵐ (x : α) ∂μ, MeasureTheory.Integrable (fun (b : β) => ((κ x).rnDeriv (η x) b).toReal ^ a) (η x)) (h_ac : 1 ≤ a → ∀ᵐ (x : α) ∂μ, (κ x).AbsolutelyContinuous (η x)) (h_int' : MeasureTheory.Integrable (fun (x : α) => ∫ (b : β), ((κ x).rnDeriv (η x) b).toReal ^ a ∂η x) μ) : ProbabilityTheory.condHellingerDiv a κ η μ = ↑(∫ (x : α), (ProbabilityTheory.hellingerDiv a (κ x) (η x)).toReal ∂μ)

theorem ProbabilityTheory.condHellingerDiv_of_ae_integrable_of_integrable_of_lt_one {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α} {κ : ProbabilityTheory.Kernel α β} {η : ProbabilityTheory.Kernel α β} {a : ℝ} (ha : a < 1) [ProbabilityTheory.IsFiniteKernel η] (h_int : ∀ᵐ (x : α) ∂μ, MeasureTheory.Integrable (fun (b : β) => ((κ x).rnDeriv (η x) b).toReal ^ a) (η x)) (h_int2 : MeasureTheory.Integrable (fun (x : α) => (ProbabilityTheory.hellingerDiv a (κ x) (η x)).toReal) μ) : ProbabilityTheory.condHellingerDiv a κ η μ = ↑(∫ (x : α), (ProbabilityTheory.hellingerDiv a (κ x) (η x)).toReal ∂μ)

theorem ProbabilityTheory.condHellingerDiv_of_integrable'_of_lt_one {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α} {κ : ProbabilityTheory.Kernel α β} {η : ProbabilityTheory.Kernel α β} {a : ℝ} (ha_pos : 0 < a) (ha : a < 1) [MeasureTheory.IsFiniteMeasure μ] [ProbabilityTheory.IsFiniteKernel κ] [ProbabilityTheory.IsFiniteKernel η] (h_int' : MeasureTheory.Integrable (fun (x : α) => ∫ (b : β), ((κ x).rnDeriv (η x) b).toReal ^ a ∂η x) μ) : ProbabilityTheory.condHellingerDiv a κ η μ = ↑(∫ (x : α), (ProbabilityTheory.hellingerDiv a (κ x) (η x)).toReal ∂μ)

theorem ProbabilityTheory.condHellingerDiv_eq_top_iff {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α} {κ : ProbabilityTheory.Kernel α β} {η : ProbabilityTheory.Kernel α β} {a : ℝ} [ProbabilityTheory.IsFiniteKernel κ] [ProbabilityTheory.IsFiniteKernel η] : ProbabilityTheory.condHellingerDiv a κ η μ = ⊤ ↔ (¬∀ᵐ (x : α) ∂μ, MeasureTheory.Integrable (fun (b : β) => ProbabilityTheory.hellingerFun a ((κ x).rnDeriv (η x) b).toReal) (η x)) ∨ (1 ≤ a ∧ ¬∀ᵐ (x : α) ∂μ, (κ x).AbsolutelyContinuous (η x)) ∨ ¬MeasureTheory.Integrable (fun (x : α) => (ProbabilityTheory.hellingerDiv a (κ x) (η x)).toReal) μ

theorem ProbabilityTheory.condHellingerDiv_ne_top_iff {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α} {κ : ProbabilityTheory.Kernel α β} {η : ProbabilityTheory.Kernel α β} {a : ℝ} [ProbabilityTheory.IsFiniteKernel κ] [ProbabilityTheory.IsFiniteKernel η] : ProbabilityTheory.condHellingerDiv a κ η μ ≠ ⊤ ↔ (∀ᵐ (x : α) ∂μ, MeasureTheory.Integrable (fun (b : β) => ProbabilityTheory.hellingerFun a ((κ x).rnDeriv (η x) b).toReal) (η x)) ∧ (1 ≤ a → ∀ᵐ (x : α) ∂μ, (κ x).AbsolutelyContinuous (η x)) ∧ MeasureTheory.Integrable (fun (x : α) => (ProbabilityTheory.hellingerDiv a (κ x) (η x)).toReal) μ

theorem ProbabilityTheory.condHellingerDiv_ne_top_iff' {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α} {κ : ProbabilityTheory.Kernel α β} {η : ProbabilityTheory.Kernel α β} {a : ℝ} (ha_pos : 0 < a) (ha_ne_one : a ≠ 1) [MeasureTheory.IsFiniteMeasure μ] [ProbabilityTheory.IsFiniteKernel κ] [ProbabilityTheory.IsFiniteKernel η] : ProbabilityTheory.condHellingerDiv a κ η μ ≠ ⊤ ↔ (∀ᵐ (x : α) ∂μ, MeasureTheory.Integrable (fun (b : β) => ((κ x).rnDeriv (η x) b).toReal ^ a) (η x)) ∧ (1 ≤ a → ∀ᵐ (x : α) ∂μ, (κ x).AbsolutelyContinuous (η x)) ∧ MeasureTheory.Integrable (fun (x : α) => ∫ (b : β), ((κ x).rnDeriv (η x) b).toReal ^ a ∂η x) μ

theorem ProbabilityTheory.condHellingerDiv_eq_top_iff' {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α} {κ : ProbabilityTheory.Kernel α β} {η : ProbabilityTheory.Kernel α β} {a : ℝ} (ha_pos : 0 < a) (ha_ne_one : a ≠ 1) [MeasureTheory.IsFiniteMeasure μ] [ProbabilityTheory.IsFiniteKernel κ] [ProbabilityTheory.IsFiniteKernel η] : ProbabilityTheory.condHellingerDiv a κ η μ = ⊤ ↔ (¬∀ᵐ (x : α) ∂μ, MeasureTheory.Integrable (fun (b : β) => ((κ x).rnDeriv (η x) b).toReal ^ a) (η x)) ∨ (1 ≤ a ∧ ¬∀ᵐ (x : α) ∂μ, (κ x).AbsolutelyContinuous (η x)) ∨ ¬MeasureTheory.Integrable (fun (x : α) => ∫ (b : β), ((κ x).rnDeriv (η x) b).toReal ^ a ∂η x) μ

theorem ProbabilityTheory.condHellingerDiv_ne_top_iff_of_one_lt {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α} {κ : ProbabilityTheory.Kernel α β} {η : ProbabilityTheory.Kernel α β} {a : ℝ} (ha : 1 < a) [MeasureTheory.IsFiniteMeasure μ] [ProbabilityTheory.IsFiniteKernel κ] [ProbabilityTheory.IsFiniteKernel η] : ProbabilityTheory.condHellingerDiv a κ η μ ≠ ⊤ ↔ (∀ᵐ (x : α) ∂μ, MeasureTheory.Integrable (fun (b : β) => ((κ x).rnDeriv (η x) b).toReal ^ a) (η x)) ∧ (∀ᵐ (x : α) ∂μ, (κ x).AbsolutelyContinuous (η x)) ∧ MeasureTheory.Integrable (fun (x : α) => ∫ (b : β), ((κ x).rnDeriv (η x) b).toReal ^ a ∂η x) μ

theorem ProbabilityTheory.condHellingerDiv_eq_top_iff_of_one_lt {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α} {κ : ProbabilityTheory.Kernel α β} {η : ProbabilityTheory.Kernel α β} {a : ℝ} (ha : 1 < a) [MeasureTheory.IsFiniteMeasure μ] [ProbabilityTheory.IsFiniteKernel κ] [ProbabilityTheory.IsFiniteKernel η] : ProbabilityTheory.condHellingerDiv a κ η μ = ⊤ ↔ (¬∀ᵐ (x : α) ∂μ, MeasureTheory.Integrable (fun (b : β) => ((κ x).rnDeriv (η x) b).toReal ^ a) (η x)) ∨ (1 ≤ a ∧ ¬∀ᵐ (x : α) ∂μ, (κ x).AbsolutelyContinuous (η x)) ∨ ¬MeasureTheory.Integrable (fun (x : α) => ∫ (b : β), ((κ x).rnDeriv (η x) b).toReal ^ a ∂η x) μ

theorem ProbabilityTheory.condHellingerDiv_eq_top_iff_of_lt_one {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α} {κ : ProbabilityTheory.Kernel α β} {η : ProbabilityTheory.Kernel α β} {a : ℝ} (ha : a < 1) [ProbabilityTheory.IsFiniteKernel κ] [ProbabilityTheory.IsFiniteKernel η] : ProbabilityTheory.condHellingerDiv a κ η μ = ⊤ ↔ (¬∀ᵐ (x : α) ∂μ, MeasureTheory.Integrable (fun (b : β) => ProbabilityTheory.hellingerFun a ((κ x).rnDeriv (η x) b).toReal) (η x)) ∨ ¬MeasureTheory.Integrable (fun (x : α) => (ProbabilityTheory.hellingerDiv a (κ x) (η x)).toReal) μ

theorem ProbabilityTheory.condHellingerDiv_ne_top_iff_of_lt_one {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α} {κ : ProbabilityTheory.Kernel α β} {η : ProbabilityTheory.Kernel α β} {a : ℝ} (ha : a < 1) [ProbabilityTheory.IsFiniteKernel κ] [ProbabilityTheory.IsFiniteKernel η] : ProbabilityTheory.condHellingerDiv a κ η μ ≠ ⊤ ↔ (∀ᵐ (x : α) ∂μ, MeasureTheory.Integrable (fun (b : β) => ProbabilityTheory.hellingerFun a ((κ x).rnDeriv (η x) b).toReal) (η x)) ∧ MeasureTheory.Integrable (fun (x : α) => (ProbabilityTheory.hellingerDiv a (κ x) (η x)).toReal) μ

theorem ProbabilityTheory.condHellingerDiv_eq_top_iff_of_lt_one' {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α} {κ : ProbabilityTheory.Kernel α β} {η : ProbabilityTheory.Kernel α β} {a : ℝ} (ha_pos : 0 < a) (ha : a < 1) [MeasureTheory.IsFiniteMeasure μ] [ProbabilityTheory.IsFiniteKernel κ] [ProbabilityTheory.IsFiniteKernel η] : ProbabilityTheory.condHellingerDiv a κ η μ = ⊤ ↔ ¬MeasureTheory.Integrable (fun (x : α) => ∫ (b : β), ((κ x).rnDeriv (η x) b).toReal ^ a ∂η x) μ

theorem ProbabilityTheory.condHellingerDiv_ne_top_iff_of_lt_one' {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α} {κ : ProbabilityTheory.Kernel α β} {η : ProbabilityTheory.Kernel α β} {a : ℝ} (ha_pos : 0 < a) (ha : a < 1) [MeasureTheory.IsFiniteMeasure μ] [ProbabilityTheory.IsFiniteKernel κ] [ProbabilityTheory.IsFiniteKernel η] : ProbabilityTheory.condHellingerDiv a κ η μ ≠ ⊤ ↔ MeasureTheory.Integrable (fun (x : α) => ∫ (b : β), ((κ x).rnDeriv (η x) b).toReal ^ a ∂η x) μ

theorem ProbabilityTheory.condHellingerDiv_eq_integral_iff_ne_top {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α} {κ : ProbabilityTheory.Kernel α β} {η : ProbabilityTheory.Kernel α β} {a : ℝ} (ha_pos : 0 < a) (ha_ne_one : a ≠ 1) [MeasureTheory.IsFiniteMeasure μ] [ProbabilityTheory.IsFiniteKernel κ] [ProbabilityTheory.IsFiniteKernel η] : ProbabilityTheory.condHellingerDiv a κ η μ ≠ ⊤ ↔ ProbabilityTheory.condHellingerDiv a κ η μ = ↑(∫ (x : α), (ProbabilityTheory.hellingerDiv a (κ x) (η x)).toReal ∂μ)

theorem ProbabilityTheory.condHellingerDiv_eq_integral_iff_of_one_lt {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α} {κ : ProbabilityTheory.Kernel α β} {η : ProbabilityTheory.Kernel α β} {a : ℝ} (ha : 1 < a) [MeasureTheory.IsFiniteMeasure μ] [ProbabilityTheory.IsFiniteKernel κ] [ProbabilityTheory.IsFiniteKernel η] : ProbabilityTheory.condHellingerDiv a κ η μ = ↑(∫ (x : α), (ProbabilityTheory.hellingerDiv a (κ x) (η x)).toReal ∂μ) ↔ (∀ᵐ (x : α) ∂μ, MeasureTheory.Integrable (fun (b : β) => ((κ x).rnDeriv (η x) b).toReal ^ a) (η x)) ∧ (∀ᵐ (x : α) ∂μ, (κ x).AbsolutelyContinuous (η x)) ∧ MeasureTheory.Integrable (fun (x : α) => ∫ (b : β), ((κ x).rnDeriv (η x) b).toReal ^ a ∂η x) μ

theorem ProbabilityTheory.condHellingerDiv_eq_integral_iff_of_lt_one {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α} {κ : ProbabilityTheory.Kernel α β} {η : ProbabilityTheory.Kernel α β} {a : ℝ} (ha_pos : 0 < a) (ha : a < 1) [MeasureTheory.IsFiniteMeasure μ] [ProbabilityTheory.IsFiniteKernel κ] [ProbabilityTheory.IsFiniteKernel η] : ProbabilityTheory.condHellingerDiv a κ η μ = ↑(∫ (x : α), (ProbabilityTheory.hellingerDiv a (κ x) (η x)).toReal ∂μ) ↔ MeasureTheory.Integrable (fun (x : α) => ∫ (b : β), ((κ x).rnDeriv (η x) b).toReal ^ a ∂η x) μ

theorem ProbabilityTheory.condHellingerDiv_eq_integral'_of_one_lt {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α} {κ : ProbabilityTheory.Kernel α β} {η : ProbabilityTheory.Kernel α β} {a : ℝ} (ha : 1 < a) [MeasureTheory.IsFiniteMeasure μ] [ProbabilityTheory.IsFiniteKernel κ] [ProbabilityTheory.IsFiniteKernel η] (h_int : ∀ᵐ (x : α) ∂μ, MeasureTheory.Integrable (fun (b : β) => ((κ x).rnDeriv (η x) b).toReal ^ a) (η x)) (h_ac : ∀ᵐ (x : α) ∂μ, (κ x).AbsolutelyContinuous (η x)) (h_int' : MeasureTheory.Integrable (fun (x : α) => ∫ (b : β), ((κ x).rnDeriv (η x) b).toReal ^ a ∂η x) μ) : ProbabilityTheory.condHellingerDiv a κ η μ = ↑(a - 1)⁻¹ * ↑(∫ (x : α), ∫ (b : β), ((κ x).rnDeriv (η x) b).toReal ^ a ∂η x ∂μ) - ↑(a - 1)⁻¹ * ↑((μ.compProd η) Set.univ).toReal

theorem ProbabilityTheory.condHellingerDiv_eq_integral'_of_one_lt' {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α} {κ : ProbabilityTheory.Kernel α β} {η : ProbabilityTheory.Kernel α β} {a : ℝ} (ha : 1 < a) [MeasureTheory.IsFiniteMeasure μ] [ProbabilityTheory.IsFiniteKernel κ] [ProbabilityTheory.IsMarkovKernel η] (h_int : ∀ᵐ (x : α) ∂μ, MeasureTheory.Integrable (fun (b : β) => ((κ x).rnDeriv (η x) b).toReal ^ a) (η x)) (h_ac : ∀ᵐ (x : α) ∂μ, (κ x).AbsolutelyContinuous (η x)) (h_int' : MeasureTheory.Integrable (fun (x : α) => ∫ (b : β), ((κ x).rnDeriv (η x) b).toReal ^ a ∂η x) μ) : ProbabilityTheory.condHellingerDiv a κ η μ = ↑(a - 1)⁻¹ * ↑(∫ (x : α), ∫ (b : β), ((κ x).rnDeriv (η x) b).toReal ^ a ∂η x ∂μ) - ↑(a - 1)⁻¹ * ↑(μ Set.univ).toReal

theorem ProbabilityTheory.condHellingerDiv_eq_integral'_of_one_lt'' {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α} {κ : ProbabilityTheory.Kernel α β} {η : ProbabilityTheory.Kernel α β} {a : ℝ} (ha : 1 < a) [MeasureTheory.IsProbabilityMeasure μ] [ProbabilityTheory.IsFiniteKernel κ] [ProbabilityTheory.IsMarkovKernel η] (h_int : ∀ᵐ (x : α) ∂μ, MeasureTheory.Integrable (fun (b : β) => ((κ x).rnDeriv (η x) b).toReal ^ a) (η x)) (h_ac : ∀ᵐ (x : α) ∂μ, (κ x).AbsolutelyContinuous (η x)) (h_int' : MeasureTheory.Integrable (fun (x : α) => ∫ (b : β), ((κ x).rnDeriv (η x) b).toReal ^ a ∂η x) μ) : ProbabilityTheory.condHellingerDiv a κ η μ = ↑(a - 1)⁻¹ * ↑(∫ (x : α), ∫ (b : β), ((κ x).rnDeriv (η x) b).toReal ^ a ∂η x ∂μ) - ↑(a - 1)⁻¹

theorem ProbabilityTheory.condHellingerDiv_eq_integral'_of_lt_one {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α} {κ : ProbabilityTheory.Kernel α β} {η : ProbabilityTheory.Kernel α β} {a : ℝ} (ha_pos : 0 < a) (ha : a < 1) [MeasureTheory.IsFiniteMeasure μ] [ProbabilityTheory.IsFiniteKernel κ] [ProbabilityTheory.IsFiniteKernel η] (h_int' : MeasureTheory.Integrable (fun (x : α) => ∫ (b : β), ((κ x).rnDeriv (η x) b).toReal ^ a ∂η x) μ) : ProbabilityTheory.condHellingerDiv a κ η μ = ↑(a - 1)⁻¹ * ↑(∫ (x : α), ∫ (b : β), ((κ x).rnDeriv (η x) b).toReal ^ a ∂η x ∂μ) - ↑(a - 1)⁻¹ * ↑((μ.compProd η) Set.univ).toReal

theorem ProbabilityTheory.condHellingerDiv_eq_integral'_of_lt_one' {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α} {κ : ProbabilityTheory.Kernel α β} {η : ProbabilityTheory.Kernel α β} {a : ℝ} (ha_pos : 0 < a) (ha : a < 1) [MeasureTheory.IsFiniteMeasure μ] [ProbabilityTheory.IsFiniteKernel κ] [ProbabilityTheory.IsMarkovKernel η] (h_int' : MeasureTheory.Integrable (fun (x : α) => ∫ (b : β), ((κ x).rnDeriv (η x) b).toReal ^ a ∂η x) μ) : ProbabilityTheory.condHellingerDiv a κ η μ = ↑(a - 1)⁻¹ * ↑(∫ (x : α), ∫ (b : β), ((κ x).rnDeriv (η x) b).toReal ^ a ∂η x ∂μ) - ↑(a - 1)⁻¹ * ↑(μ Set.univ).toReal

theorem ProbabilityTheory.condHellingerDiv_eq_integral'_of_lt_one'' {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α} {κ : ProbabilityTheory.Kernel α β} {η : ProbabilityTheory.Kernel α β} {a : ℝ} (ha_pos : 0 < a) (ha : a < 1) [MeasureTheory.IsProbabilityMeasure μ] [ProbabilityTheory.IsFiniteKernel κ] [ProbabilityTheory.IsMarkovKernel η] (h_int' : MeasureTheory.Integrable (fun (x : α) => ∫ (b : β), ((κ x).rnDeriv (η x) b).toReal ^ a ∂η x) μ) : ProbabilityTheory.condHellingerDiv a κ η μ = ↑(a - 1)⁻¹ * ↑(∫ (x : α), ∫ (b : β), ((κ x).rnDeriv (η x) b).toReal ^ a ∂η x ∂μ) - ↑(a - 1)⁻¹

theorem ProbabilityTheory.hellingerDiv_compProd_left {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {a : ℝ} [MeasurableSpace.CountableOrCountablyGenerated α β] (ha_nonneg : 0 ≤ a) (μ : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure μ] (κ : ProbabilityTheory.Kernel α β) (η : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsFiniteKernel κ] [∀ (x : α), NeZero (κ x)] [ProbabilityTheory.IsFiniteKernel η] : ProbabilityTheory.hellingerDiv a (μ.compProd κ) (μ.compProd η) = ProbabilityTheory.condHellingerDiv a κ η μ

theorem ProbabilityTheory.hellingerDiv_comp_left_le {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {a : ℝ} [Nonempty α] [StandardBorelSpace α] [MeasurableSpace.CountableOrCountablyGenerated α β] (ha_pos : 0 < a) (μ : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure μ] (κ : ProbabilityTheory.Kernel α β) (η : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsFiniteKernel κ] [∀ (a : α), NeZero (κ a)] [ProbabilityTheory.IsFiniteKernel η] : ProbabilityTheory.hellingerDiv a (μ.bind ⇑κ) (μ.bind ⇑η) ≤ ProbabilityTheory.condHellingerDiv a κ η μ