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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst✝¹ : SFinite μ
inst✝ : IsSFiniteKernel κ
h_zero : ∀ (a : α), NeZero (κ a)
h : μ ⊗ₘ κ ≪ ν ⊗ₘ η
⊢ μ ≪ ν

Tactic:
by
  refine Measure.AbsolutelyContinuous.mk (fun s hs hs0 ↦ ?_)
  have h1 : (ν ⊗ₘ η) (s ×ˢ univ) = 0 := by
    by_cases hν : SFinite ν
    swap; · simp [compProd_of_not_sfinite _ _ hν]
    by_cases hη : IsSFiniteKernel η
    swap; · simp [compProd_of_not_isSFiniteKernel _ _ hη]
    rw [Measure.compProd_apply_prod hs MeasurableSet.univ]
    exact setLIntegral_measure_zero _ _ hs0
  have h2 : (μ ⊗ₘ κ) (s ×ˢ univ) = 0 := h h1
  rw [Measure.compProd_apply_prod hs MeasurableSet.univ, lintegral_eq_zero_iff] at h2
  swap; · exact Kernel.measurable_coe _ MeasurableSet.univ
  by_contra hμs
  have : Filter.NeBot (ae (μ.restrict s)) := by simp [hμs]
  obtain ⟨a, ha⟩ : ∃ a, κ a univ = 0 := h2.exists
  refine absurd ha ?_
  simp only [Measure.measure_univ_eq_zero]
  exact (h_zero a).out

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ✝ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ✝ : MeasurableSpace γ✝
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
h : IsZeroOrMarkovKernel κ
η : Kernel α γ
inst✝ : IsZeroOrMarkovKernel η
⊢ IsZeroOrMarkovKernel (κ ×ₖ η)

Tactic:
rcases eq_zero_or_isMarkovKernel κ with rfl | h

Goal state after:
case inl
α : Type u_1
β : Type u_2
γ✝ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ✝ : MeasurableSpace γ✝
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
η : Kernel α γ
inst✝ : IsZeroOrMarkovKernel η
h : IsZeroOrMarkovKernel 0
⊢ IsZeroOrMarkovKernel (0 ×ₖ η)

case inr
α : Type u_1
β : Type u_2
γ✝ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ✝ : MeasurableSpace γ✝
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
h✝ : IsZeroOrMarkovKernel κ
η : Kernel α γ
inst✝ : IsZeroOrMarkovKernel η
h : IsMarkovKernel κ
⊢ IsZeroOrMarkovKernel (κ ×ₖ η)
Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
ξ : Measure α
inst✝³ : SFinite μ
inst✝² : SFinite ν
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
h : μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ η
hμ : ξ ≪ μ
hν : ξ ≪ ν
hs : MeasurableSet h.nullSet
hμ_zero : ∫⁻ (a : α), (κ a) (Prod.mk a ⁻¹' h.nullSet) ∂μ = 0
hν_zero : ∫⁻ (a : α), (η a) (Prod.mk a ⁻¹' h.nullSetᶜ) ∂ν = 0
⊢ AEMeasurable (fun a ↦ (κ a) (Prod.mk a ⁻¹' h.nullSet)) μ

pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
ξ : Measure α
inst✝³ : SFinite μ
inst✝² : SFinite ν
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
h : μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ η
hμ : ξ ≪ μ
hν : ξ ≪ ν
hs : MeasurableSet h.nullSet
hμ_zero : ∫⁻ (a : α), (κ a) (Prod.mk a ⁻¹' h.nullSet) ∂μ = 0
hν_zero : (ν ⊗ₘ η) h.nullSetᶜ = 0
⊢ MeasurableSet h.nullSetᶜ

pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
ξ : Measure α
inst✝³ : SFinite μ
inst✝² : SFinite ν
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
h : μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ η
hμ : ξ ≪ μ
hν : ξ ≪ ν
hs : MeasurableSet h.nullSet
hμ_zero : (μ ⊗ₘ κ) h.nullSet = 0
hν_zero : (ν ⊗ₘ η) h.nullSetᶜ = 0
⊢ MeasurableSet h.nullSet

Tactic:
· exact (Kernel.measurable_kernel_prodMk_left hs).aemeasurable

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
ξ : Measure α
inst✝³ : SFinite μ
inst✝² : SFinite ν
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
h : μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ η
hμ : ξ ≪ μ
hν : ξ ≪ ν
hs : MeasurableSet h.nullSet
hμ_zero : ∫⁻ (a : α), (κ a) (Prod.mk a ⁻¹' h.nullSet) ∂μ = 0
hν_zero : (ν ⊗ₘ η) h.nullSetᶜ = 0
⊢ MeasurableSet h.nullSetᶜ

α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
ξ : Measure α
inst✝³ : SFinite μ
inst✝² : SFinite ν
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
h : μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ η
hμ : ξ ≪ μ
hν : ξ ≪ ν
hs : MeasurableSet h.nullSet
hμ_zero : (μ ⊗ₘ κ) h.nullSet = 0
hν_zero : (ν ⊗ₘ η) h.nullSetᶜ = 0
⊢ MeasurableSet h.nullSet
Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd

Goal state before:
pp: case refine_3
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ : Kernel α β
inst✝² : SFinite μ
inst✝¹ : SigmaFinite ν
inst✝ : IsSFiniteKernel κ
hκ : ∀ (x : α), NeZero (κ x)
h : μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ κ
hh : ∀ᵐ (x : α) ∂ν.withDensity (μ.rnDeriv ν), κ x ⟂ₘ κ x
⊢ ν.withDensity (μ.rnDeriv ν) = 0

pp: case refine_1
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ : Kernel α β
inst✝² : SFinite μ
inst✝¹ : SigmaFinite ν
inst✝ : IsSFiniteKernel κ
hκ : ∀ (x : α), NeZero (κ x)
h : μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ κ
⊢ ν.withDensity (μ.rnDeriv ν) ≪ μ

pp: case refine_2
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ : Kernel α β
inst✝² : SFinite μ
inst✝¹ : SigmaFinite ν
inst✝ : IsSFiniteKernel κ
hκ : ∀ (x : α), NeZero (κ x)
h : μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ κ
⊢ ν.withDensity (μ.rnDeriv ν) ≪ ν

Tactic:
rotate_left

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ : Kernel α β
inst✝² : SFinite μ
inst✝¹ : SigmaFinite ν
inst✝ : IsSFiniteKernel κ
hκ : ∀ (x : α), NeZero (κ x)
h : μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ κ
⊢ ν.withDensity (μ.rnDeriv ν) ≪ μ

case refine_2
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ : Kernel α β
inst✝² : SFinite μ
inst✝¹ : SigmaFinite ν
inst✝ : IsSFiniteKernel κ
hκ : ∀ (x : α), NeZero (κ x)
h : μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ κ
⊢ ν.withDensity (μ.rnDeriv ν) ≪ ν

case refine_3
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ : Kernel α β
inst✝² : SFinite μ
inst✝¹ : SigmaFinite ν
inst✝ : IsSFiniteKernel κ
hκ : ∀ (x : α), NeZero (κ x)
h : μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ κ
hh : ∀ᵐ (x : α) ∂ν.withDensity (μ.rnDeriv ν), κ x ⟂ₘ κ x
⊢ ν.withDensity (μ.rnDeriv ν) = 0
Module: Mathlib.Probability.Kernel.Composition.CompProd

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set (β × γ)
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
a : α
h2s : ((κ ⊗ₖ η) a) s ≠ ∞
t : Set (β × γ) := toMeasurable ((κ ⊗ₖ η) a) s
this : ∀ (b : β), (η (a, b)) (Prod.mk b ⁻¹' s) ≤ (η (a, b)) (Prod.mk b ⁻¹' t)
ht : MeasurableSet t
⊢ ∀ᵐ (b : β) ∂κ a, (η (a, b)) (Prod.mk b ⁻¹' s) < ∞

Tactic:
have h2t : (κ ⊗ₖ η) a t ≠ ∞ := by rwa [measure_toMeasurable]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set (β × γ)
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
a : α
h2s : ((κ ⊗ₖ η) a) s ≠ ∞
t : Set (β × γ) := toMeasurable ((κ ⊗ₖ η) a) s
this : ∀ (b : β), (η (a, b)) (Prod.mk b ⁻¹' s) ≤ (η (a, b)) (Prod.mk b ⁻¹' t)
ht : MeasurableSet t
h2t : ((κ ⊗ₖ η) a) t ≠ ∞
⊢ ∀ᵐ (b : β) ∂κ a, (η (a, b)) (Prod.mk b ⁻¹' s) < ∞
Module: Mathlib.Probability.Kernel.Composition.MeasureComp

Goal state before:
pp: α : Type u_1
γ : Type u_3
mα : MeasurableSpace α
mγ : MeasurableSpace γ
μ ν : Measure α
hμν : μ ≪ ν
κ : Kernel α γ
s : Set γ
hs : MeasurableSet s
hs_zero : (⇑κ ∘ₘ ν) s = 0
⊢ (⇑κ ∘ₘ μ) s = 0

Tactic:
rw [Measure.bind_apply hs (Kernel.aemeasurable _),
    lintegral_eq_zero_iff (Kernel.measurable_coe _ hs)] at hs_zero ⊢

Goal state after:
α : Type u_1
γ : Type u_3
mα : MeasurableSpace α
mγ : MeasurableSpace γ
μ ν : Measure α
hμν : μ ≪ ν
κ : Kernel α γ
s : Set γ
hs : MeasurableSet s
hs_zero : (fun a ↦ (κ a) s) =ᵐ[ν] 0
⊢ (fun a ↦ (κ a) s) =ᵐ[μ] 0
Module: Mathlib.Probability.Kernel.Composition.MeasureComp

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
μ : Measure α
hκη : ∀ᵐ (a : α) ∂μ, κ a ≪ η a
s : Set β
hs : MeasurableSet s
hs_zero : (⇑η ∘ₘ μ) s = 0
⊢ (⇑κ ∘ₘ μ) s = 0

Tactic:
rw [Measure.bind_apply hs (Kernel.aemeasurable _),
    lintegral_eq_zero_iff (Kernel.measurable_coe _ hs)] at hs_zero ⊢

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
μ : Measure α
hκη : ∀ᵐ (a : α) ∂μ, κ a ≪ η a
s : Set β
hs : MeasurableSet s
hs_zero : (fun a ↦ (η a) s) =ᵐ[μ] 0
⊢ (fun a ↦ (κ a) s) =ᵐ[μ] 0
Module: Mathlib.Probability.Kernel.Composition.CompProd

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
a : α
f : β × γ → ℝ≥0∞
hf : AEMeasurable f ((κ ⊗ₖ η) a)
A : ∫⁻ (z : β × γ), f z ∂(κ ⊗ₖ η) a = ∫⁻ (z : β × γ), AEMeasurable.mk f hf z ∂(κ ⊗ₖ η) a
⊢ ∫⁻ (x : β), ∫⁻ (y : γ), f (x, y) ∂η (a, x) ∂κ a = ∫⁻ (x : β), ∫⁻ (y : γ), AEMeasurable.mk f hf (x, y) ∂η (a, x) ∂κ a

Tactic:
apply lintegral_congr_ae

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
a : α
f : β × γ → ℝ≥0∞
hf : AEMeasurable f ((κ ⊗ₖ η) a)
A : ∫⁻ (z : β × γ), f z ∂(κ ⊗ₖ η) a = ∫⁻ (z : β × γ), AEMeasurable.mk f hf z ∂(κ ⊗ₖ η) a
⊢ (fun a_1 ↦ ∫⁻ (y : γ), f (a_1, y) ∂η (a, a_1)) =ᵐ[κ a] fun a_1 ↦ ∫⁻ (y : γ), AEMeasurable.mk f hf (a_1, y) ∂η (a, a_1)
Module: Mathlib.Probability.Kernel.Composition.IntegralCompProd

Goal state before:
pp: case pos.h_ind.e_a
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝³ : NormedAddCommGroup E
a : α
κ : Kernel α β
inst✝² : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel η
inst✝ : NormedSpace ℝ E
f✝ : β × γ → E
hE : CompleteSpace E
c : E
s : Set (β × γ)
hs : MeasurableSet s
h2s : ((κ ⊗ₖ η) a) s < ∞
⊢ (((κ ⊗ₖ η) a) s).toReal = (∫⁻ (a_1 : β), (η (a, a_1)) (Prod.mk a_1 ⁻¹' s) ∂κ a).toReal

pp: case pos.h_ind.e_a.hfm
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝³ : NormedAddCommGroup E
a : α
κ : Kernel α β
inst✝² : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel η
inst✝ : NormedSpace ℝ E
f✝ : β × γ → E
hE : CompleteSpace E
c : E
s : Set (β × γ)
hs : MeasurableSet s
h2s : ((κ ⊗ₖ η) a) s < ∞
⊢ AEMeasurable (fun x ↦ (η (a, x)) (Prod.mk x ⁻¹' s)) (κ a)

pp: case pos.h_ind.e_a.hf
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝³ : NormedAddCommGroup E
a : α
κ : Kernel α β
inst✝² : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel η
inst✝ : NormedSpace ℝ E
f✝ : β × γ → E
hE : CompleteSpace E
c : E
s : Set (β × γ)
hs : MeasurableSet s
h2s : ((κ ⊗ₖ η) a) s < ∞
⊢ ∀ᵐ (x : β) ∂κ a, (η (a, x)) (Prod.mk x ⁻¹' s) < ∞

Tactic:
rotate_left

Goal state after:
case pos.h_ind.e_a.hfm
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝³ : NormedAddCommGroup E
a : α
κ : Kernel α β
inst✝² : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel η
inst✝ : NormedSpace ℝ E
f✝ : β × γ → E
hE : CompleteSpace E
c : E
s : Set (β × γ)
hs : MeasurableSet s
h2s : ((κ ⊗ₖ η) a) s < ∞
⊢ AEMeasurable (fun x ↦ (η (a, x)) (Prod.mk x ⁻¹' s)) (κ a)

case pos.h_ind.e_a.hf
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝³ : NormedAddCommGroup E
a : α
κ : Kernel α β
inst✝² : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel η
inst✝ : NormedSpace ℝ E
f✝ : β × γ → E
hE : CompleteSpace E
c : E
s : Set (β × γ)
hs : MeasurableSet s
h2s : ((κ ⊗ₖ η) a) s < ∞
⊢ ∀ᵐ (x : β) ∂κ a, (η (a, x)) (Prod.mk x ⁻¹' s) < ∞

case pos.h_ind.e_a
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝³ : NormedAddCommGroup E
a : α
κ : Kernel α β
inst✝² : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel η
inst✝ : NormedSpace ℝ E
f✝ : β × γ → E
hE : CompleteSpace E
c : E
s : Set (β × γ)
hs : MeasurableSet s
h2s : ((κ ⊗ₖ η) a) s < ∞
⊢ (((κ ⊗ₖ η) a) s).toReal = (∫⁻ (a_1 : β), (η (a, a_1)) (Prod.mk a_1 ⁻¹' s) ∂κ a).toReal
Module: Mathlib.MeasureTheory.Measure.Tilted

Goal state before:
pp: case pos.hf
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
g : α → ℝ≥0∞
s : Set α
hs : MeasurableSet s
hf : AEMeasurable f μ
⊢ AEMeasurable (fun x ↦ ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ)) μ

Tactic:
exact ((measurable_exp.comp_aemeasurable hf).div_const _).ennreal_ofReal

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

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

Tactic:
exact ((measurable_exp.comp_aemeasurable hf).div_const _).ennreal_ofReal

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

Goal state before:
pp: case pos
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
f : α → ℝ
g : α → ℝ≥0∞
s : Set α
hf : AEMeasurable f μ
⊢ ∫⁻ (x : α) in s, g x ∂μ.tilted f = ∫⁻ (x : α) in s, ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) * g x ∂μ

Tactic:
rw [Measure.tilted, setLIntegral_withDensity_eq_setLIntegral_mul_non_measurable₀']
    · simp only [Pi.mul_apply]
    · refine AEMeasurable.restrict ?_
      exact ((measurable_exp.comp_aemeasurable hf).div_const _).ennreal_ofReal
    · filter_upwards
      simp only [ENNReal.ofReal_lt_top, implies_true]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
x : α
s : Set β
hs : MeasurableSet s
⊢ ((κ ⊗ₖ η).fst x) s = ∫⁻ (b : β), s.indicator (fun b ↦ (η (x, b)) Set.univ) b ∂κ x

Tactic:
by
  rw [Kernel.fst_apply' _ _ hs, Kernel.compProd_apply]
  swap; · exact measurable_fst hs
  have h_eq b : η (x, b) {c | b ∈ s} = s.indicator (fun b ↦ η (x, b) Set.univ) b := by
    by_cases hb : b ∈ s <;> simp [hb]
  simp_rw [Set.preimage, Set.mem_ofPred_eq, h_eq]

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
x : α
hx : (-llr μ ν) x = llr ν μ x
hx_exp_log : rexp (llr ν μ x) = (ν.rnDeriv μ x).toReal
⊢ rexp (-llr μ ν x) = (ν.rnDeriv μ x).toReal

Tactic:
rw [Pi.neg_apply] at hx

Goal state after:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
x : α
hx : -llr μ ν x = llr ν μ x
hx_exp_log : rexp (llr ν μ x) = (ν.rnDeriv μ x).toReal
⊢ rexp (-llr μ ν x) = (ν.rnDeriv μ x).toReal
Module: Mathlib.MeasureTheory.Measure.LogLikelihoodRatio

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : μ.HaveLebesgueDecomposition ν
hμν : μ ≪ ν
c : ℝ≥0∞
hc : c ≠ 0
hc_ne_top : c ≠ ∞
h : (c • μ).rnDeriv ν =ᵐ[ν] c • μ.rnDeriv ν
x : α
hx_eq : (c • μ).rnDeriv ν 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

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

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

Tactic:
rotate_left

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

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

α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : μ.HaveLebesgueDecomposition ν
hμν : μ ≪ ν
c : ℝ≥0∞
hc : c ≠ 0
hc_ne_top : c ≠ ∞
h : (c • μ).rnDeriv ν =ᵐ[ν] c • μ.rnDeriv ν
x : α
hx_eq : (c • μ).rnDeriv ν 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
Module: Mathlib.MeasureTheory.Measure.LogLikelihoodRatio

Goal state before:
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

pp: case hx
α : 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 < ∞
⊢ c⁻¹.toReal ≠ 0

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

Tactic:
rotate_left

Goal state after:
case hx
α : 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 < ∞
⊢ c⁻¹.toReal ≠ 0

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

α : 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
Module: Mathlib.MeasureTheory.Measure.Tilted

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
inst✝ : SigmaFinite μ
hf : AEMeasurable f μ
⊢ (fun x ↦ ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) * μ.rnDeriv μ x) =ᵐ[μ] fun x ↦
    ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ)

Tactic:
filter_upwards [Measure.rnDeriv_self μ] with x hx

Goal state after:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
inst✝ : SigmaFinite μ
hf : AEMeasurable f μ
x : α
hx : μ.rnDeriv μ x = 1
⊢ ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) * μ.rnDeriv μ x =
    ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ)
Module: Mathlib.InformationTheory.KullbackLeibler.Basic

Goal state before:
pp: case pos.refine_3
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int_iff :
  ∫⁻ (a : α), ENNReal.ofReal (klFun (μ.rnDeriv ν a).toReal) ∂ν ≠ ∞ ↔ Integrable (fun x ↦ klFun (μ.rnDeriv ν x).toReal) ν
⊢ (if μ ≪ ν ∧ Integrable (llr μ ν) μ then ENNReal.ofReal (∫ (x : α), klFun (μ.rnDeriv ν x).toReal ∂ν) else ∞) =
    if μ ≪ ν then ∫⁻ (x : α), ENNReal.ofReal (klFun (μ.rnDeriv ν x).toReal) ∂ν else ∞

pp: case pos.refine_1
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hμν : μ ≪ ν
⊢ AEStronglyMeasurable (fun x ↦ klFun (μ.rnDeriv ν x).toReal) ν

pp: case pos.refine_2
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hμν : μ ≪ ν
⊢ 0 ≤ᵐ[ν] fun x ↦ klFun (μ.rnDeriv ν x).toReal

Tactic:
rotate_left

Goal state after:
case pos.refine_1
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hμν : μ ≪ ν
⊢ AEStronglyMeasurable (fun x ↦ klFun (μ.rnDeriv ν x).toReal) ν

case pos.refine_2
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hμν : μ ≪ ν
⊢ 0 ≤ᵐ[ν] fun x ↦ klFun (μ.rnDeriv ν x).toReal

case pos.refine_3
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int_iff :
  ∫⁻ (a : α), ENNReal.ofReal (klFun (μ.rnDeriv ν a).toReal) ∂ν ≠ ∞ ↔ Integrable (fun x ↦ klFun (μ.rnDeriv ν x).toReal) ν
⊢ (if μ ≪ ν ∧ Integrable (llr μ ν) μ then ENNReal.ofReal (∫ (x : α), klFun (μ.rnDeriv ν x).toReal ∂ν) else ∞) =
    if μ ≪ ν then ∫⁻ (x : α), ENNReal.ofReal (klFun (μ.rnDeriv ν x).toReal) ∂ν else ∞
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:
rw [integrable_congr (llr_tilted_right hμν hfν)]
  exact Integrable.add (hfμ.neg.add (integrable_const _)) h_int

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
c : ℝ≥0
hc : c ≠ 0
⊢ (klDiv μ (c • ν)).toReal = (klDiv μ ν).toReal + (↑c - 1) * ν.real univ - log ↑c * μ.real univ

Tactic:
rw [toReal_klDiv_smul_right_eq_smul_left hμν h_int c, toReal_klDiv_smul_left hμν h_int c⁻¹]
  simp only [NNReal.coe_inv, log_inv, mul_neg, neg_mul, ← sub_eq_add_neg]
  field_simp

Goal state after: