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

Tactic:
cases h_int 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 : μ ⊗ₘ κ ≪ ν ⊗ₘ η
h_int : Integrable (llr (μ ⊗ₘ κ) (ν ⊗ₘ η)) (μ ⊗ₘ κ)
h_ac_μν : μ ≪ ν
h_ac_κη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
h_int_μν : Integrable (llr μ ν) μ
h_int_κη : Integrable (llr (μ ⊗ₘ κ) (μ ⊗ₘ η)) (μ ⊗ₘ κ)
pos :
  ENNReal.ofReal
      (∫ (x : 𝓧 × 𝓨), llr (μ ⊗ₘ κ) (ν ⊗ₘ η) x ∂μ ⊗ₘ κ + ENNReal.toReal ((ν : (a : Set 𝓧) → ℝ≥0∞) univ) -
        ENNReal.toReal ((μ : (a : Set 𝓧) → ℝ≥0∞) univ)) =
    ENNReal.ofReal
      (∫ (x : 𝓧), llr μ ν x ∂μ + ENNReal.toReal ((ν : (a : Set 𝓧) → ℝ≥0∞) univ) -
          ENNReal.toReal ((μ : (a : Set 𝓧) → ℝ≥0∞) univ) +
        ∫ (x : 𝓧 × 𝓨), llr (μ ⊗ₘ κ) (μ ⊗ₘ η) x ∂μ ⊗ₘ κ)
⊢ klDiv (μ ⊗ₘ κ) (ν ⊗ₘ η) = klDiv μ ν + klDiv (μ ⊗ₘ κ) (μ ⊗ₘ η)

Tactic:
simp_rw [klDiv_of_ac_of_integrable h_ac h_int, klDiv_of_ac_of_integrable h_ac_μν h_int_μν,
    klDiv_of_ac_of_integrable h_ac_κη h_int_κη,
    ← ENNReal.ofReal_add (integral_llr_add_sub_measure_univ_nonneg h_ac_μν h_int_μν)
    (integral_llr_add_sub_measure_univ_nonneg h_ac_κη h_int_κη), measureReal_def,
    Measure.compProd_apply_univ, add_sub_cancel_right]

Premises used: InformationTheory.integral_llr_add_sub_measure_univ_nonneg, MeasureTheory.Measure.compProd_apply_univ, InformationTheory.klDiv_of_ac_of_integrable, ENNReal.ofReal_add, MeasureTheory.measureReal_def, add_sub_cancel_right
-- 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 (μ ⊗ₘ κ) (μ ⊗ₘ η)) (μ ⊗ₘ κ)
this :
  ∫ (p : 𝓧 × 𝓨), llr (μ ⊗ₘ κ) (ν ⊗ₘ η) p ∂μ ⊗ₘ κ =
    HAdd.hAdd (α := ℝ) (∫ (a : 𝓧), llr μ ν a ∂μ) (∫ (p : 𝓧 × 𝓨), llr (μ ⊗ₘ κ) (μ ⊗ₘ η) p ∂μ ⊗ₘ κ)
rw :
  ENNReal.ofReal
      (HAdd.hAdd (α := ℝ) (∫ (a : 𝓧), llr μ ν a ∂μ) (∫ (p : 𝓧 × 𝓨), llr (μ ⊗ₘ κ) (μ ⊗ₘ η) p ∂μ ⊗ₘ κ) +
          ENNReal.toReal ((ν : (a : Set 𝓧) → ℝ≥0∞) univ) -
        ENNReal.toReal ((μ : (a : Set 𝓧) → ℝ≥0∞) univ)) =
    ENNReal.ofReal
      (∫ (x : 𝓧), llr μ ν x ∂μ + ENNReal.toReal ((ν : (a : Set 𝓧) → ℝ≥0∞) univ) -
          ENNReal.toReal ((μ : (a : Set 𝓧) → ℝ≥0∞) univ) +
        ∫ (x : 𝓧 × 𝓨), llr (μ ⊗ₘ κ) (μ ⊗ₘ η) x ∂μ ⊗ₘ κ)
⊢ ENNReal.ofReal
      (∫ (x : 𝓧 × 𝓨), llr (μ ⊗ₘ κ) (ν ⊗ₘ η) x ∂μ ⊗ₘ κ + ENNReal.toReal ((ν : (a : Set 𝓧) → ℝ≥0∞) univ) -
        ENNReal.toReal ((μ : (a : Set 𝓧) → ℝ≥0∞) univ)) =
    ENNReal.ofReal
      (∫ (x : 𝓧), llr μ ν x ∂μ + ENNReal.toReal ((ν : (a : Set 𝓧) → ℝ≥0∞) univ) -
          ENNReal.toReal ((μ : (a : Set 𝓧) → ℝ≥0∞) univ) +
        ∫ (x : 𝓧 × 𝓨), llr (μ ⊗ₘ κ) (μ ⊗ₘ η) x ∂μ ⊗ₘ κ)

Tactic:
rw [this]
-- 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 (μ ⊗ₘ κ) (μ ⊗ₘ η)) (μ ⊗ₘ κ)
this :
  ∫ (p : 𝓧 × 𝓨), llr (μ ⊗ₘ κ) (ν ⊗ₘ η) p ∂μ ⊗ₘ κ =
    HAdd.hAdd (α := ℝ) (∫ (a : 𝓧), llr μ ν a ∂μ) (∫ (p : 𝓧 × 𝓨), llr (μ ⊗ₘ κ) (μ ⊗ₘ η) p ∂μ ⊗ₘ κ)
⊢ ENNReal.ofReal
      (HAdd.hAdd (α := ℝ) (∫ (a : 𝓧), llr μ ν a ∂μ) (∫ (p : 𝓧 × 𝓨), llr (μ ⊗ₘ κ) (μ ⊗ₘ η) p ∂μ ⊗ₘ κ) +
          ENNReal.toReal ((ν : (a : Set 𝓧) → ℝ≥0∞) univ) -
        ENNReal.toReal ((μ : (a : Set 𝓧) → ℝ≥0∞) univ)) =
    ENNReal.ofReal
      (∫ (x : 𝓧), llr μ ν x ∂μ + ENNReal.toReal ((ν : (a : Set 𝓧) → ℝ≥0∞) univ) -
          ENNReal.toReal ((μ : (a : Set 𝓧) → ℝ≥0∞) univ) +
        ∫ (x : 𝓧 × 𝓨), llr (μ ⊗ₘ κ) (μ ⊗ₘ η) x ∂μ ⊗ₘ κ)

Tactic:
ring_nf
-- 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 (μ ⊗ₘ κ) (μ ⊗ₘ η)) (μ ⊗ₘ κ)
pos :
  ∫ (p : 𝓧 × 𝓨), llr (μ ⊗ₘ κ) (ν ⊗ₘ η) p ∂μ ⊗ₘ κ =
    HAdd.hAdd (α := ℝ) (∫ (a : 𝓧), llr μ ν a ∂μ) (∫ (p : 𝓧 × 𝓨), llr (μ ⊗ₘ κ) (μ ⊗ₘ η) p ∂μ ⊗ₘ κ)
⊢ ENNReal.ofReal
      (∫ (x : 𝓧 × 𝓨), llr (μ ⊗ₘ κ) (ν ⊗ₘ η) x ∂μ ⊗ₘ κ + ENNReal.toReal ((ν : (a : Set 𝓧) → ℝ≥0∞) univ) -
        ENNReal.toReal ((μ : (a : Set 𝓧) → ℝ≥0∞) univ)) =
    ENNReal.ofReal
      (∫ (x : 𝓧), llr μ ν x ∂μ + ENNReal.toReal ((ν : (a : Set 𝓧) → ℝ≥0∞) univ) -
          ENNReal.toReal ((μ : (a : Set 𝓧) → ℝ≥0∞) univ) +
        ∫ (x : 𝓧 × 𝓨), llr (μ ⊗ₘ κ) (μ ⊗ₘ η) x ∂μ ⊗ₘ κ)

Tactic:
suffices ∫ p, llr (μ ⊗ₘ κ) (ν ⊗ₘ η) p ∂μ ⊗ₘ κ =
      ∫ a, llr μ ν a ∂μ + ∫ p, llr (μ ⊗ₘ κ) (μ ⊗ₘ η) p ∂(μ ⊗ₘ κ) by rw [this]; ring_nf
-- 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 (μ ⊗ₘ κ) (μ ⊗ₘ η)) (μ ⊗ₘ κ)
⊢ ∫ (p : 𝓧 × 𝓨), llr (μ ⊗ₘ κ) (ν ⊗ₘ η) p ∂μ ⊗ₘ κ =
    HAdd.hAdd (α := ℝ) (∫ (a : 𝓧), llr μ ν a ∂μ) (∫ (p : 𝓧 × 𝓨), llr (μ ⊗ₘ κ) (μ ⊗ₘ η) p ∂μ ⊗ₘ κ)

Tactic:
integral_llr_compProd_eq_add h_ac h_int

Premises used: InformationTheory.integral_llr_compProd_eq_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 (μ ⊗ₘ κ) (μ ⊗ₘ η)) (μ ⊗ₘ κ)
⊢ ∫ (p : 𝓧 × 𝓨), llr (μ ⊗ₘ κ) (ν ⊗ₘ η) p ∂μ ⊗ₘ κ =
    HAdd.hAdd (α := ℝ) (∫ (a : 𝓧), llr μ ν a ∂μ) (∫ (p : 𝓧 × 𝓨), llr (μ ⊗ₘ κ) (μ ⊗ₘ η) p ∂μ ⊗ₘ κ)

Tactic:
exact integral_llr_compProd_eq_add h_ac h_int

Premises used: InformationTheory.integral_llr_compProd_eq_add
-- Module: Mathlib.InformationTheory.KullbackLeibler.KLFun
Goal:
x : ℝ
⊢ klFun x = x * log x + 1 - x

Tactic:
rfl

Premises used: InformationTheory.klFun, rfl
-- Module: Mathlib.InformationTheory.KullbackLeibler.KLFun
Goal:
⊢ klFun 0 = 1

Tactic:
simp [klFun]

Premises used: InformationTheory.klFun
-- Module: Mathlib.InformationTheory.KullbackLeibler.KLFun
Goal:
⊢ klFun 1 = 0

Tactic:
simp [klFun]

Premises used: InformationTheory.klFun
-- Module: Mathlib.InformationTheory.KullbackLeibler.KLFun
Goal:
⊢ StrictConvexOn ℝ (Ici 0) klFun

Tactic:
(strictConvexOn_mul_log.add_convexOn (convexOn_const _ (convex_Ici _))).sub_concaveOn
    (concaveOn_id (convex_Ici _))

Premises used: concaveOn_id, Real.strictConvexOn_mul_log, convex_Ici, InformationTheory.klFun, StrictConvexOn.add_convexOn, convexOn_const, StrictConvexOn.sub_concaveOn
-- Module: Mathlib.InformationTheory.KullbackLeibler.KLFun
Goal:
⊢ ConvexOn ℝ (Ici 0) klFun

Tactic:
strictConvexOn_klFun.convexOn

Premises used: InformationTheory.strictConvexOn_klFun, StrictConvexOn.convexOn
-- Module: Mathlib.InformationTheory.KullbackLeibler.KLFun
Goal:
⊢ ConvexOn ℝ (Ioi 0) klFun

Tactic:
convexOn_klFun.subset (Ioi_subset_Ici le_rfl) (convex_Ioi _)

Premises used: le_rfl, InformationTheory.convexOn_klFun, Set.Ioi_subset_Ici, convex_Ioi, ConvexOn.subset
-- Module: Mathlib.InformationTheory.KullbackLeibler.KLFun
Goal:
funProp funProp₁ : ∀ (x : ℝ), x ≠ 0
⊢ Continuous (Y := ℝ) fun (x : ℝ) ↦ x * log x + 1 - x

Tactic:
fun_prop
-- Module: Mathlib.InformationTheory.KullbackLeibler.KLFun
Goal:
⊢ Measurable klFun

Tactic:
continuous_klFun.measurable

Premises used: InformationTheory.continuous_klFun, Continuous.measurable
-- Module: Mathlib.InformationTheory.KullbackLeibler.KLFun
Goal:
⊢ StronglyMeasurable klFun

Tactic:
measurable_klFun.stronglyMeasurable

Premises used: InformationTheory.measurable_klFun, Measurable.stronglyMeasurable
-- Module: Mathlib.InformationTheory.KullbackLeibler.KLFun
Goal:
x : ℝ
hx : x ≠ 0
⊢ HasDerivAt ((HAdd.hAdd (α := ℝ → ℝ) (fun (x : ℝ) ↦ x * log x) fun (x : ℝ) ↦ 1) - id) (log x + 1 + 0 - 1) x

Tactic:
((hasDerivAt_mul_log hx).add (hasDerivAt_const x 1)).sub (hasDerivAt_id x)

Premises used: Real.hasDerivAt_mul_log, HasDerivAt.add, HasDerivAt.sub, hasDerivAt_const, hasDerivAt_id, OfNat.ofNat
-- Module: Mathlib.InformationTheory.KullbackLeibler.KLFun
Goal:
x : ℝ
hx : x ≠ 0
h : log x = log x + 1 + 0 - 1
⊢ HasDerivAt klFun (log x) x

Tactic:
convert! ((hasDerivAt_mul_log hx).add (hasDerivAt_const x 1)).sub (hasDerivAt_id x) using 1

Premises used: Real.hasDerivAt_mul_log, HasDerivAt.add, HasDerivAt.sub, hasDerivAt_const, hasDerivAt_id, OfNat.ofNat
-- Module: Mathlib.InformationTheory.KullbackLeibler.KLFun
Goal:
x : ℝ
hx : x ≠ 0
⊢ log x = log x + 1 + 0 - 1

Tactic:
ring
-- Module: Mathlib.InformationTheory.KullbackLeibler.KLFun
Goal:
⊢ ¬DifferentiableAt ℝ (F := ℝ) (fun (x : ℝ) ↦ x * log x + 1 - x) 0

Tactic:
simpa using not_DifferentiableAt_log_mul_zero

Premises used: Real.not_DifferentiableAt_log_mul_zero
-- Module: Mathlib.InformationTheory.KullbackLeibler.KLFun
Goal:
h : ∀ (x : ℝ), deriv klFun x = log x
⊢ deriv klFun = log

Tactic:
ext x
-- Module: Mathlib.InformationTheory.KullbackLeibler.KLFun
Goal:
x : ℝ
pos : ∀ (h0 : x = 0), deriv klFun x = log x
neg : ∀ (h0 : ¬x = 0), deriv klFun x = log x
⊢ deriv klFun x = log x

Tactic:
by_cases h0 : x = 0
-- Module: Mathlib.InformationTheory.KullbackLeibler.KLFun
Goal:
x : ℝ
h0 : x = 0
pos : deriv klFun 0 = 0
⊢ deriv klFun x = log x

Tactic:
simp only [h0, log_zero]

Premises used: Real.log_zero
-- Module: Mathlib.InformationTheory.KullbackLeibler.KLFun
Goal:
x : ℝ
h0 : x = 0
⊢ deriv klFun 0 = 0

Tactic:
deriv_zero_of_not_differentiableAt not_differentiableAt_klFun_zero

Premises used: deriv_zero_of_not_differentiableAt, InformationTheory.not_differentiableAt_klFun_zero
-- Module: Mathlib.InformationTheory.KullbackLeibler.KLFun
Goal:
x : ℝ
h0 : x = 0
⊢ deriv klFun 0 = 0

Tactic:
exact deriv_zero_of_not_differentiableAt not_differentiableAt_klFun_zero

Premises used: deriv_zero_of_not_differentiableAt, InformationTheory.not_differentiableAt_klFun_zero
-- Module: Mathlib.InformationTheory.KullbackLeibler.KLFun
Goal:
x : ℝ
h0 : ¬x = 0
⊢ deriv klFun x = log x

Tactic:
(hasDerivAt_klFun h0).deriv

Premises used: InformationTheory.hasDerivAt_klFun, HasDerivAt.deriv
-- Module: Mathlib.InformationTheory.KullbackLeibler.KLFun
Goal:
x : ℝ
h0 : ¬x = 0
⊢ deriv klFun x = log x

Tactic:
exact (hasDerivAt_klFun h0).deriv

Premises used: InformationTheory.hasDerivAt_klFun, HasDerivAt.deriv
-- Module: Mathlib.InformationTheory.KullbackLeibler.KLFun
Goal:
⊢ ¬DifferentiableWithinAt ℝ klFun (Ioi 0) 0

Tactic:
not_differentiableWithinAt_of_deriv_tendsto_atBot_Ioi _ ?_

Premises used: not_differentiableWithinAt_of_deriv_tendsto_atBot_Ioi
-- Module: Mathlib.InformationTheory.KullbackLeibler.KLFun
Goal:
refine : Tendsto (deriv klFun) (nhdsWithin 0 (Ioi 0)) atBot
⊢ ¬DifferentiableWithinAt ℝ klFun (Ioi 0) 0

Tactic:
refine not_differentiableWithinAt_of_deriv_tendsto_atBot_Ioi _ ?_

Premises used: not_differentiableWithinAt_of_deriv_tendsto_atBot_Ioi
-- Module: Mathlib.InformationTheory.KullbackLeibler.KLFun
Goal:
rw : Tendsto log (nhdsWithin 0 (Ioi 0)) atBot
⊢ Tendsto (deriv klFun) (nhdsWithin 0 (Ioi 0)) atBot

Tactic:
rw [deriv_klFun]

Premises used: InformationTheory.deriv_klFun
-- Module: Mathlib.InformationTheory.KullbackLeibler.KLFun
Goal:
⊢ Tendsto log (nhdsWithin 0 (Ioi 0)) atBot

Tactic:
tendsto_log_nhdsGT_zero

Premises used: Real.tendsto_log_nhdsGT_zero
-- Module: Mathlib.InformationTheory.KullbackLeibler.KLFun
Goal:
⊢ Tendsto log (nhdsWithin 0 (Ioi 0)) atBot

Tactic:
exact tendsto_log_nhdsGT_zero

Premises used: Real.tendsto_log_nhdsGT_zero
-- Module: Mathlib.InformationTheory.KullbackLeibler.KLFun
Goal:
⊢ ¬DifferentiableWithinAt ℝ klFun (Iio 0) 0

Tactic:
not_differentiableWithinAt_of_deriv_tendsto_atBot_Iio _ ?_

Premises used: not_differentiableWithinAt_of_deriv_tendsto_atBot_Iio
-- Module: Mathlib.InformationTheory.KullbackLeibler.KLFun
Goal:
refine : Tendsto (deriv klFun) (nhdsWithin 0 (Iio 0)) atBot
⊢ ¬DifferentiableWithinAt ℝ klFun (Iio 0) 0

Tactic:
refine not_differentiableWithinAt_of_deriv_tendsto_atBot_Iio _ ?_

Premises used: not_differentiableWithinAt_of_deriv_tendsto_atBot_Iio
-- Module: Mathlib.InformationTheory.KullbackLeibler.KLFun
Goal:
rw : Tendsto log (nhdsWithin 0 (Iio 0)) atBot
⊢ Tendsto (deriv klFun) (nhdsWithin 0 (Iio 0)) atBot

Tactic:
rw [deriv_klFun]

Premises used: InformationTheory.deriv_klFun
-- Module: Mathlib.InformationTheory.KullbackLeibler.KLFun
Goal:
⊢ Tendsto log (nhdsWithin 0 (Iio 0)) atBot

Tactic:
tendsto_log_nhdsLT_zero

Premises used: Real.tendsto_log_nhdsLT_zero
-- Module: Mathlib.InformationTheory.KullbackLeibler.KLFun
Goal:
⊢ Tendsto log (nhdsWithin 0 (Iio 0)) atBot

Tactic:
exact tendsto_log_nhdsLT_zero

Premises used: Real.tendsto_log_nhdsLT_zero
-- Module: Mathlib.InformationTheory.KullbackLeibler.KLFun
Goal:
x : ℝ
pos : ∀ (h0 : x = 0), derivWithin klFun (Ioi x) x = log x
neg : ∀ (h0 : ¬x = 0), derivWithin klFun (Ioi x) x = log x
⊢ derivWithin klFun (Ioi x) x = log x

Tactic:
by_cases h0 : x = 0
-- Module: Mathlib.InformationTheory.KullbackLeibler.KLFun
Goal:
x : ℝ
h0 : x = 0
pos : derivWithin klFun (Ioi 0) 0 = 0
⊢ derivWithin klFun (Ioi x) x = log x

Tactic:
simp only [h0, log_zero]

Premises used: Real.log_zero
-- Module: Mathlib.InformationTheory.KullbackLeibler.KLFun
Goal:
x : ℝ
h0 : x = 0
⊢ derivWithin klFun (Ioi 0) 0 = 0

Tactic:
derivWithin_zero_of_not_differentiableWithinAt not_differentiableWithinAt_klFun_Ioi_zero

Premises used: InformationTheory.not_differentiableWithinAt_klFun_Ioi_zero, derivWithin_zero_of_not_differentiableWithinAt
-- Module: Mathlib.InformationTheory.KullbackLeibler.KLFun
Goal:
x : ℝ
h0 : x = 0
⊢ derivWithin klFun (Ioi 0) 0 = 0

Tactic:
exact derivWithin_zero_of_not_differentiableWithinAt not_differentiableWithinAt_klFun_Ioi_zero

Premises used: InformationTheory.not_differentiableWithinAt_klFun_Ioi_zero, derivWithin_zero_of_not_differentiableWithinAt
-- Module: Mathlib.InformationTheory.KullbackLeibler.KLFun
Goal:
x : ℝ
h0 : ¬x = 0
⊢ derivWithin klFun (Ioi x) x = log x

Tactic:
(hasDerivAt_klFun h0).hasDerivWithinAt.derivWithin (uniqueDiffWithinAt_Ioi x)

Premises used: HasDerivAt.hasDerivWithinAt, InformationTheory.hasDerivAt_klFun, HasDerivWithinAt.derivWithin, uniqueDiffWithinAt_Ioi
-- Module: Mathlib.InformationTheory.KullbackLeibler.KLFun
Goal:
x : ℝ
h0 : ¬x = 0
⊢ derivWithin klFun (Ioi x) x = log x

Tactic:
exact (hasDerivAt_klFun h0).hasDerivWithinAt.derivWithin (uniqueDiffWithinAt_Ioi x)

Premises used: HasDerivAt.hasDerivWithinAt, InformationTheory.hasDerivAt_klFun, HasDerivWithinAt.derivWithin, uniqueDiffWithinAt_Ioi
-- Module: Mathlib.InformationTheory.KullbackLeibler.KLFun
Goal:
x : ℝ
pos : ∀ (h0 : x = 0), derivWithin klFun (Iio x) x = log x
neg : ∀ (h0 : ¬x = 0), derivWithin klFun (Iio x) x = log x
⊢ derivWithin klFun (Iio x) x = log x

Tactic:
by_cases h0 : x = 0
-- Module: Mathlib.InformationTheory.KullbackLeibler.KLFun
Goal:
x : ℝ
h0 : x = 0
pos : derivWithin klFun (Iio 0) 0 = 0
⊢ derivWithin klFun (Iio x) x = log x

Tactic:
simp only [h0, log_zero]

Premises used: Real.log_zero
-- Module: Mathlib.InformationTheory.KullbackLeibler.KLFun
Goal:
x : ℝ
h0 : x = 0
⊢ derivWithin klFun (Iio 0) 0 = 0

Tactic:
derivWithin_zero_of_not_differentiableWithinAt not_differentiableWithinAt_klFun_Iio_zero

Premises used: InformationTheory.not_differentiableWithinAt_klFun_Iio_zero, derivWithin_zero_of_not_differentiableWithinAt
-- Module: Mathlib.InformationTheory.KullbackLeibler.KLFun
Goal:
x : ℝ
h0 : x = 0
⊢ derivWithin klFun (Iio 0) 0 = 0

Tactic:
exact derivWithin_zero_of_not_differentiableWithinAt not_differentiableWithinAt_klFun_Iio_zero

Premises used: InformationTheory.not_differentiableWithinAt_klFun_Iio_zero, derivWithin_zero_of_not_differentiableWithinAt
-- Module: Mathlib.InformationTheory.KullbackLeibler.KLFun
Goal:
x : ℝ
h0 : ¬x = 0
⊢ derivWithin klFun (Iio x) x = log x

Tactic:
(hasDerivAt_klFun h0).hasDerivWithinAt.derivWithin (uniqueDiffWithinAt_Iio x)

Premises used: HasDerivAt.hasDerivWithinAt, InformationTheory.hasDerivAt_klFun, HasDerivWithinAt.derivWithin, uniqueDiffWithinAt_Iio
-- Module: Mathlib.InformationTheory.KullbackLeibler.KLFun
Goal:
x : ℝ
h0 : ¬x = 0
⊢ derivWithin klFun (Iio x) x = log x

Tactic:
exact (hasDerivAt_klFun h0).hasDerivWithinAt.derivWithin (uniqueDiffWithinAt_Iio x)

Premises used: HasDerivAt.hasDerivWithinAt, InformationTheory.hasDerivAt_klFun, HasDerivWithinAt.derivWithin, uniqueDiffWithinAt_Iio
-- Module: Mathlib.InformationTheory.KullbackLeibler.KLFun
Goal:
⊢ derivWithin klFun (Ioi 1) 1 = 0

Tactic:
simp
-- Module: Mathlib.InformationTheory.KullbackLeibler.KLFun
Goal:
⊢ derivWithin klFun (Iio 1) 1 = 0

Tactic:
simp
-- Module: Mathlib.InformationTheory.KullbackLeibler.KLFun
Goal:
simp : Tendsto (β := ℝ) (fun (x : ℝ) ↦ log x) atTop atTop
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ derivWithin klFun (Ioi x) x) atTop atTop

Tactic:
simp only [rightDeriv_klFun]

Premises used: InformationTheory.rightDeriv_klFun
-- Module: Mathlib.InformationTheory.KullbackLeibler.KLFun
Goal:
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ log x) atTop atTop

Tactic:
tendsto_log_atTop

Premises used: Real.tendsto_log_atTop
-- Module: Mathlib.InformationTheory.KullbackLeibler.KLFun
Goal:
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ log x) atTop atTop

Tactic:
exact tendsto_log_atTop

Premises used: Real.tendsto_log_atTop
-- Module: Mathlib.InformationTheory.KullbackLeibler.KLFun
Goal:
⊢ Membership.mem (γ := Set ℝ) (interior (Ici 0)) 1

Tactic:
simp
-- Module: Mathlib.InformationTheory.KullbackLeibler.KLFun
Goal:
x : ℝ
hx : 0 ≤ x
⊢ 0 ≤ klFun x

Tactic:
klFun_one ▸ isMinOn_klFun hx

Premises used: Eq.rec, InformationTheory.isMinOn_klFun, InformationTheory.klFun_one
-- Module: Mathlib.InformationTheory.KullbackLeibler.KLFun
Goal:
x : ℝ
hx : 0 ≤ x
h : x = 1
⊢ klFun x = 0

Tactic:
simp [klFun_apply, h]

Premises used: InformationTheory.klFun_apply
-- Module: Mathlib.InformationTheory.KullbackLeibler.KLFun
Goal:
x : ℝ
hx : 0 ≤ x
refine : ∀ (h : klFun x = 0), x = 1
⊢ klFun x = 0 ↔ x = 1

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ by simp [klFun_apply, h]⟩
-- Module: Mathlib.InformationTheory.KullbackLeibler.KLFun
Goal:
x : ℝ
hx : 0 ≤ x
h : klFun x = 0
⊢ x = 1

Tactic:
strictConvexOn_klFun.eq_of_isMinOn (isMinOn_iff.mpr fun y hy ↦ h ▸ klFun_nonneg hy)
    isMinOn_klFun hx (zero_le_one' ℝ)

Premises used: Iff.mpr, Real, Eq.rec, zero_le_one', StrictConvexOn.eq_of_isMinOn, InformationTheory.klFun_nonneg, InformationTheory.isMinOn_klFun, InformationTheory.strictConvexOn_klFun, isMinOn_iff, Eq.symm
-- Module: Mathlib.InformationTheory.KullbackLeibler.KLFun
Goal:
x : ℝ
hx : 0 ≤ x
h : klFun x = 0
⊢ x = 1

Tactic:
exact strictConvexOn_klFun.eq_of_isMinOn (isMinOn_iff.mpr fun y hy ↦ h ▸ klFun_nonneg hy)
    isMinOn_klFun hx (zero_le_one' ℝ)

Premises used: Iff.mpr, Real, zero_le_one', StrictConvexOn.eq_of_isMinOn, InformationTheory.isMinOn_klFun, InformationTheory.strictConvexOn_klFun, isMinOn_iff
-- Module: Mathlib.InformationTheory.KullbackLeibler.KLFun
Goal:
h : ∀ (x : ℝ), x * log x + 1 - x = x * (log x - 1) + 1
⊢ Eq (α := (x : ℝ) → ℝ) (fun (x : ℝ) ↦ x * log x + 1 - x) fun (x : ℝ) ↦ x * (log x - 1) + 1

Tactic:
ext
-- Module: Mathlib.InformationTheory.KullbackLeibler.KLFun
Goal:
x : ℝ
⊢ x * log x + 1 - x = x * (log x - 1) + 1

Tactic:
ring
-- Module: Mathlib.InformationTheory.KullbackLeibler.KLFun
Goal:
⊢ klFun = fun (x : ℝ) ↦ x * (log x - 1) + 1

Tactic:
have : klFun = (fun x ↦ x * (log x - 1) + 1) := by unfold klFun; ext; ring
-- Module: Mathlib.InformationTheory.KullbackLeibler.KLFun
Goal:
this : klFun = fun (x : ℝ) ↦ x * (log x - 1) + 1
rw : Tendsto (β := ℝ) (fun (x : ℝ) ↦ x * (log x - 1) + 1) atTop atTop
⊢ Tendsto klFun atTop atTop

Tactic:
rw [this]
-- Module: Mathlib.InformationTheory.KullbackLeibler.KLFun
Goal:
this : klFun = fun (x : ℝ) ↦ x * (log x - 1) + 1
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ x * (log x - 1) + 1) atTop atTop

Tactic:
Tendsto.atTop_add ?_ tendsto_const_nhds

Premises used: tendsto_const_nhds, Filter.Tendsto.atTop_add
-- Module: Mathlib.InformationTheory.KullbackLeibler.KLFun
Goal:
this : klFun = fun (x : ℝ) ↦ x * (log x - 1) + 1
refine : Tendsto (β := ℝ) (fun (x : ℝ) ↦ x * (log x - 1)) atTop atTop
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ x * (log x - 1) + 1) atTop atTop

Tactic:
refine Tendsto.atTop_add ?_ tendsto_const_nhds

Premises used: tendsto_const_nhds, Filter.Tendsto.atTop_add
-- Module: Mathlib.InformationTheory.KullbackLeibler.KLFun
Goal:
this : klFun = fun (x : ℝ) ↦ x * (log x - 1) + 1
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ x * (log x - 1)) atTop atTop

Tactic:
tendsto_id.atTop_mul_atTop₀ ?_

Premises used: Filter.tendsto_id, Filter.Tendsto.atTop_mul_atTop₀
-- Module: Mathlib.InformationTheory.KullbackLeibler.KLFun
Goal:
this : klFun = fun (x : ℝ) ↦ x * (log x - 1) + 1
refine : Tendsto (β := ℝ) (fun (x : ℝ) ↦ log x - 1) atTop atTop
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ x * (log x - 1)) atTop atTop

Tactic:
refine tendsto_id.atTop_mul_atTop₀ ?_

Premises used: Filter.tendsto_id, Filter.Tendsto.atTop_mul_atTop₀
-- Module: Mathlib.InformationTheory.KullbackLeibler.KLFun
Goal:
this : klFun = fun (x : ℝ) ↦ x * (log x - 1) + 1
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ log x - 1) atTop atTop

Tactic:
tendsto_log_atTop.atTop_add tendsto_const_nhds

Premises used: tendsto_const_nhds, Filter.Tendsto.atTop_add, Real.tendsto_log_atTop
-- Module: Mathlib.InformationTheory.KullbackLeibler.KLFun
Goal:
this : klFun = fun (x : ℝ) ↦ x * (log x - 1) + 1
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ log x - 1) atTop atTop

Tactic:
exact tendsto_log_atTop.atTop_add tendsto_const_nhds

Premises used: tendsto_const_nhds, Filter.Tendsto.atTop_add, Real.tendsto_log_atTop
-- Module: Mathlib.InformationTheory.KullbackLeibler.KLFun
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
hμν : μ ≪ ν
this :
  Integrable (ε := ℝ) (fun (x : α) ↦ (μ.rnDeriv ν x).toReal * log (μ.rnDeriv ν x).toReal + (1 - (μ.rnDeriv ν x).toReal))
      ν ↔
    Integrable (llr μ ν) μ
⊢ Integrable (ε := ℝ) (fun (x : α) ↦ (μ.rnDeriv ν x).toReal * log (μ.rnDeriv ν x).toReal + (1 - (μ.rnDeriv ν x).toReal))
      ν ↔
    Integrable (llr μ ν) μ

Tactic:
this