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 α β
inst✝² : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel η
inst✝ : NormedSpace ℝ E
f✝ : β × γ → E
hE : CompleteSpace E
f g : β × γ → E
a✝ : Disjoint (support f) (support g)
i_f : Integrable f ((κ ⊗ₖ η) a)
i_g : Integrable g ((κ ⊗ₖ η) a)
hf : ∫ (z : β × γ), f z ∂(κ ⊗ₖ η) a = ∫ (x : β), ∫ (y : γ), f (x, y) ∂η (a, x) ∂κ a
hg : ∫ (z : β × γ), g z ∂(κ ⊗ₖ η) a = ∫ (x : β), ∫ (y : γ), g (x, y) ∂η (a, x) ∂κ a
⊢ ∫ (a : β × γ), f a ∂(κ ⊗ₖ η) a + ∫ (a : β × γ), g a ∂(κ ⊗ₖ η) a =
    ∫ (x : β), ∫ (y : γ), f (x, y) ∂η (a, x) ∂κ a + ∫ (x : β), ∫ (y : γ), g (x, y) ∂η (a, x) ∂κ a

Tactic:
hf,

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 α β
inst✝² : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel η
inst✝ : NormedSpace ℝ E
f✝ : β × γ → E
hE : CompleteSpace E
f g : β × γ → E
a✝ : Disjoint (support f) (support g)
i_f : Integrable f ((κ ⊗ₖ η) a)
i_g : Integrable g ((κ ⊗ₖ η) a)
hf : ∫ (z : β × γ), f z ∂(κ ⊗ₖ η) a = ∫ (x : β), ∫ (y : γ), f (x, y) ∂η (a, x) ∂κ a
hg : ∫ (z : β × γ), g z ∂(κ ⊗ₖ η) a = ∫ (x : β), ∫ (y : γ), g (x, y) ∂η (a, x) ∂κ a
⊢ ∫ (x : β), ∫ (y : γ), f (x, y) ∂η (a, x) ∂κ a + ∫ (a : β × γ), g a ∂(κ ⊗ₖ η) a =
    ∫ (x : β), ∫ (y : γ), f (x, y) ∂η (a, x) ∂κ a + ∫ (x : β), ∫ (y : γ), g (x, y) ∂η (a, x) ∂κ a
Module: Mathlib.MeasureTheory.Measure.Tilted

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ
hs : MeasurableSet s
hf : Integrable (fun x ↦ rexp (f x)) μ
x✝ : α
⊢ 0 x✝ ≤ (fun a ↦ rexp (f a) / ∫ (x : α), rexp (f x) ∂μ) x✝

Tactic:
by positivity

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
f : α → ℝ
s : Set α
hf : Integrable (fun x ↦ rexp (f x)) μ
x✝ : α
⊢ 0 x✝ ≤ (fun a ↦ rexp (f a) / ∫ (x : α), rexp (f x) ∂μ) x✝

Tactic:
by positivity

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 γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
f : δ → γ
hf : MeasurableEmbedding f
⊢ (κ ⊗ₖ η).comapRight ⋯ = κ ⊗ₖ η.comapRight hf

Tactic:
ext a t ht
  rw [comapRight_apply' _ _ _ ht, compProd_apply, compProd_apply ht]
  · refine lintegral_congr fun b ↦ ?_
    rw [comapRight_apply']
    · congr with x
      grind
    · exact measurable_prodMk_left ht
  · exact (MeasurableEmbedding.id.prodMap hf).measurableSet_image.mpr ht

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable (fun x ↦ rexp (f x)) μ
g : α → ℝ
h0 : NeZero μ
s : Set α
hs : MeasurableSet s
x : α
⊢ 0 ≤ rexp (f x) / ∫ (x : α), rexp (f x) ∂μ

Tactic:
by positivity

Goal state after:
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
i_f : Integrable f ((η ∘ₖ κ) a)
i_g : Integrable g ((η ∘ₖ κ) a)
hf : ∫ (z : γ), f z ∂(η ∘ₖ κ) a = ∫ (x : β), ∫ (y : γ), f y ∂η x ∂κ a
hg : ∫ (z : γ), g z ∂(η ∘ₖ κ) a = ∫ (x : β), ∫ (y : γ), g y ∂η x ∂κ a
⊢ ∫ (a : γ), f a ∂(η ∘ₖ κ) a + ∫ (a : γ), g a ∂(η ∘ₖ κ) a =
    ∫ (x : β), ∫ (a : γ), f a ∂η x ∂κ a + ∫ (x : β), ∫ (a : γ), g a ∂η x ∂κ a

Tactic:
hf,

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
i_f : Integrable f ((η ∘ₖ κ) a)
i_g : Integrable g ((η ∘ₖ κ) a)
hf : ∫ (z : γ), f z ∂(η ∘ₖ κ) a = ∫ (x : β), ∫ (y : γ), f y ∂η x ∂κ a
hg : ∫ (z : γ), g z ∂(η ∘ₖ κ) a = ∫ (x : β), ∫ (y : γ), g y ∂η x ∂κ a
⊢ ∫ (x : β), ∫ (a : γ), f a ∂η x ∂κ a + ∫ (a : γ), g a ∂(η ∘ₖ κ) a =
    ∫ (x : β), ∫ (a : γ), f a ∂η x ∂κ a + ∫ (x : β), ∫ (a : γ), g a ∂η 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)) ν
x : α
hx : μ.rnDeriv (ν.tilted f) x = ENNReal.ofReal (rexp (-f x) * ∫ (x : α), rexp (f x) ∂ν) * μ.rnDeriv ν x
⊢ 0 ≤ rexp (-f x) * ∫ (x : α), rexp (f x) ∂ν

Tactic:
by positivity

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

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

Tactic:
by positivity

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:
rw [integrable_congr (llr_tilted_left hμν hfμ hfν)]
  exact Integrable.add (hf.sub (integrable_const _)) h_int

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 positivity

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
h : ¬μ ≪ ν
⊢ (if μ ≪ ν ∧ Integrable (llr μ ν) μ then ENNReal.ofReal (∫ (x : α), llr μ ν x ∂μ + ν.real univ - μ.real univ) else ∞) =
    ∞

Tactic:
exact if_neg (not_and_of_not_left _ h)

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 positivity

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:
hf,

Goal state after:
α : 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
⊢ 0 =ᵐ[μ] ↑↑0
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
hfne : ¬↑↑f =ᵐ[μ] 0
h'p : p < ∞
hp : p ≠ 0
h'f : AEFinStronglyMeasurable (↑↑f) μ
s : Set α
s_meas : MeasurableSet s
s_pos : 0 < μ s
s_top : μ s < ∞
hzero : indicatorConstLp p s_meas ⋯ 1 = 0
this : μ.real s ^ p.toReal⁻¹ = 0
⊢ 0 ≤ μ.real s

Tactic:
by positivity

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 μ ν) μ
⊢ (klDiv μ ν).toReal = ∫ (a : α), llr μ ν a ∂μ + ν.real univ - μ.real univ

Tactic:
rw [klDiv_of_ac_of_integrable h h_int, ENNReal.toReal_ofReal]

Goal state after:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
h : μ ≪ ν
h_int : Integrable (llr μ ν) μ
⊢ 0 ≤ ∫ (x : α), llr μ ν x ∂μ + ν.real univ - μ.real univ
Module: Mathlib.InformationTheory.KullbackLeibler.Basic

Goal state before:
pp: case neg
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
c : ℝ≥0
hc : ¬c = 0
h_llr : llr (c • μ) ν =ᵐ[μ] fun x ↦ llr μ ν x + log ↑c
⊢ Integrable (llr (c • μ) ν) (c • μ)

Tactic:
refine Integrable.smul_measure_nnreal ?_

Goal state after:
case neg
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
c : ℝ≥0
hc : ¬c = 0
h_llr : llr (c • μ) ν =ᵐ[μ] fun x ↦ llr μ ν x + log ↑c
⊢ Integrable (llr (c • μ) ν) μ
Module: Mathlib.InformationTheory.KullbackLeibler.Basic

Goal state before:
pp: case neg.h_int
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
c : ℝ≥0
hc : ¬c = 0
h_llr_left : llr (c⁻¹ • μ) ν =ᵐ[μ] fun x ↦ llr μ ν x + log ↑c⁻¹
h_llr_right : llr μ (c • ν) =ᵐ[μ] fun x ↦ llr μ ν x - log ↑c
⊢ Integrable (llr (c⁻¹ • μ) ν) (c⁻¹ • μ)

Tactic:
refine Integrable.smul_measure_nnreal ?_

Goal state after:
case neg.h_int
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
c : ℝ≥0
hc : ¬c = 0
h_llr_left : llr (c⁻¹ • μ) ν =ᵐ[μ] fun x ↦ llr μ ν x + log ↑c⁻¹
h_llr_right : llr μ (c • ν) =ᵐ[μ] fun x ↦ llr μ ν x - log ↑c
⊢ Integrable (llr (c⁻¹ • μ) ν) μ
Module: Mathlib.InformationTheory.KullbackLeibler.Basic

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

Tactic:
refine Integrable.smul_measure_nnreal ?_

Goal state after:
case neg.h_int
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
c : ℝ≥0
hc : ¬c = 0
⊢ Integrable (llr (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⁻¹ • μ) ν) (c⁻¹ • μ)
⊢ Integrable (llr (c • c⁻¹ • μ) ν) (c • c⁻¹ • μ)

Tactic:
refine Integrable.smul_measure_nnreal ?_

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⁻¹ • μ) ν) (c⁻¹ • μ)
⊢ Integrable (llr (c • c⁻¹ • μ) ν) (c⁻¹ • μ)
Module: Mathlib.InformationTheory.KullbackLeibler.Basic

Goal state before:
pp: α : 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 μ ν) μ
⊢ Integrable (llr (c⁻¹ • μ) ν) (c⁻¹ • μ)

Tactic:
refine Integrable.smul_measure_nnreal ?_

Goal state after:
α : 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 μ ν) μ
⊢ Integrable (llr (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 : ∀ (μ : Measure α), μ = c⁻¹ • c • μ
hμν : ¬μ ≪ ν
⊢ klDiv (c • μ) (c • ν) = ↑c * klDiv μ ν

Tactic:
rw [klDiv_of_not_ac hμν, klDiv_of_not_ac, ENNReal.mul_top hc']

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 : ∀ (μ : Measure α), μ = c⁻¹ • c • μ
hμν : ¬μ ≪ ν
⊢ ¬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 : ∀ (μ : Measure α), μ = c⁻¹ • c • μ
hμν : μ ≪ ν
h_int : ¬Integrable (llr μ ν) μ
h_contra : Integrable (llr (c • μ) (c • ν)) (c • μ)
⊢ Integrable (llr (c⁻¹ • c • μ) (c⁻¹ • c • ν)) (c⁻¹ • c • μ)

Tactic:
refine Integrable.smul_measure_nnreal ?_

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 : ∀ (μ : Measure α), μ = c⁻¹ • c • μ
hμν : μ ≪ ν
h_int : ¬Integrable (llr μ ν) μ
h_contra : Integrable (llr (c • μ) (c • ν)) (c • μ)
⊢ Integrable (llr (c⁻¹ • c • μ) (c⁻¹ • c • ν)) (c • μ)
Module: Mathlib.InformationTheory.KullbackLeibler.Basic

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

Tactic:
refine Integrable.smul_measure_nnreal ?_

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

Goal state before:
pp: case refine_2
α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst✝² : NormedAddCommGroup F
m m0 : MeasurableSpace α
μ : Measure α
inst✝¹ : Fact (1 ≤ p)
inst✝ : NormedSpace ℝ F
hm : m ≤ m0
hp_ne_top : p ≠ ∞
P : ↥(Lp F p μ) → Prop
h_ind : ∀ (c : F) {s : Set α} (hs : MeasurableSet s) (hμs : μ s < ∞), P ↑(simpleFunc.indicatorConst p ⋯ ⋯ c)
h_add :
  ∀ ⦃f g : α → F⦄ (hf : MemLp f p μ) (hg : MemLp g p μ),
    AEStronglyMeasurable f μ →
      AEStronglyMeasurable g μ →
        Disjoint (Function.support f) (Function.support g) →
          P (MemLp.toLp f hf) → P (MemLp.toLp g hg) → P (MemLp.toLp f hf + MemLp.toLp g hg)
h_closed : IsClosed {f | P ↑f}
f✝ : ↥(Lp F p μ)
hf✝ : AEStronglyMeasurable (↑↑f✝) μ
f' : ↥(lpMeas F ℝ m p μ) := ⟨f✝, hf✝⟩
g✝ : ↥(Lp F p (μ.trim hm)) := (lpMeasToLpTrimLie F ℝ p μ hm) f'
hfg : f' = (lpMeasToLpTrimLie F ℝ p μ hm).symm g✝
f g : α → F
hf : MemLp f p (μ.trim hm)
hg : MemLp g p (μ.trim hm)
h_disj : Disjoint (Function.support f) (Function.support g)
hfP : P (MemLp.toLp f ⋯)
hgP : P ↑((lpMeasToLpTrimLie F ℝ p μ hm).symm (MemLp.toLp g hg))
h_eq :
  ∀ (f : α → F) (hf : MemLp f p (μ.trim hm)), ↑((lpMeasToLpTrimLie F ℝ p μ hm).symm (MemLp.toLp f hf)) = MemLp.toLp f ⋯
⊢ P (MemLp.toLp f ⋯ + ↑((lpMeasToLpTrimLie F ℝ p μ hm).symm (MemLp.toLp g hg)))

Tactic:
h_eq g hg

Goal state after:
case refine_2
α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst✝² : NormedAddCommGroup F
m m0 : MeasurableSpace α
μ : Measure α
inst✝¹ : Fact (1 ≤ p)
inst✝ : NormedSpace ℝ F
hm : m ≤ m0
hp_ne_top : p ≠ ∞
P : ↥(Lp F p μ) → Prop
h_ind : ∀ (c : F) {s : Set α} (hs : MeasurableSet s) (hμs : μ s < ∞), P ↑(simpleFunc.indicatorConst p ⋯ ⋯ c)
h_add :
  ∀ ⦃f g : α → F⦄ (hf : MemLp f p μ) (hg : MemLp g p μ),
    AEStronglyMeasurable f μ →
      AEStronglyMeasurable g μ →
        Disjoint (Function.support f) (Function.support g) →
          P (MemLp.toLp f hf) → P (MemLp.toLp g hg) → P (MemLp.toLp f hf + MemLp.toLp g hg)
h_closed : IsClosed {f | P ↑f}
f✝ : ↥(Lp F p μ)
hf✝ : AEStronglyMeasurable (↑↑f✝) μ
f' : ↥(lpMeas F ℝ m p μ) := ⟨f✝, hf✝⟩
g✝ : ↥(Lp F p (μ.trim hm)) := (lpMeasToLpTrimLie F ℝ p μ hm) f'
hfg : f' = (lpMeasToLpTrimLie F ℝ p μ hm).symm g✝
f g : α → F
hf : MemLp f p (μ.trim hm)
hg : MemLp g p (μ.trim hm)
h_disj : Disjoint (Function.support f) (Function.support g)
hfP : P (MemLp.toLp f ⋯)
hgP : P (MemLp.toLp g ⋯)
h_eq :
  ∀ (f : α → F) (hf : MemLp f p (μ.trim hm)), ↑((lpMeasToLpTrimLie F ℝ p μ hm).symm (MemLp.toLp f hf)) = MemLp.toLp f ⋯
⊢ P (MemLp.toLp f ⋯ + MemLp.toLp g ⋯)
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1

Goal state before:
pp: case refine_1
α : 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 ≠ ∞
⊢ ∀ (c : F') {s_1 : Set α} (hs : MeasurableSet s_1) (hμs : μ s_1 < ∞),
    ∫ (x : α) in s, ↑↑((condExpL1CLM F' hm μ) ↑(simpleFunc.indicatorConst 1 hs ⋯ c)) x ∂μ =
      ∫ (x : α) in s, ↑↑↑(simpleFunc.indicatorConst 1 hs ⋯ c) x ∂μ

Tactic:
intro x t ht hμt
    simp_rw [condExpL1CLM_indicatorConst ht hμt.ne x]
    rw [Lp.simpleFunc.coe_indicatorConst, setIntegral_indicatorConstLp (hm _ hs)]
    exact setIntegral_condExpInd hs ht hμs hμt.ne x

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

Goal state before:
pp: X : Type u_1
E : Type u_2
x✝ : MeasurableSpace X
μ : Measure X
inst✝¹ : NormedAddCommGroup E
p : ℝ≥0∞
hp : Fact (1 ≤ p)
inst✝ : CompleteSpace E
f : ℕ → ↥(Lp E p μ)
hf : ∑' (n : ℕ), ‖f n‖ₑ ≠ ∞
A : ∀ᵐ (a : X) ∂μ, Summable fun n ↦ ‖↑↑(f n) a‖
⊢ ∀ᵐ (a : X) ∂μ, HasSum (fun n ↦ ↑↑(f n) a) (↑↑(∑' (n : ℕ), f n) a)

Tactic:
have B : ∀ᵐ x ∂μ, ∀ n, ⇑(∑ i ∈ range n, f i) x = ∑ i ∈ range n, f i x := by
    rw [ae_all_iff]
    exact fun i ↦ coeFn_fun_finsetSum _ _

Goal state after:
X : Type u_1
E : Type u_2
x✝ : MeasurableSpace X
μ : Measure X
inst✝¹ : NormedAddCommGroup E
p : ℝ≥0∞
hp : Fact (1 ≤ p)
inst✝ : CompleteSpace E
f : ℕ → ↥(Lp E p μ)
hf : ∑' (n : ℕ), ‖f n‖ₑ ≠ ∞
A : ∀ᵐ (a : X) ∂μ, Summable fun n ↦ ‖↑↑(f n) a‖
B : ∀ᵐ (x : X) ∂μ, ∀ (n : ℕ), ↑↑(∑ i ∈ range n, f i) x = ∑ i ∈ range n, ↑↑(f i) x
⊢ ∀ᵐ (a : X) ∂μ, HasSum (fun n ↦ ↑↑(f n) a) (↑↑(∑' (n : ℕ), f n) a)
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 ∂μ
⊢ ∫ (a : α) in s, ↑↑((condExpL1CLM F' hm μ) (MemLp.toLp f hf_Lp)) a ∂μ +
      ∫ (a : α) in s, ↑↑((condExpL1CLM F' hm μ) (MemLp.toLp g hg_Lp)) a ∂μ =
    ∫ (a : α) in s, ↑↑(MemLp.toLp f hf_Lp) a ∂μ + ∫ (a : α) in s, ↑↑(MemLp.toLp g hg_Lp) a ∂μ

Tactic:
hf,

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, ↑↑(MemLp.toLp f hf_Lp) x ∂μ + ∫ (a : α) in s, ↑↑((condExpL1CLM F' hm μ) (MemLp.toLp g hg_Lp)) a ∂μ =
    ∫ (a : α) in s, ↑↑(MemLp.toLp f hf_Lp) a ∂μ + ∫ (a : α) in s, ↑↑(MemLp.toLp g hg_Lp) a ∂μ
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_int : Integrable (fun a ↦ ((∂μ/∂ν) a).toReal * log ((∂μ/∂ν) a).toReal) ν
⊢ Integrable (llr μ ν) μ

Tactic:
exact (integrable_rnDeriv_mul_log_iff hμν_ac).mp h_int

Goal state after:
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 : μ ⊗ₘ κ ≪ ν ⊗ₘ η
h_int : Integrable (llr (μ ⊗ₘ κ) (ν ⊗ₘ η)) (μ ⊗ₘ κ)
h_ac_μν : μ ≪ ν
h_ac_κη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
h_int_μν : Integrable (llr μ ν) μ
h_int_κη : Integrable (llr (μ ⊗ₘ κ) (μ ⊗ₘ η)) (μ ⊗ₘ κ)
⊢ klDiv (μ ⊗ₘ κ) (ν ⊗ₘ η) = klDiv μ ν + klDiv (μ ⊗ₘ κ) (μ ⊗ₘ η)

Tactic:
klDiv_of_ac_of_integrable h_ac h_int,

Goal state after:
case pos
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
κ η : Kernel 𝓧 𝓨
inst✝³ : IsFiniteMeasure μ
inst✝² : IsFiniteMeasure ν
inst✝¹ : IsMarkovKernel κ
inst✝ : IsMarkovKernel η
h_ac : μ ⊗ₘ κ ≪ ν ⊗ₘ η
h_int : Integrable (llr (μ ⊗ₘ κ) (ν ⊗ₘ η)) (μ ⊗ₘ κ)
h_ac_μν : μ ≪ ν
h_ac_κη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
h_int_μν : Integrable (llr μ ν) μ
h_int_κη : Integrable (llr (μ ⊗ₘ κ) (μ ⊗ₘ η)) (μ ⊗ₘ κ)
⊢ ENNReal.ofReal (∫ (x : 𝓧 × 𝓨), llr (μ ⊗ₘ κ) (ν ⊗ₘ η) x ∂μ ⊗ₘ κ + (ν ⊗ₘ η).real univ - (μ ⊗ₘ κ).real univ) =
    klDiv μ ν + klDiv (μ ⊗ₘ κ) (μ ⊗ₘ η)
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator

Goal state before:
pp: case refine_1
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
hs_m : MeasurableSet s
hf_int : Integrable f μ
this : SigmaFinite ((μ.restrict s).trim hm)
t : Set α
ht : MeasurableSet t
a✝ : μ t < ∞
⊢ IntegrableOn (s.indicator (μ.restrict s)[f | m]) t μ

Tactic:
rw [← integrable_indicator_iff (hm _ ht), Set.indicator_indicator, Set.inter_comm, ←
      Set.indicator_indicator]

Goal state after:
case refine_1
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
hs_m : MeasurableSet s
hf_int : Integrable f μ
this : SigmaFinite ((μ.restrict s).trim hm)
t : Set α
ht : MeasurableSet t
a✝ : μ t < ∞
⊢ Integrable (s.indicator (t.indicator (μ.restrict s)[f | m])) μ