awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.ChainRule (hypothesis)
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 (llr μ ν) μ
h_int_κη : Integrable (llr (μ ⊗ₘ κ) (μ ⊗ₘ η)) (μ ⊗ₘ κ)
⊢ ∫ (p : 𝓧 × 𝓨), llr (μ ⊗ₘ κ) (ν ⊗ₘ η) p ∂μ ⊗ₘ κ =
    HAdd.hAdd (α := ℝ) (∫ (a : 𝓧), llr μ ν a ∂μ) (∫ (p : 𝓧 × 𝓨), llr (μ ⊗ₘ κ) (μ ⊗ₘ η) p ∂μ ⊗ₘ κ)
have h_int1 : Integrable (ε := ℝ) (fun (p : 𝓧 × 𝓨) ↦ log ((∂μ/∂ν) p.1).toReal) (μ ⊗ₘ κ)
Tactic: have h_int1 : Integrable (fun p ↦ log ((∂μ/∂ν) p.1).toReal) (μ ⊗ₘ κ) := by
    rw [Measure.integrable_compProd_iff]
    · 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]
      rwa [← integrable_norm_iff (by fun_prop)] at h_int_μν
    · exact StronglyMeasurable.aestronglyMeasurable (by fun_prop)
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.ChainRule (goal)
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 (llr μ ν) μ
h_int_κη : Integrable (llr (μ ⊗ₘ κ) (μ ⊗ₘ η)) (μ ⊗ₘ κ)
h_int1 : Integrable (ε := ℝ) (fun (p : 𝓧 × 𝓨) ↦ log ((∂μ/∂ν) p.1).toReal) (μ ⊗ₘ κ)
⊢ Eq (α := ℝ) (∫ (p : 𝓧 × 𝓨), llr (μ ⊗ₘ κ) (ν ⊗ₘ η) p ∂μ ⊗ₘ κ)
    (∫ (p : 𝓧 × 𝓨), ((∂μ ⊗ₘ κ/∂ν ⊗ₘ η) p).toReal * log ((∂μ ⊗ₘ κ/∂ν ⊗ₘ η) p).toReal ∂ν ⊗ₘ η)
have rw : Eq (α := ℝ) (∫ (p : 𝓧 × 𝓨), llr (μ ⊗ₘ κ) (ν ⊗ₘ η) p ∂μ ⊗ₘ κ) (∫ (a : 𝓧 × 𝓨), llr (μ ⊗ₘ κ) (ν ⊗ₘ η) a ∂μ ⊗ₘ κ)
Tactic: rw [integral_rnDeriv_mul_log h_ac]
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.ChainRule (goal)
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 (llr μ ν) μ
h_int_κη : Integrable (llr (μ ⊗ₘ κ) (μ ⊗ₘ η)) (μ ⊗ₘ κ)
h_int1 : Integrable (ε := ℝ) (fun (p : 𝓧 × 𝓨) ↦ log ((∂μ/∂ν) p.1).toReal) (μ ⊗ₘ κ)
⊢ ∫ (p : 𝓧 × 𝓨), log ((∂μ/∂ν) p.1).toReal + log ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p).toReal ∂μ ⊗ₘ κ =
    HAdd.hAdd (α := ℝ) (∫ (p : 𝓧 × 𝓨), log ((∂μ/∂ν) p.1).toReal ∂μ ⊗ₘ κ)
      (∫ (p : 𝓧 × 𝓨), log ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p).toReal ∂μ ⊗ₘ κ)
have rw : Integrable (ε := ℝ) (fun (p : 𝓧 × 𝓨) ↦ log ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p).toReal) (μ ⊗ₘ κ)
Tactic: rw [integral_add h_int1]
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.ChainRule (goal)
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 (llr μ ν) μ
h_int_κη : Integrable (llr (μ ⊗ₘ κ) (μ ⊗ₘ η)) (μ ⊗ₘ κ)
h_int1 : Integrable (ε := ℝ) (fun (p : 𝓧 × 𝓨) ↦ log ((∂μ/∂ν) p.1).toReal) (μ ⊗ₘ κ)
⊢ HAdd.hAdd (α := ℝ) (∫ (p : 𝓧 × 𝓨), log ((∂μ/∂ν) p.1).toReal ∂μ ⊗ₘ κ)
      (∫ (p : 𝓧 × 𝓨), log ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p).toReal ∂μ ⊗ₘ κ) =
    HAdd.hAdd (α := ℝ) (∫ (a : 𝓧), llr μ ν a ∂μ) (∫ (p : 𝓧 × 𝓨), llr (μ ⊗ₘ κ) (μ ⊗ₘ η) p ∂μ ⊗ₘ κ)
have e_a : Eq (α := ℝ) (∫ (p : 𝓧 × 𝓨), log ((∂μ/∂ν) p.1).toReal ∂μ ⊗ₘ κ) (∫ (a : 𝓧), llr μ ν a ∂μ)
Tactic: congr
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.ChainRule (goal)
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 (llr μ ν) μ
h_int_κη : Integrable (llr (μ ⊗ₘ κ) (μ ⊗ₘ η)) (μ ⊗ₘ κ)
h_int1 : Integrable (ε := ℝ) (fun (p : 𝓧 × 𝓨) ↦ log ((∂μ/∂ν) p.1).toReal) (μ ⊗ₘ κ)
⊢ Eq (α := ℝ) (∫ (p : 𝓧 × 𝓨), log ((∂μ/∂ν) p.1).toReal ∂μ ⊗ₘ κ) (∫ (a : 𝓧), llr μ ν a ∂μ)
have e_a : Eq (α := ℝ)
  (∫ (a : 𝓧), @integral _ _ _ _ m𝓨 ((κ : (a : 𝓧) → Measure 𝓨) a) fun (b : 𝓨) ↦ log ((∂μ/∂ν) (a, b).1).toReal ∂μ)
  (∫ (a : 𝓧), llr μ ν a ∂μ)
Tactic: rw [Measure.integral_compProd h_int1]
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.ChainRule (goal)
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 (llr μ ν) μ
h_int_κη : Integrable (llr (μ ⊗ₘ κ) (μ ⊗ₘ η)) (μ ⊗ₘ κ)
h_int1 : Integrable (ε := ℝ) (fun (p : 𝓧 × 𝓨) ↦ log ((∂μ/∂ν) p.1).toReal) (μ ⊗ₘ κ)
⊢ ∫ (p : 𝓧 × 𝓨), llr (μ ⊗ₘ κ) (ν ⊗ₘ η) p ∂μ ⊗ₘ κ =
    HAdd.hAdd (α := ℝ) (∫ (a : 𝓧), llr μ ν a ∂μ) (∫ (p : 𝓧 × 𝓨), llr (μ ⊗ₘ κ) (μ ⊗ₘ η) p ∂μ ⊗ₘ κ)
have calc : Eq (α := ℝ) (∫ (p : 𝓧 × 𝓨), llr (μ ⊗ₘ κ) (ν ⊗ₘ η) p ∂μ ⊗ₘ κ)
  (∫ (p : 𝓧 × 𝓨), ((∂μ ⊗ₘ κ/∂ν ⊗ₘ η) p).toReal * log ((∂μ ⊗ₘ κ/∂ν ⊗ₘ η) p).toReal ∂ν ⊗ₘ η)
Tactic: calc ∫ p, llr (μ ⊗ₘ κ) (ν ⊗ₘ η) p ∂μ ⊗ₘ κ
  _ = ∫ p, ((∂μ ⊗ₘ κ/∂ν ⊗ₘ η) p).toReal * log ((∂μ ⊗ₘ κ/∂ν ⊗ₘ η) p).toReal ∂(ν ⊗ₘ η) := by
    rw [integral_rnDeriv_mul_log h_ac]
  _ = ∫ p, ((∂μ ⊗ₘ κ/∂ν ⊗ₘ η) p).toReal *
      (log ((∂μ/∂ν) p.1).toReal + log ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p).toReal) ∂(ν ⊗ₘ η) :=
    integral_congr_ae (rnDeriv_compProd_mul_log_eq_mul_add h_ac_κη)
  _ = ∫ p, (log ((∂μ/∂ν) p.1).toReal + log ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p).toReal) ∂(μ ⊗ₘ κ) :=
    integral_rnDeriv_smul h_ac
  _ = ∫ p, log ((∂μ/∂ν) p.1).toReal ∂(μ ⊗ₘ κ) +
      ∫ p, log ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p).toReal ∂(μ ⊗ₘ κ) := by
    rw [integral_add h_int1]
    exact h_int_κη.ofReal
  _ = ∫ a, llr μ ν a ∂μ + ∫ p, llr (μ ⊗ₘ κ) (μ ⊗ₘ η) p ∂(μ ⊗ₘ κ) := by
    congr
    rw [Measure.integral_compProd h_int1]
    simp [llr]
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.ChainRule (goal)
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 (llr μ ν) μ
h_int_κη : Integrable (llr (μ ⊗ₘ κ) (μ ⊗ₘ η)) (μ ⊗ₘ κ)
h_int1 : Integrable (ε := ℝ) (fun (p : 𝓧 × 𝓨) ↦ log ((∂μ/∂ν) p.1).toReal) (μ ⊗ₘ κ)
calc :
  Eq (α := ℝ) (∫ (p : 𝓧 × 𝓨), llr (μ ⊗ₘ κ) (ν ⊗ₘ η) p ∂μ ⊗ₘ κ)
    (∫ (p : 𝓧 × 𝓨), ((∂μ ⊗ₘ κ/∂ν ⊗ₘ η) p).toReal * log ((∂μ ⊗ₘ κ/∂ν ⊗ₘ η) p).toReal ∂ν ⊗ₘ η)
⊢ ∫ (p : 𝓧 × 𝓨), llr (μ ⊗ₘ κ) (ν ⊗ₘ η) p ∂μ ⊗ₘ κ =
    HAdd.hAdd (α := ℝ) (∫ (a : 𝓧), llr μ ν a ∂μ) (∫ (p : 𝓧 × 𝓨), llr (μ ⊗ₘ κ) (μ ⊗ₘ η) p ∂μ ⊗ₘ κ)
have calc₁ : ∫ (p : 𝓧 × 𝓨), log ((∂μ/∂ν) p.1).toReal + log ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p).toReal ∂μ ⊗ₘ κ =
  HAdd.hAdd (α := ℝ) (∫ (p : 𝓧 × 𝓨), log ((∂μ/∂ν) p.1).toReal ∂μ ⊗ₘ κ)
    (∫ (p : 𝓧 × 𝓨), log ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p).toReal ∂μ ⊗ₘ κ)
Tactic: calc ∫ p, llr (μ ⊗ₘ κ) (ν ⊗ₘ η) p ∂μ ⊗ₘ κ
  _ = ∫ p, ((∂μ ⊗ₘ κ/∂ν ⊗ₘ η) p).toReal * log ((∂μ ⊗ₘ κ/∂ν ⊗ₘ η) p).toReal ∂(ν ⊗ₘ η) := by
    rw [integral_rnDeriv_mul_log h_ac]
  _ = ∫ p, ((∂μ ⊗ₘ κ/∂ν ⊗ₘ η) p).toReal *
      (log ((∂μ/∂ν) p.1).toReal + log ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p).toReal) ∂(ν ⊗ₘ η) :=
    integral_congr_ae (rnDeriv_compProd_mul_log_eq_mul_add h_ac_κη)
  _ = ∫ p, (log ((∂μ/∂ν) p.1).toReal + log ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p).toReal) ∂(μ ⊗ₘ κ) :=
    integral_rnDeriv_smul h_ac
  _ = ∫ p, log ((∂μ/∂ν) p.1).toReal ∂(μ ⊗ₘ κ) +
      ∫ p, log ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p).toReal ∂(μ ⊗ₘ κ) := by
    rw [integral_add h_int1]
    exact h_int_κη.ofReal
  _ = ∫ a, llr μ ν a ∂μ + ∫ p, llr (μ ⊗ₘ κ) (μ ⊗ₘ η) p ∂(μ ⊗ₘ κ) := by
    congr
    rw [Measure.integral_compProd h_int1]
    simp [llr]
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.ChainRule (goal)
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 (llr μ ν) μ
h_int_κη : Integrable (llr (μ ⊗ₘ κ) (μ ⊗ₘ η)) (μ ⊗ₘ κ)
h_int1 : Integrable (ε := ℝ) (fun (p : 𝓧 × 𝓨) ↦ log ((∂μ/∂ν) p.1).toReal) (μ ⊗ₘ κ)
calc :
  Eq (α := ℝ) (∫ (p : 𝓧 × 𝓨), llr (μ ⊗ₘ κ) (ν ⊗ₘ η) p ∂μ ⊗ₘ κ)
    (∫ (p : 𝓧 × 𝓨), ((∂μ ⊗ₘ κ/∂ν ⊗ₘ η) p).toReal * log ((∂μ ⊗ₘ κ/∂ν ⊗ₘ η) p).toReal ∂ν ⊗ₘ η)
calc₁ :
  ∫ (p : 𝓧 × 𝓨), log ((∂μ/∂ν) p.1).toReal + log ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p).toReal ∂μ ⊗ₘ κ =
    HAdd.hAdd (α := ℝ) (∫ (p : 𝓧 × 𝓨), log ((∂μ/∂ν) p.1).toReal ∂μ ⊗ₘ κ)
      (∫ (p : 𝓧 × 𝓨), log ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p).toReal ∂μ ⊗ₘ κ)
⊢ ∫ (p : 𝓧 × 𝓨), llr (μ ⊗ₘ κ) (ν ⊗ₘ η) p ∂μ ⊗ₘ κ =
    HAdd.hAdd (α := ℝ) (∫ (a : 𝓧), llr μ ν a ∂μ) (∫ (p : 𝓧 × 𝓨), llr (μ ⊗ₘ κ) (μ ⊗ₘ η) p ∂μ ⊗ₘ κ)
have calc₂ : HAdd.hAdd (α := ℝ) (∫ (p : 𝓧 × 𝓨), log ((∂μ/∂ν) p.1).toReal ∂μ ⊗ₘ κ)
    (∫ (p : 𝓧 × 𝓨), log ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p).toReal ∂μ ⊗ₘ κ) =
  HAdd.hAdd (α := ℝ) (∫ (a : 𝓧), llr μ ν a ∂μ) (∫ (p : 𝓧 × 𝓨), llr (μ ⊗ₘ κ) (μ ⊗ₘ η) p ∂μ ⊗ₘ κ)
Tactic: calc ∫ p, llr (μ ⊗ₘ κ) (ν ⊗ₘ η) p ∂μ ⊗ₘ κ
  _ = ∫ p, ((∂μ ⊗ₘ κ/∂ν ⊗ₘ η) p).toReal * log ((∂μ ⊗ₘ κ/∂ν ⊗ₘ η) p).toReal ∂(ν ⊗ₘ η) := by
    rw [integral_rnDeriv_mul_log h_ac]
  _ = ∫ p, ((∂μ ⊗ₘ κ/∂ν ⊗ₘ η) p).toReal *
      (log ((∂μ/∂ν) p.1).toReal + log ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p).toReal) ∂(ν ⊗ₘ η) :=
    integral_congr_ae (rnDeriv_compProd_mul_log_eq_mul_add h_ac_κη)
  _ = ∫ p, (log ((∂μ/∂ν) p.1).toReal + log ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p).toReal) ∂(μ ⊗ₘ κ) :=
    integral_rnDeriv_smul h_ac
  _ = ∫ p, log ((∂μ/∂ν) p.1).toReal ∂(μ ⊗ₘ κ) +
      ∫ p, log ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p).toReal ∂(μ ⊗ₘ κ) := by
    rw [integral_add h_int1]
    exact h_int_κη.ofReal
  _ = ∫ a, llr μ ν a ∂μ + ∫ p, llr (μ ⊗ₘ κ) (μ ⊗ₘ η) p ∂(μ ⊗ₘ κ) := by
    congr
    rw [Measure.integral_compProd h_int1]
    simp [llr]
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.ChainRule (goal)
Goal:
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
κ : Kernel 𝓧 𝓨
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsMarkovKernel κ
⊢ klDiv (μ ⊗ₘ κ) (ν ⊗ₘ κ) = klDiv μ ν
have pos : ∀ (h_ac : μ ⊗ₘ κ ≪ ν ⊗ₘ κ), klDiv (μ ⊗ₘ κ) (ν ⊗ₘ κ) = klDiv μ ν
Tactic: by_cases h_ac : μ ⊗ₘ κ ≪ ν ⊗ₘ κ
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.ChainRule (goal)
Goal:
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
κ : Kernel 𝓧 𝓨
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsMarkovKernel κ
pos : ∀ (h_ac : μ ⊗ₘ κ ≪ ν ⊗ₘ κ), klDiv (μ ⊗ₘ κ) (ν ⊗ₘ κ) = klDiv μ ν
⊢ klDiv (μ ⊗ₘ κ) (ν ⊗ₘ κ) = klDiv μ ν
have neg : ∀ (h_ac : ¬μ ⊗ₘ κ ≪ ν ⊗ₘ κ), klDiv (μ ⊗ₘ κ) (ν ⊗ₘ κ) = klDiv μ ν
Tactic: by_cases h_ac : μ ⊗ₘ κ ≪ ν ⊗ₘ κ
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.ChainRule (goal)
Goal:
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
κ : Kernel 𝓧 𝓨
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsMarkovKernel κ
h_ac : ¬μ ⊗ₘ κ ≪ ν ⊗ₘ κ
⊢ klDiv (μ ⊗ₘ κ) (ν ⊗ₘ κ) = klDiv μ ν
have neg : ¬μ ≪ ν
Tactic: rw [klDiv_of_not_ac h_ac, klDiv_of_not_ac]
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.ChainRule (goal)
Goal:
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
κ : Kernel 𝓧 𝓨
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsMarkovKernel κ
h_ac : ¬μ ⊗ₘ κ ≪ ν ⊗ₘ κ
⊢ ¬μ ≪ ν
have neg : ∀ (h_ac : ¬μ ≪ ν), ¬μ ≪ ν
Tactic: rwa [Measure.absolutelyContinuous_compProd_left_iff] at h_ac
Cleared hypotheses: h_ac
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.ChainRule (goal)
Goal:
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
κ : Kernel 𝓧 𝓨
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsMarkovKernel κ
h_ac : μ ⊗ₘ κ ≪ ν ⊗ₘ κ
⊢ klDiv (μ ⊗ₘ κ) (ν ⊗ₘ κ) = klDiv μ ν
have pos : ∫⁻ (x : 𝓧 × 𝓨), ENNReal.ofReal (klFun ((∂μ ⊗ₘ κ/∂ν ⊗ₘ κ) x).toReal) ∂ν ⊗ₘ κ =
  ∫⁻ (x : 𝓧), ENNReal.ofReal (klFun ((∂μ/∂ν) x).toReal) ∂ν
Tactic: rw [klDiv_eq_lintegral_klFun_of_ac h_ac,
    klDiv_eq_lintegral_klFun_of_ac (Measure.absolutelyContinuous_compProd_left_iff.mp h_ac)]
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.ChainRule (hypothesis)
Goal:
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
κ : Kernel 𝓧 𝓨
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsMarkovKernel κ
h_ac : μ ⊗ₘ κ ≪ ν ⊗ₘ κ
⊢ ∫⁻ (x : 𝓧 × 𝓨), ENNReal.ofReal (klFun ((∂μ ⊗ₘ κ/∂ν ⊗ₘ κ) x).toReal) ∂ν ⊗ₘ κ =
    ∫⁻ (x : 𝓧), ENNReal.ofReal (klFun ((∂μ/∂ν) x).toReal) ∂ν
have h_ac₁ : μ ≪ ν
Tactic: rw [Measure.absolutelyContinuous_compProd_left_iff] at h_ac
Cleared hypotheses: h_ac
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.ChainRule (goal)
Goal:
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
κ : Kernel 𝓧 𝓨
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsMarkovKernel κ
h_ac : μ ≪ ν
⊢ ∫⁻ (p : 𝓧 × 𝓨), ENNReal.ofReal (klFun ((∂μ ⊗ₘ κ/∂ν ⊗ₘ κ) p).toReal) ∂ν ⊗ₘ κ =
    ∫⁻ (p : 𝓧 × 𝓨), ENNReal.ofReal (klFun ((∂μ/∂ν) p.1).toReal) ∂ν ⊗ₘ κ
have refine : (ae (ν ⊗ₘ κ)).EventuallyEq (β := ℝ≥0∞) (fun (p : 𝓧 × 𝓨) ↦ ENNReal.ofReal (klFun ((∂μ ⊗ₘ κ/∂ν ⊗ₘ κ) p).toReal))
  fun (p : 𝓧 × 𝓨) ↦ ENNReal.ofReal (klFun ((∂μ/∂ν) p.1).toReal)
Tactic: refine lintegral_congr_ae ?_
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.ChainRule (goal)
Goal:
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
κ : Kernel 𝓧 𝓨
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsMarkovKernel κ
h_ac : μ ≪ ν
⊢ (ae (ν ⊗ₘ κ)).EventuallyEq (β := ℝ≥0∞) (fun (p : 𝓧 × 𝓨) ↦ ENNReal.ofReal (klFun ((∂μ ⊗ₘ κ/∂ν ⊗ₘ κ) p).toReal))
    fun (p : 𝓧 × 𝓨) ↦ ENNReal.ofReal (klFun ((∂μ/∂ν) p.1).toReal)
have h : ∀ (a : 𝓧 × 𝓨),
  Membership.mem (γ := Set (𝓧 × 𝓨))
    {x : 𝓧 × 𝓨 |
      Membership.mem (γ := Set (𝓧 × 𝓨))
          {x : 𝓧 × 𝓨 | (fun (x : 𝓧 × 𝓨) ↦ (∂μ ⊗ₘ κ/∂ν ⊗ₘ κ) x = (fun (p : 𝓧 × 𝓨) ↦ (∂μ/∂ν) p.1) x) x} x →
        Membership.mem (γ := Set (𝓧 × 𝓨))
          {x : 𝓧 × 𝓨 |
            (fun (x : 𝓧 × 𝓨) ↦
                Eq (α := ℝ≥0∞) ((fun (p : 𝓧 × 𝓨) ↦ ENNReal.ofReal (klFun ((∂μ ⊗ₘ κ/∂ν ⊗ₘ κ) p).toReal)) x)
                  ((fun (p : 𝓧 × 𝓨) ↦ ENNReal.ofReal (klFun ((∂μ/∂ν) p.1).toReal)) x))
              x}
          x}
    a
Tactic: filter_upwards [rnDeriv_measure_compProd_left μ ν κ] with p hp using by simp_rw [hp]
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.ChainRule (goal)
Goal:
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
κ : Kernel 𝓧 𝓨
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsMarkovKernel κ
h_ac : μ ≪ ν
h :
  ∀ (a : 𝓧 × 𝓨),
    Membership.mem (γ := Set (𝓧 × 𝓨))
      {x : 𝓧 × 𝓨 |
        Membership.mem (γ := Set (𝓧 × 𝓨))
            {x : 𝓧 × 𝓨 | (fun (x : 𝓧 × 𝓨) ↦ (∂μ ⊗ₘ κ/∂ν ⊗ₘ κ) x = (fun (p : 𝓧 × 𝓨) ↦ (∂μ/∂ν) p.1) x) x} x →
          Membership.mem (γ := Set (𝓧 × 𝓨))
            {x : 𝓧 × 𝓨 |
              (fun (x : 𝓧 × 𝓨) ↦
                  Eq (α := ℝ≥0∞) ((fun (p : 𝓧 × 𝓨) ↦ ENNReal.ofReal (klFun ((∂μ ⊗ₘ κ/∂ν ⊗ₘ κ) p).toReal)) x)
                    ((fun (p : 𝓧 × 𝓨) ↦ ENNReal.ofReal (klFun ((∂μ/∂ν) p.1).toReal)) x))
                x}
            x}
      a
⊢ (ae (ν ⊗ₘ κ)).EventuallyEq (β := ℝ≥0∞) (fun (p : 𝓧 × 𝓨) ↦ ENNReal.ofReal (klFun ((∂μ ⊗ₘ κ/∂ν ⊗ₘ κ) p).toReal))
    fun (p : 𝓧 × 𝓨) ↦ ENNReal.ofReal (klFun ((∂μ/∂ν) p.1).toReal)
have h₁ : ∀ (a : 𝓧 × 𝓨),
  (∂μ ⊗ₘ κ/∂ν ⊗ₘ κ) a = (∂μ/∂ν) a.1 →
    ENNReal.ofReal (klFun ((∂μ ⊗ₘ κ/∂ν ⊗ₘ κ) a).toReal) = ENNReal.ofReal (klFun ((∂μ/∂ν) a.1).toReal)
Tactic: filter_upwards [rnDeriv_measure_compProd_left μ ν κ] with p hp using by simp_rw [hp]
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.ChainRule (goal)
Goal:
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
κ : Kernel 𝓧 𝓨
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsMarkovKernel κ
h_ac : μ ≪ ν
⊢ ∫⁻ (p : 𝓧 × 𝓨), ENNReal.ofReal (klFun ((∂μ/∂ν) p.1).toReal) ∂ν ⊗ₘ κ =
    ∫⁻ (x : 𝓧), ENNReal.ofReal (klFun ((∂μ/∂ν) x).toReal) ∂ν
have rw : ∫⁻ (a : 𝓧), ∫⁻ (b : 𝓨), ENNReal.ofReal (klFun ((∂μ/∂ν) (a, b).1).toReal) ∂(κ : (a : 𝓧) → Measure 𝓨) a ∂ν =
  ∫⁻ (x : 𝓧), ENNReal.ofReal (klFun ((∂μ/∂ν) x).toReal) ∂ν
Tactic: rw [Measure.lintegral_compProd (by fun_prop)]
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.ChainRule (goal)
Goal:
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
κ : Kernel 𝓧 𝓨
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsMarkovKernel κ
h_ac : μ ≪ ν
⊢ ∫⁻ (x : 𝓧 × 𝓨), ENNReal.ofReal (klFun ((∂μ ⊗ₘ κ/∂ν ⊗ₘ κ) x).toReal) ∂ν ⊗ₘ κ =
    ∫⁻ (x : 𝓧), ENNReal.ofReal (klFun ((∂μ/∂ν) x).toReal) ∂ν
have calc : ∫⁻ (p : 𝓧 × 𝓨), ENNReal.ofReal (klFun ((∂μ ⊗ₘ κ/∂ν ⊗ₘ κ) p).toReal) ∂ν ⊗ₘ κ =
  ∫⁻ (p : 𝓧 × 𝓨), ENNReal.ofReal (klFun ((∂μ/∂ν) p.1).toReal) ∂ν ⊗ₘ κ
Tactic: calc ∫⁻ p, ENNReal.ofReal (klFun ((∂μ ⊗ₘ κ/∂ν ⊗ₘ κ) p).toReal) ∂(ν ⊗ₘ κ)
  _ = ∫⁻ p, ENNReal.ofReal (klFun ((∂μ/∂ν) p.1).toReal) ∂(ν ⊗ₘ κ) := by
    refine lintegral_congr_ae ?_
    filter_upwards [rnDeriv_measure_compProd_left μ ν κ] with p hp using by simp_rw [hp]
  _ = ∫⁻ x, ENNReal.ofReal (klFun ((∂μ/∂ν) x).toReal) ∂ν := by
    rw [Measure.lintegral_compProd (by fun_prop)]
    simp
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.ChainRule (goal)
Goal:
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
κ : Kernel 𝓧 𝓨
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsMarkovKernel κ
h_ac : μ ≪ ν
calc :
  ∫⁻ (p : 𝓧 × 𝓨), ENNReal.ofReal (klFun ((∂μ ⊗ₘ κ/∂ν ⊗ₘ κ) p).toReal) ∂ν ⊗ₘ κ =
    ∫⁻ (p : 𝓧 × 𝓨), ENNReal.ofReal (klFun ((∂μ/∂ν) p.1).toReal) ∂ν ⊗ₘ κ
⊢ ∫⁻ (x : 𝓧 × 𝓨), ENNReal.ofReal (klFun ((∂μ ⊗ₘ κ/∂ν ⊗ₘ κ) x).toReal) ∂ν ⊗ₘ κ =
    ∫⁻ (x : 𝓧), ENNReal.ofReal (klFun ((∂μ/∂ν) x).toReal) ∂ν
have calc₁ : ∫⁻ (p : 𝓧 × 𝓨), ENNReal.ofReal (klFun ((∂μ/∂ν) p.1).toReal) ∂ν ⊗ₘ κ =
  ∫⁻ (x : 𝓧), ENNReal.ofReal (klFun ((∂μ/∂ν) x).toReal) ∂ν
Tactic: calc ∫⁻ p, ENNReal.ofReal (klFun ((∂μ ⊗ₘ κ/∂ν ⊗ₘ κ) p).toReal) ∂(ν ⊗ₘ κ)
  _ = ∫⁻ p, ENNReal.ofReal (klFun ((∂μ/∂ν) p.1).toReal) ∂(ν ⊗ₘ κ) := by
    refine lintegral_congr_ae ?_
    filter_upwards [rnDeriv_measure_compProd_left μ ν κ] with p hp using by simp_rw [hp]
  _ = ∫⁻ x, ENNReal.ofReal (klFun ((∂μ/∂ν) x).toReal) ∂ν := by
    rw [Measure.lintegral_compProd (by fun_prop)]
    simp
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.ChainRule (goal)
Goal:
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
κ η : Kernel 𝓧 𝓨
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsMarkovKernel κ
inst_3 : IsMarkovKernel η
⊢ klDiv (μ ⊗ₘ κ) (ν ⊗ₘ η) = klDiv μ ν + klDiv (μ ⊗ₘ κ) (μ ⊗ₘ η)
have pos : ∀ (h_ac : μ ⊗ₘ κ ≪ ν ⊗ₘ η), klDiv (μ ⊗ₘ κ) (ν ⊗ₘ η) = klDiv μ ν + klDiv (μ ⊗ₘ κ) (μ ⊗ₘ η)
Tactic: by_cases h_ac : μ ⊗ₘ κ ≪ ν ⊗ₘ η
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.ChainRule (goal)
Goal:
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
κ η : Kernel 𝓧 𝓨
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsMarkovKernel κ
inst_3 : IsMarkovKernel η
pos : ∀ (h_ac : μ ⊗ₘ κ ≪ ν ⊗ₘ η), klDiv (μ ⊗ₘ κ) (ν ⊗ₘ η) = klDiv μ ν + klDiv (μ ⊗ₘ κ) (μ ⊗ₘ η)
⊢ klDiv (μ ⊗ₘ κ) (ν ⊗ₘ η) = klDiv μ ν + klDiv (μ ⊗ₘ κ) (μ ⊗ₘ η)
have neg : ∀ (h_ac : ¬μ ⊗ₘ κ ≪ ν ⊗ₘ η), klDiv (μ ⊗ₘ κ) (ν ⊗ₘ η) = klDiv μ ν + klDiv (μ ⊗ₘ κ) (μ ⊗ₘ η)
Tactic: by_cases h_ac : μ ⊗ₘ κ ≪ ν ⊗ₘ η
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.ChainRule (goal)
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 : ¬μ ⊗ₘ κ ≪ ν ⊗ₘ η
⊢ klDiv (μ ⊗ₘ κ) (ν ⊗ₘ η) = klDiv μ ν + klDiv (μ ⊗ₘ κ) (μ ⊗ₘ η)
have neg : ∞ = klDiv μ ν + klDiv (μ ⊗ₘ κ) (μ ⊗ₘ η)
Tactic: rw [klDiv_of_not_ac h_ac]
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.ChainRule (hypothesis)
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 : ¬μ ⊗ₘ κ ≪ ν ⊗ₘ η
⊢ ∞ = klDiv μ ν + klDiv (μ ⊗ₘ κ) (μ ⊗ₘ η)
have h_ac₁ : ¬(μ ≪ ν ∧ μ ⊗ₘ κ ≪ μ ⊗ₘ η)
Tactic: rw [Measure.absolutelyContinuous_compProd_iff] at h_ac
Cleared hypotheses: h_ac
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.ChainRule (hypothesis)
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 : ¬(μ ≪ ν ∧ μ ⊗ₘ κ ≪ μ ⊗ₘ η)
⊢ ∞ = klDiv μ ν + klDiv (μ ⊗ₘ κ) (μ ⊗ₘ η)
have h_ac₁ : ¬μ ≪ ν ∨ ¬μ ⊗ₘ κ ≪ μ ⊗ₘ η
Tactic: simp only [not_and_or] at h_ac
Cleared hypotheses: h_ac
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.ChainRule (goal)
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 : ¬μ ≪ ν ∨ ¬μ ⊗ₘ κ ≪ μ ⊗ₘ η
⊢ ∞ = klDiv μ ν + klDiv (μ ⊗ₘ κ) (μ ⊗ₘ η)
have neg : ∀ (h : ¬μ ≪ ν), ∞ = klDiv μ ν + klDiv (μ ⊗ₘ κ) (μ ⊗ₘ η)
Tactic: cases h_ac with
    | inl h => simp [h]
    | inr h => simp [h]
Cleared hypotheses: h_ac
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.ChainRule (goal)
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 : ¬μ ≪ ν ∨ ¬μ ⊗ₘ κ ≪ μ ⊗ₘ η
neg : ∀ (h : ¬μ ≪ ν), ∞ = klDiv μ ν + klDiv (μ ⊗ₘ κ) (μ ⊗ₘ η)
⊢ ∞ = klDiv μ ν + klDiv (μ ⊗ₘ κ) (μ ⊗ₘ η)
have neg₁ : ∀ (h : ¬μ ⊗ₘ κ ≪ μ ⊗ₘ η), ∞ = klDiv μ ν + klDiv (μ ⊗ₘ κ) (μ ⊗ₘ η)
Tactic: cases h_ac with
    | inl h => simp [h]
    | inr h => simp [h]
Cleared hypotheses: h_ac
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.ChainRule (goal)
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 : μ ⊗ₘ κ ≪ ν ⊗ₘ η
⊢ klDiv (μ ⊗ₘ κ) (ν ⊗ₘ η) = klDiv μ ν + klDiv (μ ⊗ₘ κ) (μ ⊗ₘ η)
have pos : ∀ (h_int : Integrable (llr (μ ⊗ₘ κ) (ν ⊗ₘ η)) (μ ⊗ₘ κ)), klDiv (μ ⊗ₘ κ) (ν ⊗ₘ η) = klDiv μ ν + klDiv (μ ⊗ₘ κ) (μ ⊗ₘ η)
Tactic: by_cases h_int : Integrable (llr (μ ⊗ₘ κ) (ν ⊗ₘ η)) (μ ⊗ₘ κ)
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.ChainRule (goal)
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 : μ ⊗ₘ κ ≪ ν ⊗ₘ η
pos :
  ∀ (h_int : Integrable (llr (μ ⊗ₘ κ) (ν ⊗ₘ η)) (μ ⊗ₘ κ)), klDiv (μ ⊗ₘ κ) (ν ⊗ₘ η) = klDiv μ ν + klDiv (μ ⊗ₘ κ) (μ ⊗ₘ η)
⊢ klDiv (μ ⊗ₘ κ) (ν ⊗ₘ η) = klDiv μ ν + klDiv (μ ⊗ₘ κ) (μ ⊗ₘ η)
have neg : ∀ (h_int : ¬Integrable (llr (μ ⊗ₘ κ) (ν ⊗ₘ η)) (μ ⊗ₘ κ)), klDiv (μ ⊗ₘ κ) (ν ⊗ₘ η) = klDiv μ ν + klDiv (μ ⊗ₘ κ) (μ ⊗ₘ η)
Tactic: by_cases h_int : Integrable (llr (μ ⊗ₘ κ) (ν ⊗ₘ η)) (μ ⊗ₘ κ)