awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 (llr μ ν) μ
h_int_κη : Integrable (llr (μ ⊗ₘ κ) (μ ⊗ₘ η)) (μ ⊗ₘ κ)
h_int1 : Integrable (ε := ℝ) (fun (p : 𝓧 × 𝓨) ↦ log ((∂μ/∂ν) p.1).toReal) (μ ⊗ₘ κ)
rw rw₁ : Eq (α := ℝ) (∫ (p : 𝓧 × 𝓨), llr (μ ⊗ₘ κ) (ν ⊗ₘ η) p ∂μ ⊗ₘ κ) (∫ (a : 𝓧 × 𝓨), llr (μ ⊗ₘ κ) (ν ⊗ₘ η) a ∂μ ⊗ₘ κ)
⊢ Eq (α := ℝ) (∫ (p : 𝓧 × 𝓨), llr (μ ⊗ₘ κ) (ν ⊗ₘ η) p ∂μ ⊗ₘ κ)
    (∫ (p : 𝓧 × 𝓨), ((∂μ ⊗ₘ κ/∂ν ⊗ₘ η) p).toReal * log ((∂μ ⊗ₘ κ/∂ν ⊗ₘ η) p).toReal ∂ν ⊗ₘ η)

Tactic:
rw [integral_rnDeriv_mul_log h_ac]

Premises used: MeasureTheory.integral_rnDeriv_mul_log
-- 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 (llr μ ν) μ
h_int_κη : Integrable (llr (μ ⊗ₘ κ) (μ ⊗ₘ η)) (μ ⊗ₘ κ)
h_int1 : Integrable (ε := ℝ) (fun (p : 𝓧 × 𝓨) ↦ log ((∂μ/∂ν) p.1).toReal) (μ ⊗ₘ κ)
⊢ Eq (α := ℝ) (∫ (p : 𝓧 × 𝓨), ((∂μ ⊗ₘ κ/∂ν ⊗ₘ η) p).toReal * log ((∂μ ⊗ₘ κ/∂ν ⊗ₘ η) p).toReal ∂ν ⊗ₘ η)
    (∫ (p : 𝓧 × 𝓨),
      ((∂μ ⊗ₘ κ/∂ν ⊗ₘ η) p).toReal * (log ((∂μ/∂ν) p.1).toReal + log ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p).toReal) ∂ν ⊗ₘ η)

Tactic:
integral_congr_ae (rnDeriv_compProd_mul_log_eq_mul_add h_ac_κη)

Premises used: InformationTheory.rnDeriv_compProd_mul_log_eq_mul_add, MeasureTheory.integral_congr_ae
-- 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 (llr μ ν) μ
h_int_κη : Integrable (llr (μ ⊗ₘ κ) (μ ⊗ₘ η)) (μ ⊗ₘ κ)
h_int1 : Integrable (ε := ℝ) (fun (p : 𝓧 × 𝓨) ↦ log ((∂μ/∂ν) p.1).toReal) (μ ⊗ₘ κ)
⊢ Eq (α := ℝ)
    (∫ (p : 𝓧 × 𝓨),
      ((∂μ ⊗ₘ κ/∂ν ⊗ₘ η) p).toReal * (log ((∂μ/∂ν) p.1).toReal + log ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p).toReal) ∂ν ⊗ₘ η)
    (∫ (p : 𝓧 × 𝓨), log ((∂μ/∂ν) p.1).toReal + log ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p).toReal ∂μ ⊗ₘ κ)

Tactic:
integral_rnDeriv_smul h_ac

Premises used: MeasureTheory.integral_rnDeriv_smul
-- 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 (llr μ ν) μ
h_int_κη : Integrable (llr (μ ⊗ₘ κ) (μ ⊗ₘ η)) (μ ⊗ₘ κ)
h_int1 : Integrable (ε := ℝ) (fun (p : 𝓧 × 𝓨) ↦ log ((∂μ/∂ν) p.1).toReal) (μ ⊗ₘ κ)
rw : Integrable (ε := ℝ) (fun (p : 𝓧 × 𝓨) ↦ log ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p).toReal) (μ ⊗ₘ κ)
⊢ ∫ (p : 𝓧 × 𝓨), log ((∂μ/∂ν) p.1).toReal + log ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p).toReal ∂μ ⊗ₘ κ =
    HAdd.hAdd (α := ℝ) (∫ (p : 𝓧 × 𝓨), log ((∂μ/∂ν) p.1).toReal ∂μ ⊗ₘ κ)
      (∫ (p : 𝓧 × 𝓨), log ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p).toReal ∂μ ⊗ₘ κ)

Tactic:
rw [integral_add h_int1]

Premises used: MeasureTheory.integral_add
-- 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 (llr μ ν) μ
h_int_κη : Integrable (llr (μ ⊗ₘ κ) (μ ⊗ₘ η)) (μ ⊗ₘ κ)
h_int1 : Integrable (ε := ℝ) (fun (p : 𝓧 × 𝓨) ↦ log ((∂μ/∂ν) p.1).toReal) (μ ⊗ₘ κ)
⊢ Integrable (ε := ℝ) (fun (p : 𝓧 × 𝓨) ↦ log ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p).toReal) (μ ⊗ₘ κ)

Tactic:
h_int_κη.ofReal

Premises used: MeasureTheory.llr, Real.log, dite, MeasureTheory.Integrable.ofReal
-- 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 (llr μ ν) μ
h_int_κη : Integrable (llr (μ ⊗ₘ κ) (μ ⊗ₘ η)) (μ ⊗ₘ κ)
h_int1 : Integrable (ε := ℝ) (fun (p : 𝓧 × 𝓨) ↦ log ((∂μ/∂ν) p.1).toReal) (μ ⊗ₘ κ)
⊢ Integrable (ε := ℝ) (fun (p : 𝓧 × 𝓨) ↦ log ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p).toReal) (μ ⊗ₘ κ)

Tactic:
exact h_int_κη.ofReal

Premises used: MeasureTheory.Integrable.ofReal
-- 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 (llr μ ν) μ
h_int_κη : Integrable (llr (μ ⊗ₘ κ) (μ ⊗ₘ η)) (μ ⊗ₘ κ)
h_int1 : Integrable (ε := ℝ) (fun (p : 𝓧 × 𝓨) ↦ log ((∂μ/∂ν) p.1).toReal) (μ ⊗ₘ κ)
e_a : Eq (α := ℝ) (∫ (p : 𝓧 × 𝓨), log ((∂μ/∂ν) p.1).toReal ∂μ ⊗ₘ κ) (∫ (a : 𝓧), llr μ ν a ∂μ)
⊢ HAdd.hAdd (α := ℝ) (∫ (p : 𝓧 × 𝓨), log ((∂μ/∂ν) p.1).toReal ∂μ ⊗ₘ κ)
      (∫ (p : 𝓧 × 𝓨), log ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p).toReal ∂μ ⊗ₘ κ) =
    HAdd.hAdd (α := ℝ) (∫ (a : 𝓧), llr μ ν a ∂μ) (∫ (p : 𝓧 × 𝓨), llr (μ ⊗ₘ κ) (μ ⊗ₘ η) p ∂μ ⊗ₘ κ)

Tactic:
congr
-- 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 (llr μ ν) μ
h_int_κη : Integrable (llr (μ ⊗ₘ κ) (μ ⊗ₘ η)) (μ ⊗ₘ κ)
h_int1 : Integrable (ε := ℝ) (fun (p : 𝓧 × 𝓨) ↦ log ((∂μ/∂ν) p.1).toReal) (μ ⊗ₘ κ)
e_a :
  Eq (α := ℝ)
    (∫ (a : 𝓧), @integral _ _ _ _ m𝓨 ((κ : (a : 𝓧) → Measure 𝓨) a) fun (b : 𝓨) ↦ log ((∂μ/∂ν) (a, b).1).toReal ∂μ)
    (∫ (a : 𝓧), llr μ ν a ∂μ)
⊢ Eq (α := ℝ) (∫ (p : 𝓧 × 𝓨), log ((∂μ/∂ν) p.1).toReal ∂μ ⊗ₘ κ) (∫ (a : 𝓧), llr μ ν a ∂μ)

Tactic:
rw [Measure.integral_compProd h_int1]

Premises used: MeasureTheory.Measure.integral_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 : μ ⊗ₘ κ ≪ ν ⊗ₘ η
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 (α := ℝ)
    (∫ (a : 𝓧), @integral _ _ _ _ m𝓨 ((κ : (a : 𝓧) → Measure 𝓨) a) fun (b : 𝓨) ↦ log ((∂μ/∂ν) (a, b).1).toReal ∂μ)
    (∫ (a : 𝓧), llr μ ν a ∂μ)

Tactic:
simp [llr]

Premises used: MeasureTheory.llr
-- 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 (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 ∂μ ⊗ₘ κ)
calc₂ :
  HAdd.hAdd (α := ℝ) (∫ (p : 𝓧 × 𝓨), log ((∂μ/∂ν) p.1).toReal ∂μ ⊗ₘ κ)
      (∫ (p : 𝓧 × 𝓨), log ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p).toReal ∂μ ⊗ₘ κ) =
    HAdd.hAdd (α := ℝ) (∫ (a : 𝓧), llr μ ν a ∂μ) (∫ (p : 𝓧 × 𝓨), llr (μ ⊗ₘ κ) (μ ⊗ₘ η) p ∂μ ⊗ₘ κ)
⊢ ∫ (p : 𝓧 × 𝓨), llr (μ ⊗ₘ κ) (ν ⊗ₘ η) p ∂μ ⊗ₘ κ =
    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]

Premises used: InformationTheory.rnDeriv_compProd_mul_log_eq_mul_add, MeasureTheory.integral_congr_ae, MeasureTheory.integral_rnDeriv_smul, 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 κ
pos : ∀ (h_ac : μ ⊗ₘ κ ≪ ν ⊗ₘ κ), klDiv (μ ⊗ₘ κ) (ν ⊗ₘ κ) = klDiv μ ν
neg : ∀ (h_ac : ¬μ ⊗ₘ κ ≪ ν ⊗ₘ κ), klDiv (μ ⊗ₘ κ) (ν ⊗ₘ κ) = klDiv μ ν
⊢ klDiv (μ ⊗ₘ κ) (ν ⊗ₘ κ) = klDiv μ ν

Tactic:
by_cases 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 κ
h_ac : ¬μ ⊗ₘ κ ≪ ν ⊗ₘ κ
neg : ¬μ ≪ ν
⊢ klDiv (μ ⊗ₘ κ) (ν ⊗ₘ κ) = klDiv μ ν

Tactic:
rw [klDiv_of_not_ac h_ac, klDiv_of_not_ac]

Premises used: InformationTheory.klDiv_of_not_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 κ
h_ac : ¬μ ⊗ₘ κ ≪ ν ⊗ₘ κ
neg neg₁ neg₂ neg₃ : ∀ (h_ac : ¬μ ≪ ν), ¬μ ≪ ν
⊢ ¬μ ≪ ν

Tactic:
rwa [Measure.absolutelyContinuous_compProd_left_iff] at h_ac

Premises used: MeasureTheory.Measure.absolutelyContinuous_compProd_left_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 κ
h_ac : μ ⊗ₘ κ ≪ ν ⊗ₘ κ
pos :
  ∫⁻ (x : 𝓧 × 𝓨), ENNReal.ofReal (klFun ((∂μ ⊗ₘ κ/∂ν ⊗ₘ κ) x).toReal) ∂ν ⊗ₘ κ =
    ∫⁻ (x : 𝓧), ENNReal.ofReal (klFun ((∂μ/∂ν) x).toReal) ∂ν
⊢ klDiv (μ ⊗ₘ κ) (ν ⊗ₘ κ) = klDiv μ ν

Tactic:
rw [klDiv_eq_lintegral_klFun_of_ac h_ac,
    klDiv_eq_lintegral_klFun_of_ac (Measure.absolutelyContinuous_compProd_left_iff.mp h_ac)]

Premises used: InformationTheory.klDiv_eq_lintegral_klFun_of_ac, MeasureTheory.Measure.absolutelyContinuous_compProd_left_iff, Iff.mp
-- 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 κ
h_ac : μ ⊗ₘ κ ≪ ν ⊗ₘ κ
⊢ μ ≪ ν

Tactic:
rw [Measure.absolutelyContinuous_compProd_left_iff] at h_ac

Premises used: MeasureTheory.Measure.absolutelyContinuous_compProd_left_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 κ
h_ac : μ ≪ ν
⊢ ∫⁻ (p : 𝓧 × 𝓨), ENNReal.ofReal (klFun ((∂μ ⊗ₘ κ/∂ν ⊗ₘ κ) p).toReal) ∂ν ⊗ₘ κ =
    ∫⁻ (p : 𝓧 × 𝓨), ENNReal.ofReal (klFun ((∂μ/∂ν) p.1).toReal) ∂ν ⊗ₘ κ

Tactic:
lintegral_congr_ae ?_

Premises used: MeasureTheory.lintegral_congr_ae
-- 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 κ
h_ac : μ ≪ ν
refine :
  (ae (ν ⊗ₘ κ)).EventuallyEq (β := ℝ≥0∞) (fun (p : 𝓧 × 𝓨) ↦ ENNReal.ofReal (klFun ((∂μ ⊗ₘ κ/∂ν ⊗ₘ κ) p).toReal))
    fun (p : 𝓧 × 𝓨) ↦ ENNReal.ofReal (klFun ((∂μ/∂ν) p.1).toReal)
⊢ ∫⁻ (p : 𝓧 × 𝓨), ENNReal.ofReal (klFun ((∂μ ⊗ₘ κ/∂ν ⊗ₘ κ) p).toReal) ∂ν ⊗ₘ κ =
    ∫⁻ (p : 𝓧 × 𝓨), ENNReal.ofReal (klFun ((∂μ/∂ν) p.1).toReal) ∂ν ⊗ₘ κ

Tactic:
refine lintegral_congr_ae ?_

Premises used: MeasureTheory.lintegral_congr_ae
-- 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 κ
h_ac : μ ≪ ν
p : 𝓧 × 𝓨
hp : (∂μ ⊗ₘ κ/∂ν ⊗ₘ κ) p = (∂μ/∂ν) p.1
⊢ ENNReal.ofReal (klFun ((∂μ ⊗ₘ κ/∂ν ⊗ₘ κ) p).toReal) = ENNReal.ofReal (klFun ((∂μ/∂ν) p.1).toReal)

Tactic:
simp_rw [hp]
-- 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 κ
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
h₁ h₂ :
  ∀ (p : 𝓧 × 𝓨) (hp : (∂μ ⊗ₘ κ/∂ν ⊗ₘ κ) p = (∂μ/∂ν) p.1),
    ENNReal.ofReal (klFun ((∂μ ⊗ₘ κ/∂ν ⊗ₘ κ) p).toReal) = ENNReal.ofReal (klFun ((∂μ/∂ν) p.1).toReal)
⊢ (ae (ν ⊗ₘ κ)).EventuallyEq (β := ℝ≥0∞) (fun (p : 𝓧 × 𝓨) ↦ ENNReal.ofReal (klFun ((∂μ ⊗ₘ κ/∂ν ⊗ₘ κ) p).toReal))
    fun (p : 𝓧 × 𝓨) ↦ ENNReal.ofReal (klFun ((∂μ/∂ν) p.1).toReal)

Tactic:
filter_upwards [rnDeriv_measure_compProd_left μ ν κ] with p hp using by simp_rw [hp]

Premises used: ProbabilityTheory.rnDeriv_measure_compProd_left
-- 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 κ
h_ac : μ ≪ ν
⊢ Measurable (β := ℝ≥0∞) fun (p : 𝓧 × 𝓨) ↦ ENNReal.ofReal (klFun ((∂μ/∂ν) p.1).toReal)

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 κ
h_ac : μ ≪ ν
rw :
  ∫⁻ (a : 𝓧), ∫⁻ (b : 𝓨), ENNReal.ofReal (klFun ((∂μ/∂ν) (a, b).1).toReal) ∂(κ : (a : 𝓧) → Measure 𝓨) a ∂ν =
    ∫⁻ (x : 𝓧), ENNReal.ofReal (klFun ((∂μ/∂ν) x).toReal) ∂ν
⊢ ∫⁻ (p : 𝓧 × 𝓨), ENNReal.ofReal (klFun ((∂μ/∂ν) p.1).toReal) ∂ν ⊗ₘ κ =
    ∫⁻ (x : 𝓧), ENNReal.ofReal (klFun ((∂μ/∂ν) x).toReal) ∂ν

Tactic:
rw [Measure.lintegral_compProd (by fun_prop)]

Premises used: MeasureTheory.Measure.lintegral_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 κ
h_ac : μ ≪ ν
⊢ ∫⁻ (a : 𝓧), ∫⁻ (b : 𝓨), ENNReal.ofReal (klFun ((∂μ/∂ν) (a, b).1).toReal) ∂(κ : (a : 𝓧) → Measure 𝓨) a ∂ν =
    ∫⁻ (x : 𝓧), ENNReal.ofReal (klFun ((∂μ/∂ν) x).toReal) ∂ν

Tactic:
simp
-- 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 κ
h_ac : μ ≪ ν
calc :
  ∫⁻ (p : 𝓧 × 𝓨), ENNReal.ofReal (klFun ((∂μ ⊗ₘ κ/∂ν ⊗ₘ κ) p).toReal) ∂ν ⊗ₘ κ =
    ∫⁻ (p : 𝓧 × 𝓨), ENNReal.ofReal (klFun ((∂μ/∂ν) p.1).toReal) ∂ν ⊗ₘ κ
calc₁ :
  ∫⁻ (p : 𝓧 × 𝓨), ENNReal.ofReal (klFun ((∂μ/∂ν) p.1).toReal) ∂ν ⊗ₘ κ =
    ∫⁻ (x : 𝓧), ENNReal.ofReal (klFun ((∂μ/∂ν) x).toReal) ∂ν
⊢ ∫⁻ (x : 𝓧 × 𝓨), ENNReal.ofReal (klFun ((∂μ ⊗ₘ κ/∂ν ⊗ₘ κ) x).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

Premises used: 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 η
pos : ∀ (h_ac : μ ⊗ₘ κ ≪ ν ⊗ₘ η), klDiv (μ ⊗ₘ κ) (ν ⊗ₘ η) = klDiv μ ν + klDiv (μ ⊗ₘ κ) (μ ⊗ₘ η)
neg : ∀ (h_ac : ¬μ ⊗ₘ κ ≪ ν ⊗ₘ η), klDiv (μ ⊗ₘ κ) (ν ⊗ₘ η) = klDiv μ ν + klDiv (μ ⊗ₘ κ) (μ ⊗ₘ η)
⊢ klDiv (μ ⊗ₘ κ) (ν ⊗ₘ η) = klDiv μ ν + klDiv (μ ⊗ₘ κ) (μ ⊗ₘ η)

Tactic:
by_cases 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 : ¬μ ⊗ₘ κ ≪ ν ⊗ₘ η
neg : ∞ = klDiv μ ν + klDiv (μ ⊗ₘ κ) (μ ⊗ₘ η)
⊢ klDiv (μ ⊗ₘ κ) (ν ⊗ₘ η) = klDiv μ ν + klDiv (μ ⊗ₘ κ) (μ ⊗ₘ η)

Tactic:
rw [klDiv_of_not_ac h_ac]

Premises used: InformationTheory.klDiv_of_not_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 : ¬μ ⊗ₘ κ ≪ ν ⊗ₘ η
⊢ ¬(μ ≪ ν ∧ μ ⊗ₘ κ ≪ μ ⊗ₘ η)

Tactic:
rw [Measure.absolutelyContinuous_compProd_iff] at h_ac

Premises used: MeasureTheory.Measure.absolutelyContinuous_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 : ¬(μ ≪ ν ∧ μ ⊗ₘ κ ≪ μ ⊗ₘ η)
⊢ ¬μ ≪ ν ∨ ¬μ ⊗ₘ κ ≪ μ ⊗ₘ η

Tactic:
simp only [not_and_or] at h_ac

Premises used: not_and_or
-- 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 : ¬μ ≪ ν
⊢ ∞ = klDiv μ ν + klDiv (μ ⊗ₘ κ) (μ ⊗ₘ η)

Tactic:
simp [h]
-- 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 : ¬μ ⊗ₘ κ ≪ μ ⊗ₘ η
⊢ ∞ = klDiv μ ν + klDiv (μ ⊗ₘ κ) (μ ⊗ₘ η)

Tactic:
simp [h]
-- 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 : ¬μ ≪ ν ∨ ¬μ ⊗ₘ κ ≪ μ ⊗ₘ η
neg : ∀ (h : ¬μ ≪ ν), ∞ = klDiv μ ν + klDiv (μ ⊗ₘ κ) (μ ⊗ₘ η)
neg₁ : ∀ (h : ¬μ ⊗ₘ κ ≪ μ ⊗ₘ η), ∞ = klDiv μ ν + klDiv (μ ⊗ₘ κ) (μ ⊗ₘ η)
⊢ ∞ = klDiv μ ν + klDiv (μ ⊗ₘ κ) (μ ⊗ₘ η)

Tactic:
cases h_ac with
    | inl h => simp [h]
    | inr h => simp [h]
-- 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 : μ ⊗ₘ κ ≪ ν ⊗ₘ η
pos :
  ∀ (h_int : Integrable (llr (μ ⊗ₘ κ) (ν ⊗ₘ η)) (μ ⊗ₘ κ)), klDiv (μ ⊗ₘ κ) (ν ⊗ₘ η) = klDiv μ ν + klDiv (μ ⊗ₘ κ) (μ ⊗ₘ η)
neg :
  ∀ (h_int : ¬Integrable (llr (μ ⊗ₘ κ) (ν ⊗ₘ η)) (μ ⊗ₘ κ)),
    klDiv (μ ⊗ₘ κ) (ν ⊗ₘ η) = klDiv μ ν + klDiv (μ ⊗ₘ κ) (μ ⊗ₘ η)
⊢ klDiv (μ ⊗ₘ κ) (ν ⊗ₘ η) = klDiv μ ν + klDiv (μ ⊗ₘ κ) (μ ⊗ₘ η)

Tactic:
by_cases h_int : Integrable (llr (μ ⊗ₘ κ) (ν ⊗ₘ η)) (μ ⊗ₘ κ)

Premises used: MeasureTheory.Integrable, MeasureTheory.llr, 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 : μ ⊗ₘ κ ≪ ν ⊗ₘ η
h_int : ¬Integrable (llr (μ ⊗ₘ κ) (ν ⊗ₘ η)) (μ ⊗ₘ κ)
neg : ∞ = klDiv μ ν + klDiv (μ ⊗ₘ κ) (μ ⊗ₘ η)
⊢ klDiv (μ ⊗ₘ κ) (ν ⊗ₘ η) = klDiv μ ν + klDiv (μ ⊗ₘ κ) (μ ⊗ₘ η)

Tactic:
rw [klDiv_of_not_integrable h_int]

Premises used: InformationTheory.klDiv_of_not_integrable
-- 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 (μ ⊗ₘ κ) (ν ⊗ₘ η)) (μ ⊗ₘ κ)
⊢ ¬(Integrable (llr μ ν) μ ∧ Integrable (llr (μ ⊗ₘ κ) (μ ⊗ₘ η)) (μ ⊗ₘ κ))

Tactic:
rw [integrable_llr_compProd_iff h_ac] at h_int

Premises used: InformationTheory.integrable_llr_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_int : ¬(Integrable (llr μ ν) μ ∧ Integrable (llr (μ ⊗ₘ κ) (μ ⊗ₘ η)) (μ ⊗ₘ κ))
⊢ ¬Integrable (llr μ ν) μ ∨ ¬Integrable (llr (μ ⊗ₘ κ) (μ ⊗ₘ η)) (μ ⊗ₘ κ)

Tactic:
simp only [not_and_or] at h_int

Premises used: not_and_or
-- 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 : ¬Integrable (llr μ ν) μ
⊢ ∞ = klDiv μ ν + klDiv (μ ⊗ₘ κ) (μ ⊗ₘ η)

Tactic:
simp [h]