mathlib-initiative/mathlib-tactics huggingface dataset:
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
⊢ (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)

Tactic:
filter_upwards [ae_ae_of_ae_compProd hf.ae_eq_mk] with _ ha using lintegral_congr_ae ha

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

Goal state before:
pp: case inl
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
c : ℝ
h : μ = 0
⊢ (μ.tilted fun x ↦ c) = (μ Set.univ)⁻¹ • μ

Tactic:
| inl h =>

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 β γ
f : γ → E
hf : AEStronglyMeasurable f ((η ∘ₖ κ) a)
⊢ (∀ᵐ (x : β) ∂κ a, HasFiniteIntegral (AEStronglyMeasurable.mk f hf) (η x)) ∧
      HasFiniteIntegral (fun x ↦ ∫ (y : γ), ‖AEStronglyMeasurable.mk f hf y‖ ∂η x) (κ a) ↔
    (∀ᵐ (x : β) ∂κ a, HasFiniteIntegral f (η x)) ∧ HasFiniteIntegral (fun x ↦ ∫ (y : γ), ‖f y‖ ∂η x) (κ a)

Tactic:
refine and_congr (eventually_congr ?_) (hasFiniteIntegral_congr ?_)

Goal state after:
case refine_1
α : 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 β γ
f : γ → E
hf : AEStronglyMeasurable f ((η ∘ₖ κ) a)
⊢ ∀ᵐ (x : β) ∂κ a, HasFiniteIntegral (AEStronglyMeasurable.mk f hf) (η x) ↔ HasFiniteIntegral f (η x)

case refine_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 β γ
f : γ → E
hf : AEStronglyMeasurable f ((η ∘ₖ κ) a)
⊢ (fun x ↦ ∫ (y : γ), ‖AEStronglyMeasurable.mk f hf y‖ ∂η x) =ᵐ[κ a] fun x ↦ ∫ (y : γ), ‖f y‖ ∂η x
Module: Mathlib.MeasureTheory.Measure.Tilted

Goal state before:
pp: case inl
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ
h : μ = 0
⊢ ∫ (x : α), rexp (g x) ∂μ.tilted f = (∫ (x : α), rexp ((f + g) x) ∂μ) / ∫ (x : α), rexp (f x) ∂μ

Tactic:
| inl h =>

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

Goal state before:
pp: case inl
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable (fun x ↦ rexp (f x)) μ
g : α → ℝ
h : μ = 0
⊢ (μ.tilted f).tilted g = μ.tilted (f + g)

Tactic:
| inl h =>

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

Goal state before:
pp: case inl
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable (fun x ↦ rexp (f x)) μ
h : μ = 0
⊢ μ ≪ μ.tilted f

Tactic:
| inl h =>

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ
hf : Integrable (fun x ↦ rexp (f x)) μ
g : α → E
hμ : ¬μ = 0
hf_meas : AEMeasurable f μ
⊢ Integrable (fun x ↦ (ENNReal.ofReal (rexp (f x) / ∫ (a : α), rexp (f a) ∂μ)).toReal • g x) μ ↔
    Integrable (fun x ↦ (rexp (f x) / ∫ (a : α), rexp (f a) ∂μ) • g x) μ

Tactic:
congr! with a

Goal state after:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ
hf : Integrable (fun x ↦ rexp (f x)) μ
g : α → E
hμ : ¬μ = 0
hf_meas : AEMeasurable f μ
a : α
⊢ (ENNReal.ofReal (rexp (f a) / ∫ (a : α), rexp (f a) ∂μ)).toReal = rexp (f a) / ∫ (a : α), rexp (f a) ∂μ
Module: Mathlib.MeasureTheory.Measure.Tilted

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

Tactic:
| inl h =>

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

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

Tactic:
| inl h =>

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

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

Tactic:
· exact (hasDerivAt_klFun h0).deriv

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

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

Tactic:
| inl h =>

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

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

Tactic:
· rcases or_not_of_imp h with (h | h) <;> simp [h]

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

Tactic:
integral_add ?_ (integrable_const _)

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

α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
f : α → ℝ
inst✝¹ : IsProbabilityMeasure μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
hfμ : Integrable f μ
hfν : Integrable (fun x ↦ rexp (f x)) ν
h_int : Integrable (llr μ ν) μ
⊢ Integrable (fun a ↦ -f a) μ
Module: Mathlib.InformationTheory.KullbackLeibler.Basic

Goal state before:
pp: case neg
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
c : ℝ≥0
hc : c ≠ 0
hc' : ↑c ≠ 0
hμ_smul : μ = c • c⁻¹ • μ
hν_smul : ν = c⁻¹ • c • ν
hμν : ¬μ ≪ ν
h_contra : μ ≪ c • ν
⊢ μ ≪ ν

Tactic:
rw [hν_smul]

Goal state after:
case neg
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
c : ℝ≥0
hc : c ≠ 0
hc' : ↑c ≠ 0
hμ_smul : μ = c • c⁻¹ • μ
hν_smul : ν = c⁻¹ • c • ν
hμν : ¬μ ≪ ν
h_contra : μ ≪ c • ν
⊢ μ ≪ c⁻¹ • c • ν
Module: Mathlib.InformationTheory.KullbackLeibler.Basic

Goal state before:
pp: case neg
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
c : ℝ≥0
hc : c ≠ 0
hc' : ↑c ≠ 0
hμ_smul : μ = c • c⁻¹ • μ
hν_smul : ν = c⁻¹ • c • ν
hμν : μ ≪ ν
hμν_right : μ ≪ c • ν
h_int : ¬Integrable (llr μ ν) μ
h_contra : Integrable (llr μ (c • ν)) μ
⊢ Integrable (llr μ ν) μ

Tactic:
rw [hν_smul]

Goal state after:
case neg
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
c : ℝ≥0
hc : c ≠ 0
hc' : ↑c ≠ 0
hμ_smul : μ = c • c⁻¹ • μ
hν_smul : ν = c⁻¹ • c • ν
hμν : μ ≪ ν
hμν_right : μ ≪ c • ν
h_int : ¬Integrable (llr μ ν) μ
h_contra : Integrable (llr μ (c • ν)) μ
⊢ Integrable (llr μ (c⁻¹ • c • ν)) μ
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable

Goal state before:
pp: α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst✝ : NormedAddCommGroup F
m m0 : MeasurableSpace α
μ : Measure α
f : ↥(Lp F p μ)
⊢ f ∈ lpMeasSubgroup F m p μ ↔ AEStronglyMeasurable (↑↑f) μ

Tactic:
← AddSubgroup.mem_carrier,

Goal state after:
α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst✝ : NormedAddCommGroup F
m m0 : MeasurableSpace α
μ : Measure α
f : ↥(Lp F p μ)
⊢ f ∈ (lpMeasSubgroup F m p μ).carrier ↔ AEStronglyMeasurable (↑↑f) μ
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1

Goal state before:
pp: case refine_2
α : Type u_1
F' : Type u_3
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝¹ : SigmaFinite (μ.trim hm)
s : Set α
inst✝ : CompleteSpace F'
f✝ : ↥(Lp F' 1 μ)
hs : MeasurableSet s
hμs : μ s ≠ ∞
f g : α → F'
hf_Lp : MemLp f 1 μ
hg_Lp : MemLp g 1 μ
a✝ : Disjoint (Function.support f) (Function.support g)
hf : ∫ (x : α) in s, ↑↑((condExpL1CLM F' hm μ) (MemLp.toLp f hf_Lp)) x ∂μ = ∫ (x : α) in s, ↑↑(MemLp.toLp f hf_Lp) x ∂μ
hg : ∫ (x : α) in s, ↑↑((condExpL1CLM F' hm μ) (MemLp.toLp g hg_Lp)) x ∂μ = ∫ (x : α) in s, ↑↑(MemLp.toLp g hg_Lp) x ∂μ
⊢ ∫ (x : α) in s, ↑↑((condExpL1CLM F' hm μ) (MemLp.toLp f hf_Lp) + (condExpL1CLM F' hm μ) (MemLp.toLp g hg_Lp)) x ∂μ =
    ∫ (x : α) in s, ↑↑(MemLp.toLp f hf_Lp + MemLp.toLp g hg_Lp) x ∂μ

Tactic:
rw [setIntegral_congr_ae (hm s hs) ((Lp.coeFn_add (condExpL1CLM F' hm μ (hf_Lp.toLp f))
      (condExpL1CLM F' hm μ (hg_Lp.toLp g))).mono fun x hx _ => hx)]

Goal state after:
case refine_2
α : Type u_1
F' : Type u_3
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝¹ : SigmaFinite (μ.trim hm)
s : Set α
inst✝ : CompleteSpace F'
f✝ : ↥(Lp F' 1 μ)
hs : MeasurableSet s
hμs : μ s ≠ ∞
f g : α → F'
hf_Lp : MemLp f 1 μ
hg_Lp : MemLp g 1 μ
a✝ : Disjoint (Function.support f) (Function.support g)
hf : ∫ (x : α) in s, ↑↑((condExpL1CLM F' hm μ) (MemLp.toLp f hf_Lp)) x ∂μ = ∫ (x : α) in s, ↑↑(MemLp.toLp f hf_Lp) x ∂μ
hg : ∫ (x : α) in s, ↑↑((condExpL1CLM F' hm μ) (MemLp.toLp g hg_Lp)) x ∂μ = ∫ (x : α) in s, ↑↑(MemLp.toLp g hg_Lp) x ∂μ
⊢ ∫ (x : α) in s,
      (↑↑((condExpL1CLM F' hm μ) (MemLp.toLp f hf_Lp)) + ↑↑((condExpL1CLM F' hm μ) (MemLp.toLp g hg_Lp))) x ∂μ =
    ∫ (x : α) in s, ↑↑(MemLp.toLp f hf_Lp + MemLp.toLp g hg_Lp) x ∂μ
Module: Mathlib.InformationTheory.KullbackLeibler.ChainRule

Goal state before:
pp: 𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
κ η : Kernel 𝓧 𝓨
inst✝³ : IsFiniteMeasure μ
inst✝² : IsFiniteMeasure ν
inst✝¹ : IsMarkovKernel κ
inst✝ : IsMarkovKernel η
h_ac : μ ⊗ₘ κ ≪ μ ⊗ₘ η
p : 𝓧 × 𝓨
hp : (∂μ ⊗ₘ κ/∂ν ⊗ₘ η) p = (∂μ/∂ν) p.1 * (∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p
⊢ ((∂μ ⊗ₘ κ/∂ν ⊗ₘ η) p).toReal * log ((∂μ ⊗ₘ κ/∂ν ⊗ₘ η) p).toReal =
    ((∂μ ⊗ₘ κ/∂ν ⊗ₘ η) p).toReal * (log ((∂μ/∂ν) p.1).toReal + log ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p).toReal)

Tactic:
simp_rw [hp, ENNReal.toReal_mul]

Goal state after:
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
κ η : Kernel 𝓧 𝓨
inst✝³ : IsFiniteMeasure μ
inst✝² : IsFiniteMeasure ν
inst✝¹ : IsMarkovKernel κ
inst✝ : IsMarkovKernel η
h_ac : μ ⊗ₘ κ ≪ μ ⊗ₘ η
p : 𝓧 × 𝓨
hp : (∂μ ⊗ₘ κ/∂ν ⊗ₘ η) p = (∂μ/∂ν) p.1 * (∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p
⊢ ((∂μ/∂ν) p.1).toReal * ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p).toReal * log (((∂μ/∂ν) p.1).toReal * ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p).toReal) =
    ((∂μ/∂ν) p.1).toReal * ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p).toReal * (log ((∂μ/∂ν) p.1).toReal + log ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p).toReal)
Module: Mathlib.InformationTheory.KullbackLeibler.ChainRule

Goal state before:
pp: case pos
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
κ η : Kernel 𝓧 𝓨
inst✝³ : IsFiniteMeasure μ
inst✝² : IsFiniteMeasure ν
inst✝¹ : IsMarkovKernel κ
inst✝ : IsMarkovKernel η
h_ac : μ ⊗ₘ κ ≪ μ ⊗ₘ η
p : 𝓧 × 𝓨
hp : (∂μ ⊗ₘ κ/∂ν ⊗ₘ η) p = (∂μ/∂ν) p.1 * (∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p
h_zero1 : ¬((∂μ/∂ν) p.1).toReal = 0
h_zero2 : ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p).toReal = 0
⊢ ((∂μ/∂ν) p.1).toReal * ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p).toReal * log (((∂μ/∂ν) p.1).toReal * ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p).toReal) =
    ((∂μ/∂ν) p.1).toReal * ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p).toReal * (log ((∂μ/∂ν) p.1).toReal + log ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p).toReal)

pp: case neg
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
κ η : Kernel 𝓧 𝓨
inst✝³ : IsFiniteMeasure μ
inst✝² : IsFiniteMeasure ν
inst✝¹ : IsMarkovKernel κ
inst✝ : IsMarkovKernel η
h_ac : μ ⊗ₘ κ ≪ μ ⊗ₘ η
p : 𝓧 × 𝓨
hp : (∂μ ⊗ₘ κ/∂ν ⊗ₘ η) p = (∂μ/∂ν) p.1 * (∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p
h_zero1 : ¬((∂μ/∂ν) p.1).toReal = 0
h_zero2 : ¬((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p).toReal = 0
⊢ ((∂μ/∂ν) p.1).toReal * ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p).toReal * log (((∂μ/∂ν) p.1).toReal * ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p).toReal) =
    ((∂μ/∂ν) p.1).toReal * ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p).toReal * (log ((∂μ/∂ν) p.1).toReal + log ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p).toReal)

Tactic:
· simp [h_zero2]

Goal state after:
case neg
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
κ η : Kernel 𝓧 𝓨
inst✝³ : IsFiniteMeasure μ
inst✝² : IsFiniteMeasure ν
inst✝¹ : IsMarkovKernel κ
inst✝ : IsMarkovKernel η
h_ac : μ ⊗ₘ κ ≪ μ ⊗ₘ η
p : 𝓧 × 𝓨
hp : (∂μ ⊗ₘ κ/∂ν ⊗ₘ η) p = (∂μ/∂ν) p.1 * (∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p
h_zero1 : ¬((∂μ/∂ν) p.1).toReal = 0
h_zero2 : ¬((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p).toReal = 0
⊢ ((∂μ/∂ν) p.1).toReal * ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p).toReal * log (((∂μ/∂ν) p.1).toReal * ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p).toReal) =
    ((∂μ/∂ν) p.1).toReal * ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p).toReal * (log ((∂μ/∂ν) p.1).toReal + log ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p).toReal)
Module: Mathlib.InformationTheory.KullbackLeibler.ChainRule

Goal state before:
pp: 𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
κ η : Kernel 𝓧 𝓨
inst✝³ : IsFiniteMeasure μ
inst✝² : IsFiniteMeasure ν
inst✝¹ : IsMarkovKernel κ
inst✝ : IsMarkovKernel η
h_ac : μ ⊗ₘ κ ≪ ν ⊗ₘ η
h_ac_μν : μ ≪ ν
h_ac_κη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
h_iff_κ : Integrable (llr μ ν) μ ↔ Integrable (fun x ↦ llr μ ν x.1) (μ ⊗ₘ κ)
h_int : Integrable (fun x ↦ log ((∂μ/∂ν) x.1).toReal + log ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) x).toReal) (μ ⊗ₘ κ)
h_int_iff :
  Integrable (llr (μ ⊗ₘ κ) (ν ⊗ₘ η)) (μ ⊗ₘ κ) ↔
    Integrable (fun x ↦ log ((∂μ/∂ν) x.1).toReal + log ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) x).toReal) (μ ⊗ₘ κ)
h_int1 : Integrable (llr μ ν) μ
⊢ Integrable (fun x ↦ llr μ ν x.1) (μ ⊗ₘ κ) ∧ Integrable (llr (μ ⊗ₘ κ) (μ ⊗ₘ η)) (μ ⊗ₘ κ)

Tactic:
rw [h_iff_κ] at h_int1

Goal state after:
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
κ η : Kernel 𝓧 𝓨
inst✝³ : IsFiniteMeasure μ
inst✝² : IsFiniteMeasure ν
inst✝¹ : IsMarkovKernel κ
inst✝ : IsMarkovKernel η
h_ac : μ ⊗ₘ κ ≪ ν ⊗ₘ η
h_ac_μν : μ ≪ ν
h_ac_κη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
h_iff_κ : Integrable (llr μ ν) μ ↔ Integrable (fun x ↦ llr μ ν x.1) (μ ⊗ₘ κ)
h_int : Integrable (fun x ↦ log ((∂μ/∂ν) x.1).toReal + log ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) x).toReal) (μ ⊗ₘ κ)
h_int_iff :
  Integrable (llr (μ ⊗ₘ κ) (ν ⊗ₘ η)) (μ ⊗ₘ κ) ↔
    Integrable (fun x ↦ log ((∂μ/∂ν) x.1).toReal + log ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) x).toReal) (μ ⊗ₘ κ)
h_int1 : Integrable (fun x ↦ llr μ ν x.1) (μ ⊗ₘ κ)
⊢ Integrable (fun x ↦ llr μ ν x.1) (μ ⊗ₘ κ) ∧ Integrable (llr (μ ⊗ₘ κ) (μ ⊗ₘ η)) (μ ⊗ₘ κ)
Module: Mathlib.InformationTheory.KullbackLeibler.ChainRule

Goal state before:
pp: case neg.inl
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
κ η : Kernel 𝓧 𝓨
inst✝³ : IsFiniteMeasure μ
inst✝² : IsFiniteMeasure ν
inst✝¹ : IsMarkovKernel κ
inst✝ : IsMarkovKernel η
h : ¬μ ≪ ν
⊢ ∞ = klDiv μ ν + klDiv (μ ⊗ₘ κ) (μ ⊗ₘ η)

Tactic:
| inl h =>

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

Goal state before:
pp: case neg.inl
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
κ η : Kernel 𝓧 𝓨
inst✝³ : IsFiniteMeasure μ
inst✝² : IsFiniteMeasure ν
inst✝¹ : IsMarkovKernel κ
inst✝ : IsMarkovKernel η
h_ac : μ ⊗ₘ κ ≪ ν ⊗ₘ η
h : ¬Integrable (llr μ ν) μ
⊢ ∞ = klDiv μ ν + klDiv (μ ⊗ₘ κ) (μ ⊗ₘ η)

Tactic:
| inl h =>

Goal state after:
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic

Goal state before:
pp: case pos
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : CompleteSpace E
F : Type u_5
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
inst✝ : NormedSpace ℝ F
hf_int : Integrable f μ
T : E →L[ℝ] F
hm : m ≤ m₀
hμ : SigmaFinite (μ.trim hm)
⊢ ⇑T ∘ μ[f | m] =ᵐ[μ] μ[⇑T ∘ f | m]

Tactic:
refine ae_eq_condExp_of_forall_setIntegral_eq hm ?_ (fun s ms hs => ?_) (fun s ms hs => ?_) ?_

Goal state after:
case pos.refine_1
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : CompleteSpace E
F : Type u_5
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
inst✝ : NormedSpace ℝ F
hf_int : Integrable f μ
T : E →L[ℝ] F
hm : m ≤ m₀
hμ : SigmaFinite (μ.trim hm)
⊢ Integrable (⇑T ∘ f) μ

case pos.refine_2
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : CompleteSpace E
F : Type u_5
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
inst✝ : NormedSpace ℝ F
hf_int : Integrable f μ
T : E →L[ℝ] F
hm : m ≤ m₀
hμ : SigmaFinite (μ.trim hm)
s : Set α
ms : MeasurableSet s
hs : μ s < ∞
⊢ IntegrableOn (⇑T ∘ μ[f | m]) s μ

case pos.refine_3
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : CompleteSpace E
F : Type u_5
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
inst✝ : NormedSpace ℝ F
hf_int : Integrable f μ
T : E →L[ℝ] F
hm : m ≤ m₀
hμ : SigmaFinite (μ.trim hm)
s : Set α
ms : MeasurableSet s
hs : μ s < ∞
⊢ ∫ (x : α) in s, (⇑T ∘ μ[f | m]) x ∂μ = ∫ (x : α) in s, (⇑T ∘ f) x ∂μ

case pos.refine_4
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : CompleteSpace E
F : Type u_5
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
inst✝ : NormedSpace ℝ F
hf_int : Integrable f μ
T : E →L[ℝ] F
hm : m ≤ m₀
hμ : SigmaFinite (μ.trim hm)
⊢ AEStronglyMeasurable (⇑T ∘ μ[f | m]) μ
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator

Goal state before:
pp: α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hf_int : Integrable f μ
hs : MeasurableSet s
hm : m ≤ m0
hμm this✝ : SigmaFinite (μ.trim hm)
this : s.indicator μ[f | m] =ᵐ[μ] s.indicator μ[s.indicator f + sᶜ.indicator f | m]
⊢ s.indicator μ[s.indicator f | m] =ᵐ[μ] μ[s.indicator f | m]

Tactic:
refine (condExp_indicator_aux hs ?_).symm.trans ?_
      · exact indicator_ae_eq_restrict_compl (hm _ hs)
      · rw [Set.indicator_indicator, Set.inter_self]

Goal state after:
Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation

Goal state before:
pp: Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
hm : mΩ ≤ mΩ₀
P : Measure Ω
hσ : SigmaFinite (P.trim hm)
X : Ω → ℝ≥0∞
s : Set Ω
hs : MeasurableSet s
hX : ¬Measurable X
h : (P.withDensity X).trim hm ≪ P.trim hm
this : SFinite ((P.withDensity X).trim hm)
⊢ Measurable (s.indicator (∂(P.withDensity X).trim hm/∂P.trim hm))

Tactic:
by measurability

Goal state after:
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.RadonNikodym

Goal state before:
pp: 𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
inst✝ : IsFiniteMeasure μ
hμν : μ ≪ ν
g : 𝓧 → 𝓨
hg : Measurable g
hσ : SigmaFinite (Measure.map g ν)
⊢ (fun a ↦ (Measure.map g μ).rnDeriv (Measure.map g ν) (g a)) =ᵐ[ν] ν⁻[μ.rnDeriv ν | MeasurableSpace.comap g m𝓨]

Tactic:
by
  have : SigmaFinite ν := SigmaFinite.of_map _ hg.aemeasurable hσ
  have h_ne_top1 : ∀ᵐ x ∂ν, (μ.map g).rnDeriv (ν.map g) (g x) ≠ ∞ :=
    ae_of_ae_map hg.aemeasurable (Measure.rnDeriv_ne_top (μ.map g) (ν.map g))
  have h_ne_top2 : ∀ᵐ x ∂ν, ν⁻[μ.rnDeriv ν|MeasurableSpace.comap g m𝓨] x ≠ ∞ := by
    refine condLExp_ne_top ?_
    simp [Measure.lintegral_rnDeriv hμν]
  have h_condExp := toReal_condLExp (m𝓨.comap g) (f := μ.rnDeriv ν) (μ := ν) (by fun_prop) ?_
  swap; · simp [Measure.lintegral_rnDeriv hμν]
  filter_upwards [toReal_rnDeriv_map hμν hg, h_condExp, h_ne_top1, h_ne_top2]
    with x hx h_condExp h_ne_top1 h_ne_top2
  rwa [← h_condExp, ENNReal.toReal_eq_toReal_iff' h_ne_top1 h_ne_top2] at hx

Goal state after:
Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation

Goal state before:
pp: Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X Y : Ω → ℝ≥0∞
hX : AEMeasurable X P
hm : mΩ ≤ mΩ₀
hσ : SigmaFinite (P.trim hm)
s : Set Ω
hs : MeasurableSet s
⊢ Measurable P⁻[X | mΩ]

Tactic:
by measurability

Goal state after:
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.RadonNikodym

Goal state before:
pp: case hf
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
inst✝¹ : IsFiniteMeasure μ
hμν : μ ≪ ν
g : 𝓧 → 𝓨
hg : Measurable g
inst✝ : SigmaFinite (Measure.map g ν)
s : Set ℝ
hs : MeasurableSet s
⊢ g ⁻¹' (fun a ↦ ((Measure.map g μ).rnDeriv (Measure.map g ν) a).toReal) ⁻¹' s =
    (fun a ↦ ((Measure.map g μ).rnDeriv (Measure.map g ν) (g a)).toReal) ⁻¹' s

Tactic:
rw [← Set.preimage_comp]

Goal state after:
case hf
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
inst✝¹ : IsFiniteMeasure μ
hμν : μ ≪ ν
g : 𝓧 → 𝓨
hg : Measurable g
inst✝ : SigmaFinite (Measure.map g ν)
s : Set ℝ
hs : MeasurableSet s
⊢ (fun a ↦ ((Measure.map g μ).rnDeriv (Measure.map g ν) a).toReal) ∘ g ⁻¹' s =
    (fun a ↦ ((Measure.map g μ).rnDeriv (Measure.map g ν) (g a)).toReal) ⁻¹' s
Module: Mathlib.InformationTheory.KullbackLeibler.DataProcessing

Goal state before:
pp: case refine_4
𝓧 : Type u_1
m m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
f : ℝ → ℝ
hm : m ≤ m𝓧
hμν : μ ≪ ν
hf : StronglyMeasurable f
hf_cvx : ConvexOn ℝ (Ici 0) f
hf_cont_at : ContinuousWithinAt f (Ici 0) 0
h_int : Integrable (fun x ↦ f ((∂μ/∂ν) x).toReal) ν
hf_cont : ContinuousOn f (Ici 0)
c c' : ℝ
h : ∀ (x : ℝ), 0 ≤ x → c * x + c' ≤ f x
⊢ Integrable (fun x ↦ c * ((∂μ.trim hm/∂ν.trim hm) x).toReal + c') (ν.trim hm)

Tactic:
exact (Integrable.const_mul (by fun_prop) _).add (integrable_const _)

Goal state after:
Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation

Goal state before:
pp: Ω : Type u_1
mΩ₀ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_2
mΩ : MeasurableSpace Ω
inst✝ : Countable ι
X : ι → Ω → ℝ≥0∞
hX : ∀ (i : ι), AEMeasurable (X i) P
hm : mΩ ≤ mΩ₀
hσ : SigmaFinite (P.trim hm)
s : Set Ω
hs : MeasurableSet s
⊢ ∀ (i : ι), AEMeasurable P⁻[X i | mΩ] (P.restrict s)

Tactic:
by measurability

Goal state after:
Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation

Goal state before:
pp: Ω : Type u_1
mΩ₀ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_2
mΩ : MeasurableSpace Ω
inst✝ : Countable ι
X : ι → Ω → ℝ≥0∞
hX : ∀ (i : ι), AEMeasurable (X i) P
hm : mΩ ≤ mΩ₀
hσ : SigmaFinite (P.trim hm)
s : Set Ω
hs : MeasurableSet s
⊢ ∀ (i : ι), AEMeasurable (X i) (P.restrict s)

Tactic:
by measurability

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.Matrix

Goal state before:
pp: ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst✝⁷ : AddCommGroup V
inst✝⁶ : AffineSpace V P
inst✝⁵ : Ring k
inst✝⁴ : Module k V
b : AffineBasis ι k P
ι' : Type u_1
inst✝³ : Finite ι
inst✝² : Fintype ι'
inst✝¹ : DecidableEq ι
inst✝ : Nontrivial k
p : ι' → P
A : Matrix ι ι' k
hA : A * b.toMatrix p = 1
val✝ : Fintype ι
i : ι
hAi : ∑ j, A i j = 1
⊢ b i = (Finset.affineCombination k Finset.univ p) (A i)

Tactic:
apply b.ext_elem

Goal state after:
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst✝⁷ : AddCommGroup V
inst✝⁶ : AffineSpace V P
inst✝⁵ : Ring k
inst✝⁴ : Module k V
b : AffineBasis ι k P
ι' : Type u_1
inst✝³ : Finite ι
inst✝² : Fintype ι'
inst✝¹ : DecidableEq ι
inst✝ : Nontrivial k
p : ι' → P
A : Matrix ι ι' k
hA : A * b.toMatrix p = 1
val✝ : Fintype ι
i : ι
hAi : ∑ j, A i j = 1
⊢ ∀ (i_1 : ι), (b.coord i_1) (b i) = (b.coord i_1) ((Finset.affineCombination k Finset.univ p) (A i))