mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Measure.Decomposition.IntegralRNDeriv

Goal state before:
pp: 𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
𝓨 : Type u_2
m𝓨 : MeasurableSpace 𝓨
κ η : Kernel 𝓧 𝓨
f : ℝ → ℝ
inst✝³ : IsFiniteMeasure μ
inst✝² : IsFiniteMeasure ν
inst✝¹ : IsMarkovKernel κ
inst✝ : IsMarkovKernel η
hf : StronglyMeasurable f
hf_cvx : ConvexOn ℝ (Ici 0) f
hf_cont_at : ContinuousWithinAt f (Ici 0) 0
h_int✝ :
  (∀ᵐ (x : 𝓧) ∂ν, Integrable (fun y ↦ f ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (x, y)).toReal) (η x)) ∧
    Integrable (fun x ↦ ∫ (y : 𝓨), ‖f ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (x, y)).toReal‖ ∂η x) ν
hκη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
hf_cont : ContinuousOn f (Ici 0)
h_lt_top✝ : ∀ᵐ (a : 𝓧) ∂ν, ∀ᵐ (b : 𝓨) ∂η a, (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (a, b) < ∞
h_integrable :
  (∀ᵐ (x : 𝓧) ∂ν, Integrable (fun y ↦ ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (x, y)).toReal) (η x)) ∧
    Integrable (fun x ↦ ∫ (y : 𝓨), ‖((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (x, y)).toReal‖ ∂η x) ν
h_ae1 : ∀ᵐ (a : 𝓧) ∂ν, μ.rnDeriv ν a * ∫⁻ (b : 𝓨), (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) (a, b) ∂η a = μ.rnDeriv ν a
h_ae2 :
  ∀ᵐ (a : 𝓧) ∂ν, ∀ᵐ (b : 𝓨) ∂η a, μ.rnDeriv ν a * (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) (a, b) = (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (a, b)
a : 𝓧
h_eq_one : μ.rnDeriv ν a * ∫⁻ (b : 𝓨), (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) (a, b) ∂η a = μ.rnDeriv ν a
h_mul_eq : ∀ᵐ (b : 𝓨) ∂η a, μ.rnDeriv ν a * (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) (a, b) = (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (a, b)
h_lt_top : ∀ᵐ (b : 𝓨) ∂η a, (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (a, b) < ∞
h_int' : Integrable (fun y ↦ ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (a, y)).toReal) (η a)
h_int : Integrable (fun y ↦ f ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (a, y)).toReal) (η a)
⊢ f (∫⁻ (b : 𝓨), (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (a, b) ∂η a).toReal =
    f (∫ (b : 𝓨), ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (a, b)).toReal ∂η a)

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Kernel.Composition.IntegralCompProd

Goal state before:
pp: α : Type u_5
β : Type u_6
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
μ : Measure α
inst✝³ : SFinite μ
inst✝² : IsSFiniteKernel κ
E : Type u_8
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set α
hs : MeasurableSet s
t : Set β
ht : MeasurableSet t
f : α × β → E
hf : IntegrableOn f (s ×ˢ t) (μ ⊗ₘ κ)
⊢ ∫ (x : α × β) in s ×ˢ t, f x ∂μ ⊗ₘ κ = ∫ (a : α) in s, ∫ (b : β) in t, f (a, b) ∂κ a ∂μ

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.LogLikelihoodRatio

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
f : α → ℝ
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
hf : Integrable (fun x ↦ rexp (f x)) μ
hfν : AEMeasurable f ν
⊢ llr (μ.tilted f) ν =ᵐ[μ] fun x ↦ f x - log (∫ (z : α), rexp (f z) ∂μ) + llr μ ν x

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.LogLikelihoodRatio

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
f : α → ℝ
inst✝¹ : IsFiniteMeasure μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
hf : Integrable f μ
h_int : Integrable (llr μ ν) μ
hfμ : Integrable (fun x ↦ rexp (f x)) μ
hfν : AEMeasurable f ν
⊢ Integrable (llr (μ.tilted f) ν) μ

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Kernel.Composition.IntegralCompProd

Goal state before:
pp: α : Type u_5
β : Type u_6
E : Type u_7
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝² : NormedAddCommGroup E
κ : Kernel α β
μ : Measure α
f : β → E
inst✝¹ : SFinite μ
inst✝ : IsSFiniteKernel κ
hf : AEStronglyMeasurable f (⇑κ ∘ₘ μ)
⊢ Integrable (fun p ↦ f p.2) (μ ⊗ₘ κ) ↔ Integrable f (⇑κ ∘ₘ μ)

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Tilted

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
inst✝ : SigmaFinite μ
hf : Integrable (fun x ↦ rexp (f x)) μ
h0 : NeZero μ
hf' : AEMeasurable f μ
x : α
hx : (μ.tilted f).rnDeriv μ x = ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ)
⊢ 0 ≤ rexp (f x) / ∫ (x : α), rexp (f x) ∂μ

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Kernel.Composition.IntegralCompProd

Goal state before:
pp: α : Type u_5
β : Type u_6
E : Type u_7
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : NormedAddCommGroup E
κ : Kernel α β
μ : Measure α
f : β → E
h_int : Integrable f (⇑κ ∘ₘ μ)
⊢ ∀ᵐ (x : α) ∂μ, Integrable f (κ x)

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Kernel.Composition.IntegralCompProd

Goal state before:
pp: α : Type u_5
β : Type u_6
E : Type u_7
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : NormedAddCommGroup E
κ : Kernel α β
μ : Measure α
f : β → E
h_int : Integrable f (⇑κ ∘ₘ μ)
⊢ Integrable (fun x ↦ ∫ (y : β), ‖f y‖ ∂κ x) μ

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Tilted

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
inst✝ : SigmaFinite μ
hf : Integrable (fun x ↦ rexp (f x)) μ
⊢ (fun x ↦ log ((μ.tilted f).rnDeriv μ x).toReal) =ᵐ[μ] fun x ↦ f x - log (∫ (x : α), rexp (f x) ∂μ)

Tactic:
by

Goal state after:
Module: Mathlib.InformationTheory.KullbackLeibler.KLFun

Goal state before:
pp: ⊢ klFun 0 = 1

Tactic:
by

Goal state after:
Module: Mathlib.InformationTheory.KullbackLeibler.KLFun

Goal state before:
pp: ⊢ klFun 1 = 0

Tactic:
by

Goal state after:
Module: Mathlib.InformationTheory.KullbackLeibler.KLFun

Goal state before:
pp: ⊢ Continuous klFun

Tactic:
by

Goal state after:
Module: Mathlib.InformationTheory.KullbackLeibler.KLFun

Goal state before:
pp: x : ℝ
hx : x ≠ 0
⊢ HasDerivAt klFun (log x) x

Tactic:
by

Goal state after:
Module: Mathlib.InformationTheory.KullbackLeibler.KLFun

Goal state before:
pp: ⊢ ¬DifferentiableAt ℝ klFun 0

Tactic:
by

Goal state after:
Module: Mathlib.InformationTheory.KullbackLeibler.KLFun

Goal state before:
pp: ⊢ deriv klFun = log

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.LogLikelihoodRatio

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
f : α → ℝ
inst✝¹ : IsProbabilityMeasure μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
hf : Integrable f μ
h_int : Integrable (llr μ ν) μ
hfμ : Integrable (fun x ↦ rexp (f x)) μ
hfν : AEMeasurable f ν
⊢ ∫ (x : α), f x - log (∫ (x : α), rexp (f x) ∂μ) + llr μ ν x ∂μ =
    ∫ (x : α), f x ∂μ - log (∫ (x : α), rexp (f x) ∂μ) + ∫ (x : α), llr μ ν x ∂μ

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Decomposition.IntegralRNDeriv

Goal state before:
pp: 𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
𝓨 : Type u_2
m𝓨 : MeasurableSpace 𝓨
κ η : Kernel 𝓧 𝓨
f : ℝ → ℝ
inst✝³ : IsFiniteMeasure μ
inst✝² : IsFiniteMeasure ν
inst✝¹ : IsMarkovKernel κ
inst✝ : IsMarkovKernel η
hf : StronglyMeasurable f
hf_cvx : ConvexOn ℝ (Ici 0) f
hf_cont_at : ContinuousWithinAt f (Ici 0) 0
h_int✝ :
  (∀ᵐ (x : 𝓧) ∂ν, Integrable (fun y ↦ f ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (x, y)).toReal) (η x)) ∧
    Integrable (fun x ↦ ∫ (y : 𝓨), ‖f ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (x, y)).toReal‖ ∂η x) ν
hκη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
hf_cont : ContinuousOn f (Ici 0)
h_lt_top✝ : ∀ᵐ (a : 𝓧) ∂ν, ∀ᵐ (b : 𝓨) ∂η a, (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (a, b) < ∞
h_integrable :
  (∀ᵐ (x : 𝓧) ∂ν, Integrable (fun y ↦ ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (x, y)).toReal) (η x)) ∧
    Integrable (fun x ↦ ∫ (y : 𝓨), ‖((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (x, y)).toReal‖ ∂η x) ν
h_ae1 : ∀ᵐ (a : 𝓧) ∂ν, μ.rnDeriv ν a * ∫⁻ (b : 𝓨), (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) (a, b) ∂η a = μ.rnDeriv ν a
h_ae2 :
  ∀ᵐ (a : 𝓧) ∂ν, ∀ᵐ (b : 𝓨) ∂η a, μ.rnDeriv ν a * (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) (a, b) = (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (a, b)
a : 𝓧
h_eq_one : μ.rnDeriv ν a * ∫⁻ (b : 𝓨), (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) (a, b) ∂η a = μ.rnDeriv ν a
h_mul_eq : ∀ᵐ (b : 𝓨) ∂η a, μ.rnDeriv ν a * (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) (a, b) = (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (a, b)
h_lt_top : ∀ᵐ (b : 𝓨) ∂η a, (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (a, b) < ∞
h_int' : Integrable (fun y ↦ ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (a, y)).toReal) (η a)
h_int : Integrable (fun y ↦ f ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (a, y)).toReal) (η a)
⊢ ∀ᵐ (x : 𝓨) ∂η a, ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (a, x)).toReal ∈ Ici 0

Tactic:
by

Goal state after:
Module: Mathlib.InformationTheory.KullbackLeibler.KLFun

Goal state before:
pp: ⊢ ¬DifferentiableWithinAt ℝ klFun (Ioi 0) 0

Tactic:
by

Goal state after:
Module: Mathlib.InformationTheory.KullbackLeibler.KLFun

Goal state before:
pp: ⊢ ¬DifferentiableWithinAt ℝ klFun (Iio 0) 0

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.LogLikelihoodRatio

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
f : α → ℝ
inst✝¹ : IsProbabilityMeasure μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
hf : Integrable f μ
h_int : Integrable (llr μ ν) μ
hfμ : Integrable (fun x ↦ rexp (f x)) μ
hfν : AEMeasurable f ν
⊢ ∫ (x : α), f x ∂μ - log (∫ (x : α), rexp (f x) ∂μ) + ∫ (x : α), llr μ ν x ∂μ =
    ∫ (x : α), llr μ ν x ∂μ + ∫ (x : α), f x ∂μ - log (∫ (x : α), rexp (f x) ∂μ)

Tactic:
by

Goal state after:
Module: Mathlib.InformationTheory.KullbackLeibler.KLFun

Goal state before:
pp: x : ℝ
⊢ derivWithin klFun (Ioi x) x = log x

Tactic:
by

Goal state after:
Module: Mathlib.InformationTheory.KullbackLeibler.KLFun

Goal state before:
pp: x : ℝ
⊢ derivWithin klFun (Iio x) x = log x

Tactic:
by

Goal state after:
Module: Mathlib.InformationTheory.KullbackLeibler.Basic

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
h1 : μ ≪ ν
h2 : Integrable (llr μ ν) μ
⊢ klDiv μ ν = ENNReal.ofReal (∫ (x : α), llr μ ν x ∂μ + ν.real univ - μ.real univ)

Tactic:
by

Goal state after:
Module: Mathlib.InformationTheory.KullbackLeibler.Basic

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
h : ¬μ ≪ ν
⊢ klDiv μ ν = ∞

Tactic:
by

Goal state after:
Module: Mathlib.InformationTheory.KullbackLeibler.Basic

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
h : ¬Integrable (llr μ ν) μ
⊢ klDiv μ ν = ∞

Tactic:
by

Goal state after:
Module: Mathlib.InformationTheory.KullbackLeibler.KLFun

Goal state before:
pp: ⊢ derivWithin klFun (Ioi 1) 1 = 0

Tactic:
by

Goal state after:
Module: Mathlib.InformationTheory.KullbackLeibler.KLFun

Goal state before:
pp: ⊢ derivWithin klFun (Iio 1) 1 = 0

Tactic:
by

Goal state after:
Module: Mathlib.InformationTheory.KullbackLeibler.KLFun

Goal state before:
pp: ⊢ Tendsto (fun x ↦ derivWithin klFun (Ioi x) x) atTop atTop

Tactic:
by

Goal state after:
Module: Mathlib.InformationTheory.KullbackLeibler.KLFun

Goal state before:
pp: ⊢ 1 ∈ interior (Ici 0)

Tactic:
by

Goal state after:
Module: Mathlib.InformationTheory.KullbackLeibler.KLFun

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
h : x = 1
⊢ klFun x = 0

Tactic:
by

Goal state after:
Module: Mathlib.InformationTheory.KullbackLeibler.KLFun

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
⊢ klFun x = 0 ↔ x = 1

Tactic:
by

Goal state after:
Module: Mathlib.InformationTheory.KullbackLeibler.KLFun

Goal state before:
pp: ⊢ klFun = fun x ↦ x * (log x - 1) + 1

Tactic:
by

Goal state after:
Module: Mathlib.InformationTheory.KullbackLeibler.KLFun

Goal state before:
pp: ⊢ Tendsto klFun atTop atTop

Tactic:
by

Goal state after:
Module: Mathlib.InformationTheory.KullbackLeibler.Basic

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
⊢ klDiv μ μ = 0

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.LogLikelihoodRatio

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
f : α → ℝ
inst✝¹ : IsProbabilityMeasure μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
hf : Integrable f μ
h_int : Integrable (llr μ ν) μ
hfμ : Integrable (fun x ↦ rexp (f x)) μ
hfν : AEMeasurable f ν
⊢ ∫ (x : α), llr (μ.tilted f) ν x ∂μ = ∫ (x : α), llr μ ν x ∂μ + ∫ (x : α), f x ∂μ - log (∫ (x : α), rexp (f x) ∂μ)

Tactic:
by

Goal state after:
Module: Mathlib.InformationTheory.KullbackLeibler.Basic

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
ν : Measure α
inst✝ : IsFiniteMeasure ν
⊢ klDiv 0 ν = ν univ

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.LogLikelihoodRatio

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
f : α → ℝ
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
hf : Integrable (fun x ↦ rexp (f x)) ν
h : ν = 0
s : Set α
a✝ : MeasurableSet s
⊢ ν s = 0

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.LogLikelihoodRatio

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
f : α → ℝ
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
hf : Integrable (fun x ↦ rexp (f x)) ν
h : ν = 0
⊢ μ = 0

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Decomposition.IntegralRNDeriv

Goal state before:
pp: 𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
𝓨 : Type u_2
m𝓨 : MeasurableSpace 𝓨
κ η : Kernel 𝓧 𝓨
f : ℝ → ℝ
inst✝³ : IsFiniteMeasure μ
inst✝² : IsFiniteMeasure ν
inst✝¹ : IsMarkovKernel κ
inst✝ : IsMarkovKernel η
hf : StronglyMeasurable f
hf_cvx : ConvexOn ℝ (Ici 0) f
hf_cont_at : ContinuousWithinAt f (Ici 0) 0
h_int✝ :
  (∀ᵐ (x : 𝓧) ∂ν, Integrable (fun y ↦ f ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (x, y)).toReal) (η x)) ∧
    Integrable (fun x ↦ ∫ (y : 𝓨), ‖f ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (x, y)).toReal‖ ∂η x) ν
hκη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
hf_cont : ContinuousOn f (Ici 0)
h_lt_top✝ : ∀ᵐ (a : 𝓧) ∂ν, ∀ᵐ (b : 𝓨) ∂η a, (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (a, b) < ∞
h_integrable :
  (∀ᵐ (x : 𝓧) ∂ν, Integrable (fun y ↦ ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (x, y)).toReal) (η x)) ∧
    Integrable (fun x ↦ ∫ (y : 𝓨), ‖((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (x, y)).toReal‖ ∂η x) ν
h_ae1 : ∀ᵐ (a : 𝓧) ∂ν, μ.rnDeriv ν a * ∫⁻ (b : 𝓨), (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) (a, b) ∂η a = μ.rnDeriv ν a
h_ae2 :
  ∀ᵐ (a : 𝓧) ∂ν, ∀ᵐ (b : 𝓨) ∂η a, μ.rnDeriv ν a * (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) (a, b) = (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (a, b)
a : 𝓧
h_eq_one : μ.rnDeriv ν a * ∫⁻ (b : 𝓨), (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) (a, b) ∂η a = μ.rnDeriv ν a
h_mul_eq : ∀ᵐ (b : 𝓨) ∂η a, μ.rnDeriv ν a * (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) (a, b) = (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (a, b)
h_lt_top : ∀ᵐ (b : 𝓨) ∂η a, (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (a, b) < ∞
h_int' : Integrable (fun y ↦ ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (a, y)).toReal) (η a)
h_int : Integrable (fun y ↦ f ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (a, y)).toReal) (η a)
⊢ f (∫ (b : 𝓨), ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (a, b)).toReal ∂η a) ≤
    ∫ (b : 𝓨), f ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (a, b)).toReal ∂η a

Tactic:
by

Goal state after:
Module: Mathlib.InformationTheory.KullbackLeibler.KLFun

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hμν : μ ≪ ν
this :
  Integrable (fun x ↦ (μ.rnDeriv ν x).toReal * log (μ.rnDeriv ν x).toReal + (1 - (μ.rnDeriv ν x).toReal)) ν ↔
    Integrable (llr μ ν) μ
⊢ Integrable (fun x ↦ klFun (μ.rnDeriv ν x).toReal) ν ↔ Integrable (llr μ ν) μ

Tactic:
by

Goal state after:
Module: Mathlib.InformationTheory.KullbackLeibler.KLFun

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hμν : μ ≪ ν
⊢ Integrable (fun x ↦ klFun (μ.rnDeriv ν x).toReal) ν ↔ Integrable (llr μ ν) μ

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Decomposition.IntegralRNDeriv

Goal state before:
pp: 𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
𝓨 : Type u_2
m𝓨 : MeasurableSpace 𝓨
κ η : Kernel 𝓧 𝓨
f : ℝ → ℝ
inst✝³ : IsFiniteMeasure μ
inst✝² : IsFiniteMeasure ν
inst✝¹ : IsMarkovKernel κ
inst✝ : IsMarkovKernel η
hf : StronglyMeasurable f
hf_cvx : ConvexOn ℝ (Ici 0) f
hf_cont_at : ContinuousWithinAt f (Ici 0) 0
h_int : Integrable (fun p ↦ f ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) p).toReal) (ν ⊗ₘ η)
hκη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
⊢ (fun a ↦ f (μ.rnDeriv ν a).toReal) ≤ᵐ[ν] fun a ↦ ∫ (b : 𝓨), f ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (a, b)).toReal ∂η a

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Decomposition.IntegralRNDeriv

Goal state before:
pp: 𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
𝓨 : Type u_2
m𝓨 : MeasurableSpace 𝓨
κ η : Kernel 𝓧 𝓨
f : ℝ → ℝ
inst✝³ : IsFiniteMeasure μ
inst✝² : IsFiniteMeasure ν
inst✝¹ : IsMarkovKernel κ
inst✝ : IsMarkovKernel η
hf : StronglyMeasurable f
hf_cvx : ConvexOn ℝ (Ici 0) f
hf_cont_at : ContinuousWithinAt f (Ici 0) 0
hf_int : Integrable (fun p ↦ f ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) p).toReal) (ν ⊗ₘ η)
hκη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
hf_cont : ContinuousOn f (Ici 0)
c c' : ℝ
h : ∀ (x : ℝ), 0 ≤ x → c * x + c' ≤ f x
⊢ Integrable (fun x ↦ c * (μ.rnDeriv ν x).toReal + c') ν

Tactic:
by

Goal state after:
Module: Mathlib.InformationTheory.KullbackLeibler.Basic

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
⊢ klDiv μ ν = ∞ ↔ μ ≪ ν → ¬Integrable (llr μ ν) μ

Tactic:
by

Goal state after:
Module: Mathlib.InformationTheory.KullbackLeibler.Basic

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
⊢ klDiv μ ν ≠ ∞ ↔ μ ≪ ν ∧ Integrable (llr μ ν) μ

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Decomposition.IntegralRNDeriv

Goal state before:
pp: 𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
𝓨 : Type u_2
m𝓨 : MeasurableSpace 𝓨
κ η : Kernel 𝓧 𝓨
f : ℝ → ℝ
inst✝³ : IsFiniteMeasure μ
inst✝² : IsFiniteMeasure ν
inst✝¹ : IsMarkovKernel κ
inst✝ : IsMarkovKernel η
hf : StronglyMeasurable f
hf_cvx : ConvexOn ℝ (Ici 0) f
hf_cont_at : ContinuousWithinAt f (Ici 0) 0
hf_int : Integrable (fun p ↦ f ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) p).toReal) (ν ⊗ₘ η)
hκη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
hf_cont : ContinuousOn f (Ici 0)
c c' : ℝ
h : ∀ (x : ℝ), 0 ≤ x → c * x + c' ≤ f x
⊢ StronglyMeasurable fun a ↦ f (μ.rnDeriv ν a).toReal

Tactic:
by

Goal state after:
Module: Mathlib.InformationTheory.KullbackLeibler.Basic

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
h : μ ≪ ν ∧ Integrable (llr μ ν) μ
⊢ ENNReal.ofReal (∫ (x : α), llr μ ν x ∂μ + ν.real univ - μ.real univ) =
    ENNReal.ofReal (∫ (x : α), klFun (μ.rnDeriv ν x).toReal ∂ν)

Tactic:
by

Goal state after:
Module: Mathlib.InformationTheory.KullbackLeibler.Basic

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
⊢ klDiv μ ν = if μ ≪ ν ∧ Integrable (llr μ ν) μ then ENNReal.ofReal (∫ (x : α), klFun (μ.rnDeriv ν x).toReal ∂ν) else ∞

Tactic:
by

Goal state after:
Module: Mathlib.InformationTheory.KullbackLeibler.KLFun

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
⊢ ∫ (x : α), klFun (μ.rnDeriv ν x).toReal ∂ν = ∫ (x : α), llr μ ν x ∂μ + ν.real univ - μ.real univ

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Decomposition.IntegralRNDeriv

Goal state before:
pp: 𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
𝓨 : Type u_2
m𝓨 : MeasurableSpace 𝓨
κ η : Kernel 𝓧 𝓨
f : ℝ → ℝ
inst✝³ : IsFiniteMeasure μ
inst✝² : IsFiniteMeasure ν
inst✝¹ : IsMarkovKernel κ
inst✝ : IsMarkovKernel η
hf : StronglyMeasurable f
hf_cvx : ConvexOn ℝ (Ici 0) f
hf_cont_at : ContinuousWithinAt f (Ici 0) 0
hf_int : Integrable (fun p ↦ f ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) p).toReal) (ν ⊗ₘ η)
hκη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
⊢ Integrable (fun a ↦ f (μ.rnDeriv ν a).toReal) ν

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSpace.CompleteOfCompleteLp

Goal state before:
pp: α : Type u_1
E : Type u_2
inst✝ : NormedAddCommGroup E
mα : MeasurableSpace α
μ : Measure α
f : α → E
h'f : ∀ (s : Set α), MeasurableSet s → 0 < μ s → ∞ ≤ μ s
fn : ℕ → SimpleFunc α E
hfn : ∀ (n : ℕ), μ (Function.support ⇑(fn n)) < ∞
hfn_lim : ∀ (x : α), Tendsto (fun n ↦ (fn n) x) atTop (𝓝 (f x))
n : ℕ
this : μ (Function.support ⇑(fn n)) ≠ 0
⊢ 0 < μ (Function.support ⇑(fn n))

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSpace.CompleteOfCompleteLp

Goal state before:
pp: α : Type u_1
E : Type u_2
inst✝ : NormedAddCommGroup E
mα : MeasurableSpace α
μ : Measure α
f : α → E
h'f : ∀ (s : Set α), MeasurableSet s → 0 < μ s → ∞ ≤ μ s
fn : ℕ → SimpleFunc α E
hfn : ∀ (n : ℕ), μ (Function.support ⇑(fn n)) < ∞
hfn_lim : ∀ (x : α), Tendsto (fun n ↦ (fn n) x) atTop (𝓝 (f x))
n : ℕ
⊢ μ (Function.support ⇑(fn n)) = 0

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSpace.CompleteOfCompleteLp

Goal state before:
pp: α : Type u_1
E : Type u_2
inst✝ : NormedAddCommGroup E
mα : MeasurableSpace α
μ : Measure α
f : α → E
hf : FinStronglyMeasurable f μ
h'f : ¬f =ᵐ[μ] 0
⊢ ∃ s, MeasurableSet s ∧ 0 < μ s ∧ μ s < ∞

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSpace.CompleteOfCompleteLp

Goal state before:
pp: α : Type u_1
E : Type u_2
inst✝ : NormedAddCommGroup E
mα : MeasurableSpace α
μ : Measure α
f : α → E
hf : AEFinStronglyMeasurable f μ
h'f : ¬f =ᵐ[μ] 0
⊢ ∃ s, MeasurableSet s ∧ 0 < μ s ∧ μ s < ∞

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSpace.CompleteOfCompleteLp

Goal state before:
pp: α : Type u_1
E : Type u_2
inst✝¹ : NormedAddCommGroup E
mα : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : Nontrivial ↥(Lp E p μ)
f : ↥(Lp E p μ)
hf : f ≠ 0
⊢ ¬↑↑f =ᵐ[μ] 0

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Trim

Goal state before:
pp: α : Type u_1
ε : Type u_3
m m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
hm : m ≤ m0
f : α → ε
hf : StronglyMeasurable f
⊢ Measurable fun a ↦ ‖f a‖ₑ ^ q

Tactic:
by

Goal state after:
Module: Mathlib.InformationTheory.KullbackLeibler.Basic

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hμν : μ ≪ ν
⊢ Measurable fun x ↦ klFun (μ.rnDeriv ν x).toReal

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Trim

Goal state before:
pp: α : Type u_1
ε : Type u_3
m m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
hm : m ≤ m0
f : α → ε
hf : StronglyMeasurable f
⊢ eLpNorm' f q (μ.trim hm) = eLpNorm' f q μ

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSpace.CompleteOfCompleteLp

Goal state before:
pp: α : Type u_1
E : Type u_2
inst✝¹ : NormedAddCommGroup E
mα : MeasurableSpace α
μ : Measure α
inst✝ : Nontrivial ↥(Lp E ∞ μ)
f : ↥(Lp E ∞ μ)
hf : f ≠ 0
hfne : MemLp.toLp (fun x ↦ 1) ⋯ = 0
this : (fun x ↦ 1) =ᵐ[μ] 0
x : α
hx : 1 = 0 x
⊢ ↑↑f x = 0 x

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSpace.CompleteOfCompleteLp

Goal state before:
pp: α : Type u_1
E : Type u_2
inst✝¹ : NormedAddCommGroup E
mα : MeasurableSpace α
μ : Measure α
inst✝ : Nontrivial ↥(Lp E 0 μ)
f : ↥(Lp E 0 μ)
hf : f ≠ 0
hfne : ¬↑↑f =ᵐ[μ] 0
h'p : 0 < ∞
⊢ MemLp (fun x ↦ 1) 0 μ

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Trim

Goal state before:
pp: α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : α → ℝ≥0∞
hf : Measurable f
h_set_eq : {a | ∀ᵐ (n : α) ∂μ.trim hm, f n ≤ a} = {a | ∀ᵐ (n : α) ∂μ, f n ≤ a}
⊢ sInf {a | ∀ᵐ (n : α) ∂μ.trim hm, f n ≤ a} = sInf {a | ∀ᵐ (n : α) ∂μ, f n ≤ a}

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSpace.CompleteOfCompleteLp

Goal state before:
pp: α : Type u_1
E : Type u_2
inst✝¹ : NormedAddCommGroup E
mα : MeasurableSpace α
μ : Measure α
inst✝ : Nontrivial ↥(Lp E 0 μ)
f : ↥(Lp E 0 μ)
hf : f ≠ 0
h'p : 0 < ∞
this✝ : MemLp (fun x ↦ 1) 0 μ
hfne : MemLp.toLp (fun x ↦ 1) this✝ = 0
this : (fun x ↦ 1) =ᵐ[μ] 0
x : α
hx : 1 = 0 x
⊢ ↑↑f x = 0 x

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.LogLikelihoodRatio

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
f : α → ℝ
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
hf : Integrable (fun x ↦ rexp (f x)) ν
⊢ llr μ (ν.tilted f) =ᵐ[μ] fun x ↦ -f x + log (∫ (z : α), rexp (f z) ∂ν) + llr μ ν x

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.LogLikelihoodRatio

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
f : α → ℝ
inst✝¹ : IsFiniteMeasure μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
hfμ : Integrable f μ
h_int : Integrable (llr μ ν) μ
hfν : Integrable (fun x ↦ rexp (f x)) ν
⊢ Integrable (llr μ (ν.tilted f)) μ

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Trim

Goal state before:
pp: α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : α → ℝ≥0∞
hf : Measurable f
a : ℝ≥0∞
h_meas_eq : μ {x | ¬f x ≤ a} = (μ.trim hm) {x | ¬f x ≤ a}
⊢ a ∈ {a | ∀ᵐ (n : α) ∂μ.trim hm, f n ≤ a} ↔ a ∈ {a | ∀ᵐ (n : α) ∂μ, f n ≤ a}

Tactic:
by

Goal state after: