mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Probability.Kernel.Composition.IntegralCompProd

Goal state before:
pp: case pos.h_add
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : NormedAddCommGroup E
a : α
κ : Kernel α β
η : Kernel β γ
inst✝ : NormedSpace ℝ E
f✝ : γ → E
hE : CompleteSpace E
⊢ ∀ ⦃f g : γ → E⦄,
    Disjoint (support f) (support g) →
      Integrable f ((η ∘ₖ κ) a) →
        Integrable g ((η ∘ₖ κ) a) →
          ∫ (z : γ), f z ∂(η ∘ₖ κ) a = ∫ (x : β), ∫ (y : γ), f y ∂η x ∂κ a →
            ∫ (z : γ), g z ∂(η ∘ₖ κ) a = ∫ (x : β), ∫ (y : γ), g y ∂η x ∂κ a →
              ∫ (z : γ), (f + g) z ∂(η ∘ₖ κ) a = ∫ (x : β), ∫ (y : γ), (f + g) y ∂η x ∂κ a

pp: case h_closed
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : NormedAddCommGroup E
a : α
κ : Kernel α β
η : Kernel β γ
inst✝ : NormedSpace ℝ E
f✝ : γ → E
hE : CompleteSpace E
⊢ IsClosed {f | ∫ (z : γ), ↑↑f z ∂(η ∘ₖ κ) a = ∫ (x : β), ∫ (y : γ), ↑↑f y ∂η x ∂κ a}

pp: case h_ae
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : NormedAddCommGroup E
a : α
κ : Kernel α β
η : Kernel β γ
inst✝ : NormedSpace ℝ E
f✝ : γ → E
hE : CompleteSpace E
⊢ ∀ ⦃f g : γ → E⦄,
    f =ᵐ[(η ∘ₖ κ) a] g →
      Integrable f ((η ∘ₖ κ) a) →
        ∫ (z : γ), f z ∂(η ∘ₖ κ) a = ∫ (x : β), ∫ (y : γ), f y ∂η x ∂κ a →
          ∫ (z : γ), g z ∂(η ∘ₖ κ) a = ∫ (x : β), ∫ (y : γ), g y ∂η x ∂κ a

Tactic:
·

Goal state after:
case pos.h_add
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : NormedAddCommGroup E
a : α
κ : Kernel α β
η : Kernel β γ
inst✝ : NormedSpace ℝ E
f✝ : γ → E
hE : CompleteSpace E
⊢ ∀ ⦃f g : γ → E⦄,
    Disjoint (support f) (support g) →
      Integrable f ((η ∘ₖ κ) a) →
        Integrable g ((η ∘ₖ κ) a) →
          ∫ (z : γ), f z ∂(η ∘ₖ κ) a = ∫ (x : β), ∫ (y : γ), f y ∂η x ∂κ a →
            ∫ (z : γ), g z ∂(η ∘ₖ κ) a = ∫ (x : β), ∫ (y : γ), g y ∂η x ∂κ a →
              ∫ (z : γ), (f + g) z ∂(η ∘ₖ κ) a = ∫ (x : β), ∫ (y : γ), (f + g) y ∂η x ∂κ a
Module: Mathlib.MeasureTheory.Measure.LogLikelihoodRatio

Goal state before:
pp: case hy
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : μ.HaveLebesgueDecomposition ν
hμν : μ ≪ ν
c : ℝ≥0∞
hc : c ≠ 0
hc_ne_top : c ≠ ∞
h : μ.rnDeriv (c • ν) =ᵐ[ν] c⁻¹ • μ.rnDeriv ν
x : α
hx_eq : μ.rnDeriv (c • ν) x = (c⁻¹ • μ.rnDeriv ν) x
hx_pos : 0 < μ.rnDeriv ν x
hx_ne_top : μ.rnDeriv ν x < ∞
⊢ (μ.rnDeriv ν x).toReal ≠ 0

pp: α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : μ.HaveLebesgueDecomposition ν
hμν : μ ≪ ν
c : ℝ≥0∞
hc : c ≠ 0
hc_ne_top : c ≠ ∞
h : μ.rnDeriv (c • ν) =ᵐ[ν] c⁻¹ • μ.rnDeriv ν
x : α
hx_eq : μ.rnDeriv (c • ν) x = (c⁻¹ • μ.rnDeriv ν) x
hx_pos : 0 < μ.rnDeriv ν x
hx_ne_top : μ.rnDeriv ν x < ∞
⊢ log c⁻¹.toReal + log (μ.rnDeriv ν x).toReal = log (μ.rnDeriv ν x).toReal - log c.toReal

Tactic:
·

Goal state after:
case hy
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : μ.HaveLebesgueDecomposition ν
hμν : μ ≪ ν
c : ℝ≥0∞
hc : c ≠ 0
hc_ne_top : c ≠ ∞
h : μ.rnDeriv (c • ν) =ᵐ[ν] c⁻¹ • μ.rnDeriv ν
x : α
hx_eq : μ.rnDeriv (c • ν) x = (c⁻¹ • μ.rnDeriv ν) x
hx_pos : 0 < μ.rnDeriv ν x
hx_ne_top : μ.rnDeriv ν x < ∞
⊢ (μ.rnDeriv ν x).toReal ≠ 0
Module: Mathlib.Probability.Kernel.Composition.IntegralCompProd

Goal state before:
pp: case h_closed
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : NormedAddCommGroup E
a : α
κ : Kernel α β
η : Kernel β γ
inst✝ : NormedSpace ℝ E
f✝ : γ → E
hE : CompleteSpace E
⊢ IsClosed {f | ∫ (z : γ), ↑↑f z ∂(η ∘ₖ κ) a = ∫ (x : β), ∫ (y : γ), ↑↑f y ∂η x ∂κ a}

pp: case h_ae
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : NormedAddCommGroup E
a : α
κ : Kernel α β
η : Kernel β γ
inst✝ : NormedSpace ℝ E
f✝ : γ → E
hE : CompleteSpace E
⊢ ∀ ⦃f g : γ → E⦄,
    f =ᵐ[(η ∘ₖ κ) a] g →
      Integrable f ((η ∘ₖ κ) a) →
        ∫ (z : γ), f z ∂(η ∘ₖ κ) a = ∫ (x : β), ∫ (y : γ), f y ∂η x ∂κ a →
          ∫ (z : γ), g z ∂(η ∘ₖ κ) a = ∫ (x : β), ∫ (y : γ), g y ∂η x ∂κ a

Tactic:
·

Goal state after:
case h_closed
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : NormedAddCommGroup E
a : α
κ : Kernel α β
η : Kernel β γ
inst✝ : NormedSpace ℝ E
f✝ : γ → E
hE : CompleteSpace E
⊢ IsClosed {f | ∫ (z : γ), ↑↑f z ∂(η ∘ₖ κ) a = ∫ (x : β), ∫ (y : γ), ↑↑f y ∂η x ∂κ a}
Module: Mathlib.MeasureTheory.Measure.Tilted

Goal state before:
pp: case inr.refine_1
α : Type u_1
mα : MeasurableSpace α
f : α → ℝ
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hf : Integrable (fun x ↦ rexp (f x)) ν
h0 : NeZero ν
⊢ AEMeasurable (fun x ↦ ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂ν)) ν

pp: case inr.refine_2
α : Type u_1
mα : MeasurableSpace α
f : α → ℝ
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hf : Integrable (fun x ↦ rexp (f x)) ν
h0 : NeZero ν
⊢ ∀ᵐ (x : α) ∂ν, ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂ν) ≠ 0

pp: case inr.refine_3
α : Type u_1
mα : MeasurableSpace α
f : α → ℝ
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hf : Integrable (fun x ↦ rexp (f x)) ν
h0 : NeZero ν
⊢ ∀ᵐ (x : α) ∂ν, ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂ν) ≠ ∞

pp: case inr.refine_4
α : Type u_1
mα : MeasurableSpace α
f : α → ℝ
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hf : Integrable (fun x ↦ rexp (f x)) ν
h0 : NeZero ν
⊢ (fun x ↦ (ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂ν))⁻¹ * μ.rnDeriv ν x) =ᵐ[ν] fun x ↦
    ENNReal.ofReal (rexp (-f x) * ∫ (x : α), rexp (f x) ∂ν) * μ.rnDeriv ν x

Tactic:
·

Goal state after:
case inr.refine_1
α : Type u_1
mα : MeasurableSpace α
f : α → ℝ
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hf : Integrable (fun x ↦ rexp (f x)) ν
h0 : NeZero ν
⊢ AEMeasurable (fun x ↦ ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂ν)) ν
Module: Mathlib.MeasureTheory.Measure.Tilted

Goal state before:
pp: case inr.refine_2
α : Type u_1
mα : MeasurableSpace α
f : α → ℝ
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hf : Integrable (fun x ↦ rexp (f x)) ν
h0 : NeZero ν
⊢ ∀ᵐ (x : α) ∂ν, ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂ν) ≠ 0

pp: case inr.refine_3
α : Type u_1
mα : MeasurableSpace α
f : α → ℝ
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hf : Integrable (fun x ↦ rexp (f x)) ν
h0 : NeZero ν
⊢ ∀ᵐ (x : α) ∂ν, ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂ν) ≠ ∞

pp: case inr.refine_4
α : Type u_1
mα : MeasurableSpace α
f : α → ℝ
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hf : Integrable (fun x ↦ rexp (f x)) ν
h0 : NeZero ν
⊢ (fun x ↦ (ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂ν))⁻¹ * μ.rnDeriv ν x) =ᵐ[ν] fun x ↦
    ENNReal.ofReal (rexp (-f x) * ∫ (x : α), rexp (f x) ∂ν) * μ.rnDeriv ν x

Tactic:
·

Goal state after:
case inr.refine_2
α : Type u_1
mα : MeasurableSpace α
f : α → ℝ
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hf : Integrable (fun x ↦ rexp (f x)) ν
h0 : NeZero ν
⊢ ∀ᵐ (x : α) ∂ν, ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂ν) ≠ 0
Module: Mathlib.Probability.Kernel.Composition.IntegralCompProd

Goal state before:
pp: case h_ae
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : NormedAddCommGroup E
a : α
κ : Kernel α β
η : Kernel β γ
inst✝ : NormedSpace ℝ E
f✝ : γ → E
hE : CompleteSpace E
⊢ ∀ ⦃f g : γ → E⦄,
    f =ᵐ[(η ∘ₖ κ) a] g →
      Integrable f ((η ∘ₖ κ) a) →
        ∫ (z : γ), f z ∂(η ∘ₖ κ) a = ∫ (x : β), ∫ (y : γ), f y ∂η x ∂κ a →
          ∫ (z : γ), g z ∂(η ∘ₖ κ) a = ∫ (x : β), ∫ (y : γ), g y ∂η x ∂κ a

Tactic:
·

Goal state after:
case h_ae
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : NormedAddCommGroup E
a : α
κ : Kernel α β
η : Kernel β γ
inst✝ : NormedSpace ℝ E
f✝ : γ → E
hE : CompleteSpace E
⊢ ∀ ⦃f g : γ → E⦄,
    f =ᵐ[(η ∘ₖ κ) a] g →
      Integrable f ((η ∘ₖ κ) a) →
        ∫ (z : γ), f z ∂(η ∘ₖ κ) a = ∫ (x : β), ∫ (y : γ), f y ∂η x ∂κ a →
          ∫ (z : γ), g z ∂(η ∘ₖ κ) a = ∫ (x : β), ∫ (y : γ), g y ∂η x ∂κ a
Module: Mathlib.MeasureTheory.Measure.Tilted

Goal state before:
pp: case inr.refine_3
α : Type u_1
mα : MeasurableSpace α
f : α → ℝ
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hf : Integrable (fun x ↦ rexp (f x)) ν
h0 : NeZero ν
⊢ ∀ᵐ (x : α) ∂ν, ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂ν) ≠ ∞

pp: case inr.refine_4
α : Type u_1
mα : MeasurableSpace α
f : α → ℝ
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hf : Integrable (fun x ↦ rexp (f x)) ν
h0 : NeZero ν
⊢ (fun x ↦ (ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂ν))⁻¹ * μ.rnDeriv ν x) =ᵐ[ν] fun x ↦
    ENNReal.ofReal (rexp (-f x) * ∫ (x : α), rexp (f x) ∂ν) * μ.rnDeriv ν x

Tactic:
·

Goal state after:
case inr.refine_3
α : Type u_1
mα : MeasurableSpace α
f : α → ℝ
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hf : Integrable (fun x ↦ rexp (f x)) ν
h0 : NeZero ν
⊢ ∀ᵐ (x : α) ∂ν, ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂ν) ≠ ∞
Module: Mathlib.Probability.Kernel.Composition.IntegralCompProd

Goal state before:
pp: case e'_2
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : NormedAddCommGroup E
a : α
κ : Kernel α β
η : Kernel β γ
inst✝ : NormedSpace ℝ E
f✝ : γ → E
hE : CompleteSpace E
f g : γ → E
hfg : f =ᵐ[(η ∘ₖ κ) a] g
hf : ∫ (z : γ), f z ∂(η ∘ₖ κ) a = ∫ (x : β), ∫ (y : γ), f y ∂η x ∂κ a
⊢ ∫ (z : γ), g z ∂(η ∘ₖ κ) a = ∫ (z : γ), f z ∂(η ∘ₖ κ) a

pp: case e'_3
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : NormedAddCommGroup E
a : α
κ : Kernel α β
η : Kernel β γ
inst✝ : NormedSpace ℝ E
f✝ : γ → E
hE : CompleteSpace E
f g : γ → E
hfg : f =ᵐ[(η ∘ₖ κ) a] g
hf : ∫ (z : γ), f z ∂(η ∘ₖ κ) a = ∫ (x : β), ∫ (y : γ), f y ∂η x ∂κ a
⊢ ∫ (x : β), ∫ (y : γ), g y ∂η x ∂κ a = ∫ (x : β), ∫ (y : γ), f y ∂η x ∂κ a

Tactic:
·

Goal state after:
case e'_2
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : NormedAddCommGroup E
a : α
κ : Kernel α β
η : Kernel β γ
inst✝ : NormedSpace ℝ E
f✝ : γ → E
hE : CompleteSpace E
f g : γ → E
hfg : f =ᵐ[(η ∘ₖ κ) a] g
hf : ∫ (z : γ), f z ∂(η ∘ₖ κ) a = ∫ (x : β), ∫ (y : γ), f y ∂η x ∂κ a
⊢ ∫ (z : γ), g z ∂(η ∘ₖ κ) a = ∫ (z : γ), f z ∂(η ∘ₖ κ) a
Module: Mathlib.MeasureTheory.Measure.Tilted

Goal state before:
pp: case inr.refine_4
α : Type u_1
mα : MeasurableSpace α
f : α → ℝ
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hf : Integrable (fun x ↦ rexp (f x)) ν
h0 : NeZero ν
⊢ (fun x ↦ (ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂ν))⁻¹ * μ.rnDeriv ν x) =ᵐ[ν] fun x ↦
    ENNReal.ofReal (rexp (-f x) * ∫ (x : α), rexp (f x) ∂ν) * μ.rnDeriv ν x

Tactic:
·

Goal state after:
case inr.refine_4
α : Type u_1
mα : MeasurableSpace α
f : α → ℝ
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hf : Integrable (fun x ↦ rexp (f x)) ν
h0 : NeZero ν
⊢ (fun x ↦ (ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂ν))⁻¹ * μ.rnDeriv ν x) =ᵐ[ν] fun x ↦
    ENNReal.ofReal (rexp (-f x) * ∫ (x : α), rexp (f x) ∂ν) * μ.rnDeriv ν x
Module: Mathlib.Probability.Kernel.Composition.IntegralCompProd

Goal state before:
pp: case e'_3
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : NormedAddCommGroup E
a : α
κ : Kernel α β
η : Kernel β γ
inst✝ : NormedSpace ℝ E
f✝ : γ → E
hE : CompleteSpace E
f g : γ → E
hfg : f =ᵐ[(η ∘ₖ κ) a] g
hf : ∫ (z : γ), f z ∂(η ∘ₖ κ) a = ∫ (x : β), ∫ (y : γ), f y ∂η x ∂κ a
⊢ ∫ (x : β), ∫ (y : γ), g y ∂η x ∂κ a = ∫ (x : β), ∫ (y : γ), f y ∂η x ∂κ a

Tactic:
·

Goal state after:
case e'_3
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : NormedAddCommGroup E
a : α
κ : Kernel α β
η : Kernel β γ
inst✝ : NormedSpace ℝ E
f✝ : γ → E
hE : CompleteSpace E
f g : γ → E
hfg : f =ᵐ[(η ∘ₖ κ) a] g
hf : ∫ (z : γ), f z ∂(η ∘ₖ κ) a = ∫ (x : β), ∫ (y : γ), f y ∂η x ∂κ a
⊢ ∫ (x : β), ∫ (y : γ), g y ∂η x ∂κ a = ∫ (x : β), ∫ (y : γ), f y ∂η x ∂κ a
Module: Mathlib.Probability.Kernel.Composition.IntegralCompProd

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : NormedAddCommGroup E
a : α
κ : Kernel α β
η : Kernel β γ
inst✝ : NormedSpace ℝ E
f : γ → E
s : Set γ
hs : MeasurableSet s
hf : IntegrableOn f s ((η ∘ₖ κ) a)
⊢ ∫ (x : β), ∫ (y : γ), f y ∂(η.restrict hs) x ∂κ a = ∫ (x : β), ∫ (y : γ) in s, f y ∂η x ∂κ a

pp: α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : NormedAddCommGroup E
a : α
κ : Kernel α β
η : Kernel β γ
inst✝ : NormedSpace ℝ E
f : γ → E
s : Set γ
hs : MeasurableSet s
hf : IntegrableOn f s ((η ∘ₖ κ) a)
⊢ Integrable f ((η.restrict hs ∘ₖ κ) a)

Tactic:
·

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : NormedAddCommGroup E
a : α
κ : Kernel α β
η : Kernel β γ
inst✝ : NormedSpace ℝ E
f : γ → E
s : Set γ
hs : MeasurableSet s
hf : IntegrableOn f s ((η ∘ₖ κ) a)
⊢ ∫ (x : β), ∫ (y : γ), f y ∂(η.restrict hs) x ∂κ a = ∫ (x : β), ∫ (y : γ) in s, f y ∂η x ∂κ a
Module: Mathlib.MeasureTheory.Measure.Tilted

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

Tactic:
filter_upwards [rnDeriv_tilted_right μ ν hf] with x hx
  rw [hx]
  simp only [ENNReal.toReal_mul, mul_eq_mul_right_iff, ENNReal.toReal_ofReal_eq_iff]
  exact Or.inl (by positivity)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : NormedAddCommGroup E
a : α
κ : Kernel α β
η : Kernel β γ
inst✝ : NormedSpace ℝ E
f : γ → E
s : Set γ
hs : MeasurableSet s
hf : IntegrableOn f s ((η ∘ₖ κ) a)
⊢ Integrable f ((η.restrict hs ∘ₖ κ) a)

Tactic:
·

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : NormedAddCommGroup E
a : α
κ : Kernel α β
η : Kernel β γ
inst✝ : NormedSpace ℝ E
f : γ → E
s : Set γ
hs : MeasurableSet s
hf : IntegrableOn f s ((η ∘ₖ κ) a)
⊢ Integrable f ((η.restrict hs ∘ₖ κ) a)
Module: Mathlib.MeasureTheory.Measure.Tilted

Goal state before:
pp: case refine_1
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hfν : AEMeasurable f ν
g : α → ℝ≥0∞ := fun x ↦ ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ)
⊢ AEMeasurable g ν

pp: case refine_2
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hfν : AEMeasurable f ν
g : α → ℝ≥0∞ := fun x ↦ ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ)
⊢ ∀ᵐ (x : α) ∂μ, g x ≠ ∞

Tactic:
·

Goal state after:
case refine_1
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hfν : AEMeasurable f ν
g : α → ℝ≥0∞ := fun x ↦ ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ)
⊢ AEMeasurable g ν
Module: Mathlib.MeasureTheory.Measure.Tilted

Goal state before:
pp: case refine_2
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hfν : AEMeasurable f ν
g : α → ℝ≥0∞ := fun x ↦ ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ)
⊢ ∀ᵐ (x : α) ∂μ, g x ≠ ∞

Tactic:
·

Goal state after:
case refine_2
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hfν : AEMeasurable f ν
g : α → ℝ≥0∞ := fun x ↦ ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ)
⊢ ∀ᵐ (x : α) ∂μ, g x ≠ ∞
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 ν
h0 : NeZero μ
x : α
hx : ((μ.tilted f).rnDeriv ν x).toReal = (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) * (μ.rnDeriv ν x).toReal
hx_pos : 0 < μ.rnDeriv ν x
hx_lt_top : μ.rnDeriv ν x < ∞
⊢ (∫ (x : α), rexp (f x) ∂μ)⁻¹ ≠ 0

pp: case hx
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
f : α → ℝ
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
hf : Integrable (fun x ↦ rexp (f x)) μ
hfν : AEMeasurable f ν
h0 : NeZero μ
x : α
hx : ((μ.tilted f).rnDeriv ν x).toReal = (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) * (μ.rnDeriv ν x).toReal
hx_pos : 0 < μ.rnDeriv ν x
hx_lt_top : μ.rnDeriv ν x < ∞
⊢ rexp (f x) / ∫ (x : α), rexp (f x) ∂μ ≠ 0

pp: case hy
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
f : α → ℝ
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
hf : Integrable (fun x ↦ rexp (f x)) μ
hfν : AEMeasurable f ν
h0 : NeZero μ
x : α
hx : ((μ.tilted f).rnDeriv ν x).toReal = (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) * (μ.rnDeriv ν x).toReal
hx_pos : 0 < μ.rnDeriv ν x
hx_lt_top : μ.rnDeriv ν x < ∞
⊢ (μ.rnDeriv ν x).toReal ≠ 0

Tactic:
·

Goal state after:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
f : α → ℝ
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
hf : Integrable (fun x ↦ rexp (f x)) μ
hfν : AEMeasurable f ν
h0 : NeZero μ
x : α
hx : ((μ.tilted f).rnDeriv ν x).toReal = (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) * (μ.rnDeriv ν x).toReal
hx_pos : 0 < μ.rnDeriv ν x
hx_lt_top : μ.rnDeriv ν x < ∞
⊢ (∫ (x : α), rexp (f x) ∂μ)⁻¹ ≠ 0
Module: Mathlib.MeasureTheory.Measure.LogLikelihoodRatio

Goal state before:
pp: case hx
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
f : α → ℝ
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
hf : Integrable (fun x ↦ rexp (f x)) μ
hfν : AEMeasurable f ν
h0 : NeZero μ
x : α
hx : ((μ.tilted f).rnDeriv ν x).toReal = (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) * (μ.rnDeriv ν x).toReal
hx_pos : 0 < μ.rnDeriv ν x
hx_lt_top : μ.rnDeriv ν x < ∞
⊢ rexp (f x) / ∫ (x : α), rexp (f x) ∂μ ≠ 0

pp: case hy
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
f : α → ℝ
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
hf : Integrable (fun x ↦ rexp (f x)) μ
hfν : AEMeasurable f ν
h0 : NeZero μ
x : α
hx : ((μ.tilted f).rnDeriv ν x).toReal = (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) * (μ.rnDeriv ν x).toReal
hx_pos : 0 < μ.rnDeriv ν x
hx_lt_top : μ.rnDeriv ν x < ∞
⊢ (μ.rnDeriv ν x).toReal ≠ 0

Tactic:
·

Goal state after:
case hx
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
f : α → ℝ
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
hf : Integrable (fun x ↦ rexp (f x)) μ
hfν : AEMeasurable f ν
h0 : NeZero μ
x : α
hx : ((μ.tilted f).rnDeriv ν x).toReal = (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) * (μ.rnDeriv ν x).toReal
hx_pos : 0 < μ.rnDeriv ν x
hx_lt_top : μ.rnDeriv ν x < ∞
⊢ rexp (f x) / ∫ (x : α), rexp (f x) ∂μ ≠ 0
Module: Mathlib.MeasureTheory.Measure.LogLikelihoodRatio

Goal state before:
pp: case hy
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
f : α → ℝ
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
hf : Integrable (fun x ↦ rexp (f x)) μ
hfν : AEMeasurable f ν
h0 : NeZero μ
x : α
hx : ((μ.tilted f).rnDeriv ν x).toReal = (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) * (μ.rnDeriv ν x).toReal
hx_pos : 0 < μ.rnDeriv ν x
hx_lt_top : μ.rnDeriv ν x < ∞
⊢ (μ.rnDeriv ν x).toReal ≠ 0

Tactic:
·

Goal state after:
case hy
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
f : α → ℝ
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
hf : Integrable (fun x ↦ rexp (f x)) μ
hfν : AEMeasurable f ν
h0 : NeZero μ
x : α
hx : ((μ.tilted f).rnDeriv ν x).toReal = (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) * (μ.rnDeriv ν x).toReal
hx_pos : 0 < μ.rnDeriv ν x
hx_lt_top : μ.rnDeriv ν x < ∞
⊢ (μ.rnDeriv ν x).toReal ≠ 0
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 ν
⊢ Integrable (fun x ↦ f x - log (∫ (x : α), rexp (f x) ∂μ)) μ

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 ν
⊢ ∫ (a : α), f a - log (∫ (x : α), rexp (f x) ∂μ) ∂μ + ∫ (a : α), llr μ ν a ∂μ =
    ∫ (x : α), f x ∂μ - log (∫ (x : α), rexp (f x) ∂μ) + ∫ (x : α), llr μ ν x ∂μ

Tactic:
·

Goal state after:
α : 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 ν
⊢ Integrable (fun x ↦ f x - log (∫ (x : α), rexp (f x) ∂μ)) μ
Module: Mathlib.InformationTheory.KullbackLeibler.KLFun

Goal state before:
pp: case pos
x : ℝ
h0 : x = 0
⊢ deriv klFun x = log x

pp: case neg
x : ℝ
h0 : ¬x = 0
⊢ deriv klFun x = log x

Tactic:
·

Goal state after:
case pos
x : ℝ
h0 : x = 0
⊢ deriv klFun x = log x
Module: Mathlib.InformationTheory.KullbackLeibler.KLFun

Goal state before:
pp: case neg
x : ℝ
h0 : ¬x = 0
⊢ deriv klFun x = log x

Tactic:
·

Goal state after:
case neg
x : ℝ
h0 : ¬x = 0
⊢ deriv klFun x = log x
Module: Mathlib.InformationTheory.KullbackLeibler.KLFun

Goal state before:
pp: case pos
x : ℝ
h0 : x = 0
⊢ derivWithin klFun (Ioi x) x = log x

pp: case neg
x : ℝ
h0 : ¬x = 0
⊢ derivWithin klFun (Ioi x) x = log x

Tactic:
·

Goal state after:
case pos
x : ℝ
h0 : x = 0
⊢ derivWithin klFun (Ioi x) x = log x
Module: Mathlib.InformationTheory.KullbackLeibler.KLFun

Goal state before:
pp: case neg
x : ℝ
h0 : ¬x = 0
⊢ derivWithin klFun (Ioi x) x = log x

Tactic:
·

Goal state after:
case neg
x : ℝ
h0 : ¬x = 0
⊢ derivWithin klFun (Ioi x) x = log x
Module: Mathlib.InformationTheory.KullbackLeibler.KLFun

Goal state before:
pp: case pos
x : ℝ
h0 : x = 0
⊢ derivWithin klFun (Iio x) x = log x

pp: case neg
x : ℝ
h0 : ¬x = 0
⊢ derivWithin klFun (Iio x) x = log x

Tactic:
·

Goal state after:
case pos
x : ℝ
h0 : x = 0
⊢ derivWithin klFun (Iio x) x = log x
Module: Mathlib.InformationTheory.KullbackLeibler.KLFun

Goal state before:
pp: case neg
x : ℝ
h0 : ¬x = 0
⊢ derivWithin klFun (Iio x) x = log x

Tactic:
·

Goal state after:
case neg
x : ℝ
h0 : ¬x = 0
⊢ derivWithin klFun (Iio x) x = log x
Module: Mathlib.InformationTheory.KullbackLeibler.Basic

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
h : llr μ μ =ᵐ[μ] 0
⊢ ENNReal.ofReal (∫ (x : α), llr μ μ x ∂μ + μ.real univ - μ.real univ) = 0

pp: case hc
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
h : llr μ μ =ᵐ[μ] 0
⊢ μ ≪ μ ∧ Integrable (llr μ μ) μ

Tactic:
·

Goal state after:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
h : llr μ μ =ᵐ[μ] 0
⊢ ENNReal.ofReal (∫ (x : α), llr μ μ x ∂μ + μ.real univ - μ.real univ) = 0
Module: Mathlib.InformationTheory.KullbackLeibler.Basic

Goal state before:
pp: case hc
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
h : llr μ μ =ᵐ[μ] 0
⊢ μ ≪ μ ∧ Integrable (llr μ μ) μ

Tactic:
·

Goal state after:
case hc
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
h : llr μ μ =ᵐ[μ] 0
⊢ μ ≪ μ ∧ Integrable (llr μ μ) μ