awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
pos : μ ≪ ν ∧ Integrable (llr μ ν) μ
⊢ klDiv μ ν ≠ ∞

Tactic:
rw [klDiv_ne_top_iff]

Premises used: InformationTheory.klDiv_ne_top_iff
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
⊢ μ ≪ ν ∧ Integrable (llr μ ν) μ

Tactic:
⟨hμν, h_int⟩

Premises used: And.intro
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
⊢ μ ≪ ν ∧ Integrable (llr μ ν) μ

Tactic:
exact ⟨hμν, h_int⟩
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
⊢ klDiv μ ν = 0 ↔ μ = ν

Tactic:
⟨fun h ↦ ?_, fun h ↦ h ▸ klDiv_self _⟩

Premises used: InformationTheory.klDiv_self, Eq.rec, Iff.intro
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
refine : ∀ (h : klDiv μ ν = 0), μ = ν
⊢ klDiv μ ν = 0 ↔ μ = ν

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ h ▸ klDiv_self _⟩
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
h : klDiv μ ν = 0
⊢ klDiv μ ν ≠ ∞

Tactic:
simp [h]
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
h : klDiv μ ν = 0
⊢ klDiv μ ν ≠ ∞

Tactic:
have h_ne : klDiv μ ν ≠ ⊤ := by simp [h]
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
h : klDiv μ ν = 0
h_ne : klDiv μ ν ≠ ∞
⊢ μ ≪ ν ∧ Integrable (llr μ ν) μ

Tactic:
rw [klDiv_ne_top_iff] at h_ne

Premises used: InformationTheory.klDiv_ne_top_iff
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
h : ∫⁻ (x : α), ENNReal.ofReal (klFun (μ.rnDeriv ν x).toReal) ∂ν = 0
h_ne : μ ≪ ν ∧ Integrable (llr μ ν) μ
⊢ Measurable (β := ℝ≥0∞) fun (x : α) ↦ ENNReal.ofReal (klFun (μ.rnDeriv ν x).toReal)

Tactic:
fun_prop
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
h : klDiv μ ν = 0
h_ne : μ ≪ ν ∧ Integrable (llr μ ν) μ
⊢ (ae ν).EventuallyEq (β := ℝ≥0∞) (fun (x : α) ↦ ENNReal.ofReal (klFun (μ.rnDeriv ν x).toReal)) 0

Tactic:
rw [klDiv_eq_lintegral_klFun, if_pos h_ne.1, lintegral_eq_zero_iff (by fun_prop)] at h

Premises used: MeasureTheory.lintegral_eq_zero_iff, InformationTheory.klDiv_eq_lintegral_klFun, if_pos, And.left
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
h : klDiv μ ν = 0
h_ne : μ ≪ ν ∧ Integrable (llr μ ν) μ
h₁ : (ae ν).EventuallyEq (β := ℝ≥0∞) (fun (x : α) ↦ ENNReal.ofReal (klFun (μ.rnDeriv ν x).toReal)) 0
⊢ μ ≪ ν ∧ Integrable (llr μ ν) μ

Tactic:
rw [klDiv_eq_lintegral_klFun, if_pos h_ne.1, lintegral_eq_zero_iff (by fun_prop)] at h

Premises used: MeasureTheory.lintegral_eq_zero_iff, InformationTheory.klDiv_eq_lintegral_klFun, if_pos, And.left
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
h : (ae ν).EventuallyEq (β := ℝ≥0∞) (fun (x : α) ↦ ENNReal.ofReal (klFun (μ.rnDeriv ν x).toReal)) 0
h_ne : μ ≪ ν ∧ Integrable (llr μ ν) μ
⊢ μ = ν

Tactic:
(Measure.rnDeriv_eq_one_iff_eq h_ne.1).mp ?_

Premises used: MeasureTheory.Measure.rnDeriv_eq_one_iff_eq, And.left, Iff.mp
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
h : (ae ν).EventuallyEq (β := ℝ≥0∞) (fun (x : α) ↦ ENNReal.ofReal (klFun (μ.rnDeriv ν x).toReal)) 0
h_ne : μ ≪ ν ∧ Integrable (llr μ ν) μ
refine : μ.rnDeriv ν =ᶠ[ae ν] 1
⊢ μ = ν

Tactic:
refine (Measure.rnDeriv_eq_one_iff_eq h_ne.1).mp ?_

Premises used: MeasureTheory.Measure.rnDeriv_eq_one_iff_eq, And.left, Iff.mp
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
h : (ae ν).EventuallyEq (β := ℝ≥0∞) (fun (x : α) ↦ ENNReal.ofReal (klFun (μ.rnDeriv ν x).toReal)) 0
h_ne : μ ≪ ν ∧ Integrable (llr μ ν) μ
h₁ : ∀ (x : α) (hx : ENNReal.ofReal (klFun (μ.rnDeriv ν x).toReal) = 0 x), μ.rnDeriv ν x = 1 x
⊢ μ.rnDeriv ν =ᶠ[ae ν] 1

Tactic:
filter_upwards [h] with x hx
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
h : (ae ν).EventuallyEq (β := ℝ≥0∞) (fun (x : α) ↦ ENNReal.ofReal (klFun (μ.rnDeriv ν x).toReal)) 0
h_ne : μ ≪ ν ∧ Integrable (llr μ ν) μ
x : α
hx : ENNReal.ofReal (klFun (μ.rnDeriv ν x).toReal) = 0 x
⊢ klFun (μ.rnDeriv ν x).toReal ≤ 0

Tactic:
simp only [Pi.zero_apply, ENNReal.ofReal_eq_zero] at hx

Premises used: ENNReal.ofReal_eq_zero, Pi.zero_apply
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
h : (ae ν).EventuallyEq (β := ℝ≥0∞) (fun (x : α) ↦ ENNReal.ofReal (klFun (μ.rnDeriv ν x).toReal)) 0
h_ne : μ ≪ ν ∧ Integrable (llr μ ν) μ
x : α
hx : klFun (μ.rnDeriv ν x).toReal ≤ 0
⊢ klFun (μ.rnDeriv ν x).toReal = 0

Tactic:
have hx' : klFun (μ.rnDeriv ν x).toReal = 0 := le_antisymm hx (klFun_nonneg ENNReal.toReal_nonneg)
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
h : (ae ν).EventuallyEq (β := ℝ≥0∞) (fun (x : α) ↦ ENNReal.ofReal (klFun (μ.rnDeriv ν x).toReal)) 0
h_ne : μ ≪ ν ∧ Integrable (llr μ ν) μ
x : α
hx : klFun (μ.rnDeriv ν x).toReal ≤ 0
hx' : klFun (μ.rnDeriv ν x).toReal = 0
h₁ : ∀ (hx' : (μ.rnDeriv ν x).toReal = 1), μ.rnDeriv ν x = 1 x
h₂ h₃ h₄ h₅ : ∀ (hx' : μ.rnDeriv ν x = 1), μ.rnDeriv ν x = 1 x
⊢ μ.rnDeriv ν x = 1 x

Tactic:
rwa [klFun_eq_zero_iff ENNReal.toReal_nonneg, ENNReal.toReal_eq_one_iff] at hx'

Premises used: InformationTheory.klFun_eq_zero_iff, ENNReal.toReal_nonneg, ENNReal.toReal_eq_one_iff
-- Module: Mathlib.InformationTheory.KullbackLeibler.ChainRule
Goal:
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
κ η : Kernel 𝓧 𝓨
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsMarkovKernel κ
inst_3 : IsMarkovKernel η
h_ac : μ ⊗ₘ κ ≪ ν ⊗ₘ η
h_int : Integrable (llr (μ ⊗ₘ κ) (ν ⊗ₘ η)) (μ ⊗ₘ κ)
⊢ μ ≪ ν

Tactic:
have ⟨hμν_ac, hκη_ac⟩ := Measure.absolutelyContinuous_compProd_iff.mp h_ac
-- Module: Mathlib.InformationTheory.KullbackLeibler.ChainRule
Goal:
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
κ η : Kernel 𝓧 𝓨
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsMarkovKernel κ
inst_3 : IsMarkovKernel η
h_ac : μ ⊗ₘ κ ≪ ν ⊗ₘ η
h_int : Integrable (llr (μ ⊗ₘ κ) (ν ⊗ₘ η)) (μ ⊗ₘ κ)
hμν_ac : μ ≪ ν
⊢ μ ⊗ₘ κ ≪ μ ⊗ₘ η

Tactic:
have ⟨hμν_ac, hκη_ac⟩ := Measure.absolutelyContinuous_compProd_iff.mp h_ac
-- Module: Mathlib.InformationTheory.KullbackLeibler.ChainRule
Goal:
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
κ η : Kernel 𝓧 𝓨
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsMarkovKernel κ
inst_3 : IsMarkovKernel η
h_ac : μ ⊗ₘ κ ≪ ν ⊗ₘ η
h_int : Integrable (llr (μ ⊗ₘ κ) (ν ⊗ₘ η)) (μ ⊗ₘ κ)
hμν_ac : μ ≪ ν
hκη_ac : μ ⊗ₘ κ ≪ μ ⊗ₘ η
⊢ Integrable (ε := ℝ) (fun (a : 𝓧 × 𝓨) ↦ ((∂μ ⊗ₘ κ/∂ν ⊗ₘ η) a).toReal * log ((∂μ ⊗ₘ κ/∂ν ⊗ₘ η) a).toReal) (ν ⊗ₘ η)

Tactic:
rw [← integrable_rnDeriv_mul_log_iff h_ac] at h_int

Premises used: MeasureTheory.integrable_rnDeriv_mul_log_iff
-- Module: Mathlib.InformationTheory.KullbackLeibler.ChainRule
Goal:
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
κ η : Kernel 𝓧 𝓨
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsMarkovKernel κ
inst_3 : IsMarkovKernel η
h_ac : μ ⊗ₘ κ ≪ ν ⊗ₘ η
h_int : Integrable (llr (μ ⊗ₘ κ) (ν ⊗ₘ η)) (μ ⊗ₘ κ)
hμν_ac : μ ≪ ν
hκη_ac : μ ⊗ₘ κ ≪ μ ⊗ₘ η
h_int₁ :
  Integrable (ε := ℝ) (fun (a : 𝓧 × 𝓨) ↦ ((∂μ ⊗ₘ κ/∂ν ⊗ₘ η) a).toReal * log ((∂μ ⊗ₘ κ/∂ν ⊗ₘ η) a).toReal) (ν ⊗ₘ η)
⊢ μ ≪ ν

Tactic:
rw [← integrable_rnDeriv_mul_log_iff h_ac] at h_int

Premises used: MeasureTheory.integrable_rnDeriv_mul_log_iff
-- Module: Mathlib.InformationTheory.KullbackLeibler.ChainRule
Goal:
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
κ η : Kernel 𝓧 𝓨
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsMarkovKernel κ
inst_3 : IsMarkovKernel η
h_ac : μ ⊗ₘ κ ≪ ν ⊗ₘ η
h_int : Integrable (llr (μ ⊗ₘ κ) (ν ⊗ₘ η)) (μ ⊗ₘ κ)
hμν_ac : μ ≪ ν
hκη_ac : μ ⊗ₘ κ ≪ μ ⊗ₘ η
h_int₁ :
  Integrable (ε := ℝ) (fun (a : 𝓧 × 𝓨) ↦ ((∂μ ⊗ₘ κ/∂ν ⊗ₘ η) a).toReal * log ((∂μ ⊗ₘ κ/∂ν ⊗ₘ η) a).toReal) (ν ⊗ₘ η)
hμν_ac₁ : μ ≪ ν
⊢ μ ⊗ₘ κ ≪ μ ⊗ₘ η

Tactic:
rw [← integrable_rnDeriv_mul_log_iff h_ac] at h_int

Premises used: MeasureTheory.integrable_rnDeriv_mul_log_iff
-- Module: Mathlib.InformationTheory.KullbackLeibler.ChainRule
Goal:
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
κ η : Kernel 𝓧 𝓨
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsMarkovKernel κ
inst_3 : IsMarkovKernel η
h_ac : μ ⊗ₘ κ ≪ ν ⊗ₘ η
h_int : Integrable (ε := ℝ) (fun (a : 𝓧 × 𝓨) ↦ ((∂μ ⊗ₘ κ/∂ν ⊗ₘ η) a).toReal * log ((∂μ ⊗ₘ κ/∂ν ⊗ₘ η) a).toReal) (ν ⊗ₘ η)
hμν_ac : μ ≪ ν
hκη_ac : μ ⊗ₘ κ ≪ μ ⊗ₘ η
⊢ Integrable (ε := ℝ) (fun (a : 𝓧) ↦ ((∂μ/∂ν) a).toReal * log ((∂μ/∂ν) a).toReal) ν

Tactic:
replace h_int := convexOn_mul_log.integrable_apply_rnDeriv_of_integrable_compProd
    continuous_mul_log.stronglyMeasurable continuous_mul_log.continuousWithinAt h_int hκη_ac
-- Module: Mathlib.InformationTheory.KullbackLeibler.ChainRule
Goal:
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
κ η : Kernel 𝓧 𝓨
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsMarkovKernel κ
inst_3 : IsMarkovKernel η
h_ac : μ ⊗ₘ κ ≪ ν ⊗ₘ η
hμν_ac : μ ≪ ν
hκη_ac : μ ⊗ₘ κ ≪ μ ⊗ₘ η
h_int : Integrable (ε := ℝ) (fun (a : 𝓧) ↦ ((∂μ/∂ν) a).toReal * log ((∂μ/∂ν) a).toReal) ν
⊢ Integrable (llr μ ν) μ

Tactic:
(integrable_rnDeriv_mul_log_iff hμν_ac).mp h_int

Premises used: Iff.mp, MeasureTheory.integrable_rnDeriv_mul_log_iff
-- Module: Mathlib.InformationTheory.KullbackLeibler.ChainRule
Goal:
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
κ η : Kernel 𝓧 𝓨
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsMarkovKernel κ
inst_3 : IsMarkovKernel η
h_ac : μ ⊗ₘ κ ≪ ν ⊗ₘ η
hμν_ac : μ ≪ ν
hκη_ac : μ ⊗ₘ κ ≪ μ ⊗ₘ η
h_int : Integrable (ε := ℝ) (fun (a : 𝓧) ↦ ((∂μ/∂ν) a).toReal * log ((∂μ/∂ν) a).toReal) ν
⊢ Integrable (llr μ ν) μ

Tactic:
exact (integrable_rnDeriv_mul_log_iff hμν_ac).mp h_int

Premises used: Iff.mp, MeasureTheory.integrable_rnDeriv_mul_log_iff
-- Module: Mathlib.InformationTheory.KullbackLeibler.ChainRule
Goal:
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
κ η : Kernel 𝓧 𝓨
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsMarkovKernel κ
inst_3 : IsMarkovKernel η
h_ac : μ ⊗ₘ κ ≪ μ ⊗ₘ η
h :
  ∀ (p : 𝓧 × 𝓨) (hp : (∂μ ⊗ₘ κ/∂ν ⊗ₘ η) p = (∂μ/∂ν) p.1 * (∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p),
    ((∂μ ⊗ₘ κ/∂ν ⊗ₘ η) p).toReal * log ((∂μ ⊗ₘ κ/∂ν ⊗ₘ η) p).toReal =
      ((∂μ ⊗ₘ κ/∂ν ⊗ₘ η) p).toReal * (log ((∂μ/∂ν) p.1).toReal + log ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p).toReal)
⊢ ∀ᵐ (p : 𝓧 × 𝓨) ∂ν ⊗ₘ η,
    ((∂μ ⊗ₘ κ/∂ν ⊗ₘ η) p).toReal * log ((∂μ ⊗ₘ κ/∂ν ⊗ₘ η) p).toReal =
      ((∂μ ⊗ₘ κ/∂ν ⊗ₘ η) p).toReal * (log ((∂μ/∂ν) p.1).toReal + log ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p).toReal)

Tactic:
filter_upwards [rnDeriv_compProd h_ac ν] with p hp

Premises used: ProbabilityTheory.rnDeriv_compProd
-- Module: Mathlib.InformationTheory.KullbackLeibler.ChainRule
Goal:
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
κ η : Kernel 𝓧 𝓨
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsMarkovKernel κ
inst_3 : IsMarkovKernel η
h_ac : μ ⊗ₘ κ ≪ μ ⊗ₘ η
p : 𝓧 × 𝓨
hp : (∂μ ⊗ₘ κ/∂ν ⊗ₘ η) p = (∂μ/∂ν) p.1 * (∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p
h :
  ((∂μ/∂ν) p.1).toReal * ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p).toReal * log (((∂μ/∂ν) p.1).toReal * ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p).toReal) =
    ((∂μ/∂ν) p.1).toReal * ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p).toReal * (log ((∂μ/∂ν) p.1).toReal + log ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p).toReal)
⊢ ((∂μ ⊗ₘ κ/∂ν ⊗ₘ η) p).toReal * log ((∂μ ⊗ₘ κ/∂ν ⊗ₘ η) p).toReal =
    ((∂μ ⊗ₘ κ/∂ν ⊗ₘ η) p).toReal * (log ((∂μ/∂ν) p.1).toReal + log ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p).toReal)

Tactic:
simp_rw [hp, ENNReal.toReal_mul]

Premises used: ENNReal.toReal_mul
-- Module: Mathlib.InformationTheory.KullbackLeibler.ChainRule
Goal:
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
κ η : Kernel 𝓧 𝓨
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsMarkovKernel κ
inst_3 : IsMarkovKernel η
h_ac : μ ⊗ₘ κ ≪ μ ⊗ₘ η
p : 𝓧 × 𝓨
hp : (∂μ ⊗ₘ κ/∂ν ⊗ₘ η) p = (∂μ/∂ν) p.1 * (∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p
pos :
  ∀ (h_zero1 : ((∂μ/∂ν) p.1).toReal = 0),
    ((∂μ/∂ν) p.1).toReal * ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p).toReal * log (((∂μ/∂ν) p.1).toReal * ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p).toReal) =
      ((∂μ/∂ν) p.1).toReal * ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p).toReal *
        (log ((∂μ/∂ν) p.1).toReal + log ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p).toReal)
neg :
  ∀ (h_zero1 : ¬((∂μ/∂ν) p.1).toReal = 0),
    ((∂μ/∂ν) p.1).toReal * ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p).toReal * log (((∂μ/∂ν) p.1).toReal * ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p).toReal) =
      ((∂μ/∂ν) p.1).toReal * ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p).toReal *
        (log ((∂μ/∂ν) p.1).toReal + log ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p).toReal)
⊢ ((∂μ/∂ν) p.1).toReal * ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p).toReal * log (((∂μ/∂ν) p.1).toReal * ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p).toReal) =
    ((∂μ/∂ν) p.1).toReal * ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p).toReal * (log ((∂μ/∂ν) p.1).toReal + log ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p).toReal)

Tactic:
by_cases h_zero1 : ((∂μ/∂ν) p.1).toReal = 0

Premises used: MeasureTheory.Measure.rnDeriv, Prod.fst, ENNReal.toReal
-- Module: Mathlib.InformationTheory.KullbackLeibler.ChainRule
Goal:
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
κ η : Kernel 𝓧 𝓨
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsMarkovKernel κ
inst_3 : IsMarkovKernel η
h_ac : μ ⊗ₘ κ ≪ μ ⊗ₘ η
p : 𝓧 × 𝓨
hp : (∂μ ⊗ₘ κ/∂ν ⊗ₘ η) p = (∂μ/∂ν) p.1 * (∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p
h_zero1 : ((∂μ/∂ν) p.1).toReal = 0
⊢ ((∂μ/∂ν) p.1).toReal * ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p).toReal * log (((∂μ/∂ν) p.1).toReal * ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p).toReal) =
    ((∂μ/∂ν) p.1).toReal * ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p).toReal * (log ((∂μ/∂ν) p.1).toReal + log ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p).toReal)

Tactic:
simp [h_zero1]
-- Module: Mathlib.InformationTheory.KullbackLeibler.ChainRule
Goal:
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
κ η : Kernel 𝓧 𝓨
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsMarkovKernel κ
inst_3 : IsMarkovKernel η
h_ac : μ ⊗ₘ κ ≪ μ ⊗ₘ η
p : 𝓧 × 𝓨
hp : (∂μ ⊗ₘ κ/∂ν ⊗ₘ η) p = (∂μ/∂ν) p.1 * (∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p
h_zero1 : ¬((∂μ/∂ν) p.1).toReal = 0
pos :
  ∀ (h_zero2 : ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p).toReal = 0),
    ((∂μ/∂ν) p.1).toReal * ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p).toReal * log (((∂μ/∂ν) p.1).toReal * ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p).toReal) =
      ((∂μ/∂ν) p.1).toReal * ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p).toReal *
        (log ((∂μ/∂ν) p.1).toReal + log ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p).toReal)
neg :
  ∀ (h_zero2 : ¬((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p).toReal = 0),
    ((∂μ/∂ν) p.1).toReal * ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p).toReal * log (((∂μ/∂ν) p.1).toReal * ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p).toReal) =
      ((∂μ/∂ν) p.1).toReal * ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p).toReal *
        (log ((∂μ/∂ν) p.1).toReal + log ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p).toReal)
⊢ ((∂μ/∂ν) p.1).toReal * ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p).toReal * log (((∂μ/∂ν) p.1).toReal * ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p).toReal) =
    ((∂μ/∂ν) p.1).toReal * ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p).toReal * (log ((∂μ/∂ν) p.1).toReal + log ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p).toReal)

Tactic:
by_cases h_zero2 : ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p).toReal = 0

Premises used: MeasureTheory.Measure.rnDeriv, ENNReal.toReal, MeasureTheory.Measure.compProd
-- Module: Mathlib.InformationTheory.KullbackLeibler.ChainRule
Goal:
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
κ η : Kernel 𝓧 𝓨
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsMarkovKernel κ
inst_3 : IsMarkovKernel η
h_ac : μ ⊗ₘ κ ≪ μ ⊗ₘ η
p : 𝓧 × 𝓨
hp : (∂μ ⊗ₘ κ/∂ν ⊗ₘ η) p = (∂μ/∂ν) p.1 * (∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p
h_zero1 : ¬((∂μ/∂ν) p.1).toReal = 0
h_zero2 : ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p).toReal = 0
⊢ ((∂μ/∂ν) p.1).toReal * ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p).toReal * log (((∂μ/∂ν) p.1).toReal * ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p).toReal) =
    ((∂μ/∂ν) p.1).toReal * ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p).toReal * (log ((∂μ/∂ν) p.1).toReal + log ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p).toReal)

Tactic:
simp [h_zero2]
-- Module: Mathlib.InformationTheory.KullbackLeibler.ChainRule
Goal:
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
κ η : Kernel 𝓧 𝓨
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsMarkovKernel κ
inst_3 : IsMarkovKernel η
h_ac : μ ⊗ₘ κ ≪ μ ⊗ₘ η
p : 𝓧 × 𝓨
hp : (∂μ ⊗ₘ κ/∂ν ⊗ₘ η) p = (∂μ/∂ν) p.1 * (∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p
h_zero1 : ¬((∂μ/∂ν) p.1).toReal = 0
h_zero2 : ¬((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p).toReal = 0
⊢ ((∂μ/∂ν) p.1).toReal * ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p).toReal * log (((∂μ/∂ν) p.1).toReal * ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p).toReal) =
    ((∂μ/∂ν) p.1).toReal * ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p).toReal * (log ((∂μ/∂ν) p.1).toReal + log ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p).toReal)

Tactic:
simp [log_mul h_zero1 h_zero2]

Premises used: Real.log_mul
-- Module: Mathlib.InformationTheory.KullbackLeibler.ChainRule
Goal:
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
κ η : Kernel 𝓧 𝓨
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsMarkovKernel κ
inst_3 : IsMarkovKernel η
h_ac : μ ⊗ₘ κ ≪ ν ⊗ₘ η
⊢ μ ≪ ν

Tactic:
have ⟨h_ac_μν, h_ac_κη⟩ := Measure.absolutelyContinuous_compProd_iff.mp h_ac
-- Module: Mathlib.InformationTheory.KullbackLeibler.ChainRule
Goal:
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
κ η : Kernel 𝓧 𝓨
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsMarkovKernel κ
inst_3 : IsMarkovKernel η
h_ac : μ ⊗ₘ κ ≪ ν ⊗ₘ η
h_ac_μν : μ ≪ ν
⊢ μ ⊗ₘ κ ≪ μ ⊗ₘ η

Tactic:
have ⟨h_ac_μν, h_ac_κη⟩ := Measure.absolutelyContinuous_compProd_iff.mp h_ac
-- Module: Mathlib.InformationTheory.KullbackLeibler.ChainRule
Goal:
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
κ η : Kernel 𝓧 𝓨
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsMarkovKernel κ
inst_3 : IsMarkovKernel η
h_ac : μ ⊗ₘ κ ≪ ν ⊗ₘ η
h_ac_μν : μ ≪ ν
h_ac_κη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
rw :
  Integrable (ε := ℝ) (fun (x : 𝓧 × 𝓨) ↦ log ((∂μ/∂ν) x.1).toReal + log ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) x).toReal) (μ ⊗ₘ κ) ↔
    Integrable (llr μ ν) μ ∧ Integrable (llr (μ ⊗ₘ κ) (μ ⊗ₘ η)) (μ ⊗ₘ κ)
⊢ Integrable (llr (μ ⊗ₘ κ) (ν ⊗ₘ η)) (μ ⊗ₘ κ) ↔ Integrable (llr μ ν) μ ∧ Integrable (llr (μ ⊗ₘ κ) (μ ⊗ₘ η)) (μ ⊗ₘ κ)

Tactic:
rw [← integrable_rnDeriv_mul_log_iff h_ac,
    integrable_congr (rnDeriv_compProd_mul_log_eq_mul_add h_ac_κη),
    integrable_toReal_rnDeriv_mul_iff h_ac]

Premises used: MeasureTheory.integrable_congr, InformationTheory.rnDeriv_compProd_mul_log_eq_mul_add, MeasureTheory.integrable_toReal_rnDeriv_mul_iff, MeasureTheory.integrable_rnDeriv_mul_log_iff
-- Module: Mathlib.InformationTheory.KullbackLeibler.ChainRule
Goal:
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
κ η : Kernel 𝓧 𝓨
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsMarkovKernel κ
inst_3 : IsMarkovKernel η
h_ac : μ ⊗ₘ κ ≪ ν ⊗ₘ η
h_ac_μν : μ ≪ ν
h_ac_κη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
rw :
  Integrable (llr μ ν) μ ↔
    (∀ᵐ (x : 𝓧) ∂μ, @Integrable ℝ _ _ _ m𝓨 (fun (y : 𝓨) ↦ llr μ ν (x, y).1) ((κ : (a : 𝓧) → Measure 𝓨) x)) ∧
      Integrable (ε := ℝ)
        (fun (x : 𝓧) ↦ @integral _ _ _ _ m𝓨 ((κ : (a : 𝓧) → Measure 𝓨) x) fun (y : 𝓨) ↦ ‖llr μ ν (x, y).1‖) μ
rw₁ : AEStronglyMeasurable (β := ℝ) (fun (x : 𝓧 × 𝓨) ↦ llr μ ν x.1) (μ ⊗ₘ κ)
⊢ Integrable (llr μ ν) μ ↔ Integrable (ε := ℝ) (fun (x : 𝓧 × 𝓨) ↦ llr μ ν x.1) (μ ⊗ₘ κ)

Tactic:
rw [Measure.integrable_compProd_iff]

Premises used: MeasureTheory.Measure.integrable_compProd_iff
-- Module: Mathlib.InformationTheory.KullbackLeibler.ChainRule
Goal:
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
κ η : Kernel 𝓧 𝓨
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsMarkovKernel κ
inst_3 : IsMarkovKernel η
h_ac : μ ⊗ₘ κ ≪ ν ⊗ₘ η
h_ac_μν : μ ≪ ν
h_ac_κη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
⊢ StronglyMeasurable (β := ℝ) fun (x : 𝓧 × 𝓨) ↦ llr μ ν x.1

Tactic:
fun_prop
-- Module: Mathlib.InformationTheory.KullbackLeibler.ChainRule
Goal:
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
κ η : Kernel 𝓧 𝓨
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsMarkovKernel κ
inst_3 : IsMarkovKernel η
h_ac : μ ⊗ₘ κ ≪ ν ⊗ₘ η
h_ac_μν : μ ≪ ν
h_ac_κη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
⊢ AEStronglyMeasurable (β := ℝ) (fun (x : 𝓧 × 𝓨) ↦ llr μ ν x.1) (μ ⊗ₘ κ)

Tactic:
exact StronglyMeasurable.aestronglyMeasurable (by fun_prop)

Premises used: MeasureTheory.StronglyMeasurable.aestronglyMeasurable
-- Module: Mathlib.InformationTheory.KullbackLeibler.ChainRule
Goal:
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
κ η : Kernel 𝓧 𝓨
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsMarkovKernel κ
inst_3 : IsMarkovKernel η
h_ac : μ ⊗ₘ κ ≪ ν ⊗ₘ η
h_ac_μν : μ ≪ ν
h_ac_κη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
simp : Integrable (llr μ ν) μ ↔ Integrable (ε := ℝ) (fun (x : 𝓧) ↦ ‖llr μ ν x‖) μ
⊢ Integrable (llr μ ν) μ ↔
    (∀ᵐ (x : 𝓧) ∂μ, @Integrable ℝ _ _ _ m𝓨 (fun (y : 𝓨) ↦ llr μ ν (x, y).1) ((κ : (a : 𝓧) → Measure 𝓨) x)) ∧
      Integrable (ε := ℝ)
        (fun (x : 𝓧) ↦ @integral _ _ _ _ m𝓨 ((κ : (a : 𝓧) → Measure 𝓨) x) fun (y : 𝓨) ↦ ‖llr μ ν (x, y).1‖) μ

Tactic:
simp only [ne_eq, enorm_ne_top, not_false_eq_true, integrable_const_enorm,
      Filter.eventually_true, integral_const, probReal_univ, smul_eq_mul, one_mul, true_and]

Premises used: ne_eq, Filter.eventually_true, MeasureTheory.integral_const, MeasureTheory.probReal_univ, MeasureTheory.integrable_const_enorm, smul_eq_mul, not_false_eq_true, enorm_ne_top, one_mul, true_and
-- Module: Mathlib.InformationTheory.KullbackLeibler.ChainRule
Goal:
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
κ η : Kernel 𝓧 𝓨
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsMarkovKernel κ
inst_3 : IsMarkovKernel η
h_ac : μ ⊗ₘ κ ≪ ν ⊗ₘ η
h_ac_μν : μ ≪ ν
h_ac_κη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
⊢ AEStronglyMeasurable (llr μ ν) μ

Tactic:
fun_prop
-- Module: Mathlib.InformationTheory.KullbackLeibler.ChainRule
Goal:
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
κ η : Kernel 𝓧 𝓨
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsMarkovKernel κ
inst_3 : IsMarkovKernel η
h_ac : μ ⊗ₘ κ ≪ ν ⊗ₘ η
h_ac_μν : μ ≪ ν
h_ac_κη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
rw rw₁ : Integrable (ε := ℝ) (fun (a : 𝓧) ↦ ‖llr μ ν a‖) μ ↔ Integrable (ε := ℝ) (fun (x : 𝓧) ↦ ‖llr μ ν x‖) μ
⊢ Integrable (llr μ ν) μ ↔ Integrable (ε := ℝ) (fun (x : 𝓧) ↦ ‖llr μ ν x‖) μ

Tactic:
rw [← integrable_norm_iff (by fun_prop)]

Premises used: MeasureTheory.integrable_norm_iff