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

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : β → E
hf : StronglyMeasurable f
hE : CompleteSpace E
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
this : TopologicalSpace.SeparableSpace ↑(range f ∪ {0})
s : ℕ → SimpleFunc β E := SimpleFunc.approxOn f ⋯ (range f ∪ {0}) 0 ⋯
⊢ StronglyMeasurable fun x ↦ ∫ (y : β), f y ∂κ x

Tactic:
let f' n : α → E := {x | Integrable f (κ x)}.indicator fun x ↦ (s n).integral (κ x)

Goal state after:
case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : β → E
hf : StronglyMeasurable f
hE : CompleteSpace E
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
this : TopologicalSpace.SeparableSpace ↑(range f ∪ {0})
s : ℕ → SimpleFunc β E := SimpleFunc.approxOn f ⋯ (range f ∪ {0}) 0 ⋯
f' : ℕ → α → E := fun n ↦ {x | Integrable f (κ x)}.indicator fun x ↦ SimpleFunc.integral (κ x) (s n)
⊢ StronglyMeasurable fun x ↦ ∫ (y : β), f y ∂κ x
Module: Mathlib.Probability.Kernel.Composition.RadonNikodym

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
hμν : μ ≪ ν
κ : Kernel α β
inst✝² : IsFiniteMeasure μ
inst✝¹ : IsFiniteMeasure ν
inst✝ : IsFiniteKernel κ
s : Set (α × β)
hs : MeasurableSet s
x✝ : (ν ⊗ₘ κ) s < ∞
t₁ : Set α
t₂ : Set β
ht₁ : MeasurableSet t₁
⊢ MeasurableSet t₂ →
    ∫⁻ (x : α × β) in t₁ ×ˢ t₂, (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ κ) x ∂ν ⊗ₘ κ =
      ∫⁻ (x : α × β) in t₁ ×ˢ t₂, μ.rnDeriv ν x.1 ∂ν ⊗ₘ κ

Tactic:
ht₂

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
hμν : μ ≪ ν
κ : Kernel α β
inst✝² : IsFiniteMeasure μ
inst✝¹ : IsFiniteMeasure ν
inst✝ : IsFiniteKernel κ
s : Set (α × β)
hs : MeasurableSet s
x✝ : (ν ⊗ₘ κ) s < ∞
t₁ : Set α
t₂ : Set β
ht₁ : MeasurableSet t₁
ht₂ : MeasurableSet t₂
⊢ ∫⁻ (x : α × β) in t₁ ×ˢ t₂, (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ κ) x ∂ν ⊗ₘ κ = ∫⁻ (x : α × β) in t₁ ×ˢ t₂, μ.rnDeriv ν x.1 ∂ν ⊗ₘ κ
Module: Mathlib.Probability.Kernel.MeasurableIntegral

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : IsSFiniteKernel κ
inst✝ : NormedSpace ℝ E
f : α → β → E
hf : StronglyMeasurable (uncurry f)
hE : CompleteSpace E
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
this : TopologicalSpace.SeparableSpace ↑(range (uncurry f) ∪ {0})
s : ℕ → SimpleFunc (α × β) E := SimpleFunc.approxOn (uncurry f) ⋯ (range (uncurry f) ∪ {0}) 0 ⋯
s' : ℕ → α → SimpleFunc β E := fun n x ↦ (s n).comp (Prod.mk x) ⋯
⊢ StronglyMeasurable fun x ↦ ∫ (y : β), f x y ∂κ x

Tactic:
let f' : ℕ → α → E := fun n =>
    {x | Integrable (f x) (κ x)}.indicator fun x => (s' n x).integral (κ x)

Goal state after:
case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : IsSFiniteKernel κ
inst✝ : NormedSpace ℝ E
f : α → β → E
hf : StronglyMeasurable (uncurry f)
hE : CompleteSpace E
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
this : TopologicalSpace.SeparableSpace ↑(range (uncurry f) ∪ {0})
s : ℕ → SimpleFunc (α × β) E := SimpleFunc.approxOn (uncurry f) ⋯ (range (uncurry f) ∪ {0}) 0 ⋯
s' : ℕ → α → SimpleFunc β E := fun n x ↦ (s n).comp (Prod.mk x) ⋯
f' : ℕ → α → E := fun n ↦ {x | Integrable (f x) (κ x)}.indicator fun x ↦ SimpleFunc.integral (κ x) (s' n x)
⊢ StronglyMeasurable fun x ↦ ∫ (y : β), f x y ∂κ x
Module: Mathlib.Probability.Kernel.MeasurableIntegral

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : IsSFiniteKernel κ
inst✝ : NormedSpace ℝ E
f : α → β → E
hf : StronglyMeasurable (uncurry f)
hE : CompleteSpace E
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
this : TopologicalSpace.SeparableSpace ↑(range (uncurry f) ∪ {0})
s : ℕ → SimpleFunc (α × β) E := SimpleFunc.approxOn (uncurry f) ⋯ (range (uncurry f) ∪ {0}) 0 ⋯
s' : ℕ → α → SimpleFunc β E := fun n x ↦ (s n).comp (Prod.mk x) ⋯
f' : ℕ → α → E := fun n ↦ {x | Integrable (f x) (κ x)}.indicator fun x ↦ SimpleFunc.integral (κ x) (s' n x)
n : ℕ
⊢ ∀ (x : α), {x ∈ (s' n x).range | x ≠ 0} ⊆ (s n).range

Tactic:
intro

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : IsSFiniteKernel κ
inst✝ : NormedSpace ℝ E
f : α → β → E
hf : StronglyMeasurable (uncurry f)
hE : CompleteSpace E
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
this : TopologicalSpace.SeparableSpace ↑(range (uncurry f) ∪ {0})
s : ℕ → SimpleFunc (α × β) E := SimpleFunc.approxOn (uncurry f) ⋯ (range (uncurry f) ∪ {0}) 0 ⋯
s' : ℕ → α → SimpleFunc β E := fun n x ↦ (s n).comp (Prod.mk x) ⋯
f' : ℕ → α → E := fun n ↦ {x | Integrable (f x) (κ x)}.indicator fun x ↦ SimpleFunc.integral (κ x) (s' n x)
n : ℕ
x✝ : α
⊢ {x ∈ (s' n x✝).range | x ≠ 0} ⊆ (s n).range
Module: Mathlib.Probability.Kernel.Composition.RadonNikodym

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ η : Kernel α β
inst✝³ : IsFiniteMeasure μ
inst✝² : IsFiniteKernel κ
inst✝¹ : IsFiniteKernel η
h_ac : μ ⊗ₘ κ ≪ μ ⊗ₘ η
ν : Measure α
inst✝ : IsFiniteMeasure ν
p : α × β
hp : (μ ⊗ₘ η).rnDeriv (ν ⊗ₘ η) p = μ.rnDeriv ν p.1
⊢ (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) p * μ.rnDeriv ν p.1 = μ.rnDeriv ν p.1 * (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) p

Tactic:
mul_comm

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ η : Kernel α β
inst✝³ : IsFiniteMeasure μ
inst✝² : IsFiniteKernel κ
inst✝¹ : IsFiniteKernel η
h_ac : μ ⊗ₘ κ ≪ μ ⊗ₘ η
ν : Measure α
inst✝ : IsFiniteMeasure ν
p : α × β
hp : (μ ⊗ₘ η).rnDeriv (ν ⊗ₘ η) p = μ.rnDeriv ν p.1
⊢ μ.rnDeriv ν p.1 * (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) p = μ.rnDeriv ν p.1 * (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) p
Module: Mathlib.MeasureTheory.Measure.Tilted

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
⊢ μ.tilted f = μ.withDensity fun x ↦ ↑(NNReal.mk (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) ⋯)

Tactic:
by
  rw [Measure.tilted]
  congr with x
  rw [ENNReal.ofReal_eq_coe_nnreal]

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 α β
inst✝ : IsSFiniteKernel κ
η : Kernel (α × β) γ
⊢ κ ⊗ₖ η = Kernel.sum fun n ↦ κ.seq n ⊗ₖ η

Tactic:
by
  simp_rw [compProd_def]
  rw [← comp_sum_left, ← comp_sum_right, ← parallelComp_sum_right, kernel_sum_seq]

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 γ
s : Set (β × γ)
κ : Kernel α β
inst✝¹ : IsZeroOrMarkovKernel κ
η : Kernel (α × β) γ
inst✝ : IsZeroOrMarkovKernel η
⊢ IsZeroOrMarkovKernel
    (swap γ β ∘ₖ (η ∥ₖ Kernel.id) ∘ₖ deterministic ⇑MeasurableEquiv.prodAssoc.symm ⋯ ∘ₖ (Kernel.id ∥ₖ copy β) ∘ₖ
        (Kernel.id ∥ₖ κ) ∘ₖ
      copy α)

Tactic:
infer_instance

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

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel (α × β) γ
inst✝ : IsFiniteKernel η
a : α
hκ : ¬IsSFiniteKernel κ
⊢ ((κ ⊗ₖ η) a) Set.univ ≤ (κ a) Set.univ * η.bound

Tactic:
compProd_of_not_isSFiniteKernel_left _ _ hκ

Goal state after:
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel (α × β) γ
inst✝ : IsFiniteKernel η
a : α
hκ : ¬IsSFiniteKernel κ
⊢ (0 a) Set.univ ≤ (κ a) Set.univ * η.bound
Module: Mathlib.MeasureTheory.Measure.Tilted

Goal state before:
pp: case inl
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
hμ : μ = 0
⊢ IsZeroOrProbabilityMeasure 0

Tactic:
infer_instance

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

Goal state before:
pp: case pos
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
hμ : NeZero μ
hf : Integrable (fun x ↦ rexp (f x)) μ
this : IsProbabilityMeasure (μ.tilted f)
⊢ IsZeroOrProbabilityMeasure (μ.tilted f)

Tactic:
infer_instance

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

Goal state before:
pp: case neg
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
hμ : NeZero μ
hf : ¬Integrable (fun x ↦ rexp (f x)) μ
⊢ IsZeroOrProbabilityMeasure 0

Tactic:
infer_instance

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 γ
s : Set (β × γ)
κ : Kernel α β
inst✝¹ : IsFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsFiniteKernel η
⊢ IsFiniteKernel
    (swap γ β ∘ₖ (η ∥ₖ Kernel.id) ∘ₖ deterministic ⇑MeasurableEquiv.prodAssoc.symm ⋯ ∘ₖ (Kernel.id ∥ₖ copy β) ∘ₖ
        (Kernel.id ∥ₖ κ) ∘ₖ
      copy α)

Tactic:
infer_instance

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 γ
s : Set (β × γ)
κ : Kernel α β
η : Kernel (α × β) γ
⊢ IsSFiniteKernel
    (swap γ β ∘ₖ (η ∥ₖ Kernel.id) ∘ₖ deterministic ⇑MeasurableEquiv.prodAssoc.symm ⋯ ∘ₖ (Kernel.id ∥ₖ copy β) ∘ₖ
        (Kernel.id ∥ₖ κ) ∘ₖ
      copy α)

Tactic:
infer_instance

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 α β
η : Kernel (α × β) γ
ξ : Kernel (α × β × γ) δ
hκ : IsSFiniteKernel κ
hη : IsSFiniteKernel η
hξ : ¬IsSFiniteKernel ξ
h_sfin : IsSFiniteKernel (ξ.comap ⇑MeasurableEquiv.prodAssoc ⋯)
this : ξ = (ξ.comap ⇑MeasurableEquiv.prodAssoc ⋯).comap ⇑MeasurableEquiv.prodAssoc.symm ⋯
⊢ IsSFiniteKernel ((ξ.comap ⇑MeasurableEquiv.prodAssoc ⋯).comap ⇑MeasurableEquiv.prodAssoc.symm ⋯)

Tactic:
infer_instance

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
g : α → ℝ≥0∞
⊢ ∫⁻ (x : α) in Set.univ, ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) * g x ∂μ =
    ∫⁻ (x : α), ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) * g x ∂μ

Tactic:
setLIntegral_univ

Goal state after:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
g : α → ℝ≥0∞
⊢ ∫⁻ (x : α), ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) * g x ∂μ =
    ∫⁻ (x : α), ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) * g x ∂μ
Module: Mathlib.InformationTheory.KullbackLeibler.KLFun

Goal state before:
pp: ⊢ Tendsto (deriv klFun) (nhdsWithin 0 (Ioi 0)) atBot

Tactic:
deriv_klFun

Goal state after:
⊢ Tendsto log (nhdsWithin 0 (Ioi 0)) atBot
Module: Mathlib.InformationTheory.KullbackLeibler.KLFun

Goal state before:
pp: ⊢ Tendsto (deriv klFun) (nhdsWithin 0 (Iio 0)) atBot

Tactic:
deriv_klFun

Goal state after:
⊢ Tendsto log (nhdsWithin 0 (Iio 0)) atBot
Module: Mathlib.InformationTheory.KullbackLeibler.KLFun

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

Tactic:
convert! this using 3 with x

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

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

Tactic:
congr 2
    exact integral_rnDeriv_smul hμν

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

Goal state before:
pp: case inr.inr
α : 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
⊢ False

Tactic:
have : ‖indicatorConstLp p s_meas s_top.ne (1 : ℝ)‖ = ‖(0 : Lp ℝ p μ)‖ := by rw [hzero]

Goal state after:
case inr.inr
α : 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 : ‖indicatorConstLp p s_meas ⋯ 1‖ = ‖0‖
⊢ False
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Trim

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

Tactic:
by
  by_cases h0 : p = 0
  · simp [h0]
  by_cases h_top : p = ∞
  · simpa only [h_top, eLpNorm_exponent_top] using eLpNormEssSup_trim hm hf
  simpa only [eLpNorm_eq_eLpNorm' h0 h_top] using eLpNorm'_trim hm hf

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

Goal state before:
pp: α : Type u_1
E' : Type u_2
𝕜 : Type u_4
p : ℝ≥0∞
m m0 : MeasurableSpace α
μ : Measure α
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E'
inst✝² : InnerProductSpace 𝕜 E'
inst✝¹ : CompleteSpace E'
inst✝ : NormedSpace ℝ E'
hm : m ≤ m0
f g : ↥(Lp E' p μ)
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → IntegrableOn (↑↑f) s μ
hg_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → IntegrableOn (↑↑g) s μ
hfg : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → ∫ (x : α) in s, ↑↑f x ∂μ = ∫ (x : α) in s, ↑↑g x ∂μ
hf_meas : AEStronglyMeasurable (↑↑f) μ
hg_meas : AEStronglyMeasurable (↑↑g) μ
s : Set α
hs : MeasurableSet s
hμs : μ s < ∞
⊢ ∫ (x : α) in s, ↑↑(f - g) x ∂μ = 0

Tactic:
integral_congr_ae (ae_restrict_of_ae (Lp.coeFn_sub f g))

Goal state after:
α : Type u_1
E' : Type u_2
𝕜 : Type u_4
p : ℝ≥0∞
m m0 : MeasurableSpace α
μ : Measure α
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E'
inst✝² : InnerProductSpace 𝕜 E'
inst✝¹ : CompleteSpace E'
inst✝ : NormedSpace ℝ E'
hm : m ≤ m0
f g : ↥(Lp E' p μ)
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → IntegrableOn (↑↑f) s μ
hg_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → IntegrableOn (↑↑g) s μ
hfg : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → ∫ (x : α) in s, ↑↑f x ∂μ = ∫ (x : α) in s, ↑↑g x ∂μ
hf_meas : AEStronglyMeasurable (↑↑f) μ
hg_meas : AEStronglyMeasurable (↑↑g) μ
s : Set α
hs : MeasurableSet s
hμs : μ s < ∞
⊢ ∫ (a : α) in s, (↑↑f - ↑↑g) a ∂μ = 0
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 μ ν) μ
h_contra : Integrable (llr μ (c • ν)) μ
⊢ IsFiniteMeasure (c • ν)

Tactic:
infer_instance

Goal state after:
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:
by
  rw [← AddSubgroup.mem_carrier, lpMeasSubgroup, Set.mem_ofPred_eq]

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

Goal state before:
pp: α : Type u_1
F : Type u_2
𝕜 : Type u_3
p : ℝ≥0∞
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
m m0 : MeasurableSpace α
μ : Measure α
hm : Fact (m ≤ m0)
inst✝ : CompleteSpace F
hp : Fact (1 ≤ p)
⊢ CompleteSpace ↥(Lp F p (μ.trim ⋯))

Tactic:
infer_instance

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

Goal state before:
pp: α : Type u_1
F : Type u_2
𝕜 : Type u_3
p : ℝ≥0∞
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
m m0 : MeasurableSpace α
μ : Measure α
hm : Fact (m ≤ m0)
inst✝ : CompleteSpace F
hp : Fact (1 ≤ p)
⊢ CompleteSpace ↥(lpMeasSubgroup F m p μ)

Tactic:
infer_instance

Goal state after:
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 α
hp : Fact (1 ≤ p)
inst✝ : CompleteSpace F
hm : m ≤ m0
this : Fact (m ≤ m0)
⊢ CompleteSpace ↥(lpMeasSubgroup F m p μ)

Tactic:
infer_instance

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
ι : Type u_3
inst✝ : Countable ι
p : ℝ≥0∞
hp : 1 ≤ p
f : ι → X → E
hf : ∀ (n : ι), AEStronglyMeasurable (f n) μ
h'f : ∑' (n : ι), eLpNorm (f n) p μ ≠ ∞
h'p : p < ∞
s : Set X
hs : MeasurableSet s
h's : μ s ≠ ∞
⊢ ∫⁻ (x : X) in s, ∑' (i : ι), ‖f i x‖ₑ ∂μ ≠ ∞

Tactic:
rw [lintegral_tsum (fun i ↦ (hf i).restrict.enorm)]

Goal state after:
X : Type u_1
E : Type u_2
x✝ : MeasurableSpace X
μ : Measure X
inst✝¹ : NormedAddCommGroup E
ι : Type u_3
inst✝ : Countable ι
p : ℝ≥0∞
hp : 1 ≤ p
f : ι → X → E
hf : ∀ (n : ι), AEStronglyMeasurable (f n) μ
h'f : ∑' (n : ι), eLpNorm (f n) p μ ≠ ∞
h'p : p < ∞
s : Set X
hs : MeasurableSet s
h's : μ s ≠ ∞
⊢ ∑' (i : ι), ∫⁻ (a : X) in s, ‖f i a‖ₑ ∂μ ≠ ∞
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1

Goal state before:
pp: α : Type u_1
G : Type u_4
inst✝² : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedSpace ℝ G
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
x : G
⊢ ↑↑((condExpInd G hm μ ∅) x) =ᵐ[μ] ↑↑(0 x)

Tactic:
grw [condExpInd_ae_eq_condExpIndSMul hm MeasurableSet.empty (by simp), condExpIndSMul_empty,
    zero_apply, Lp.coeFn_zero, Lp.coeFn_zero]

Goal state after:
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 α
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 μ),
    StronglyMeasurable f →
      StronglyMeasurable 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 g : α → F
hf : MemLp f p μ
hg : MemLp g p μ
hfm : AEStronglyMeasurable f μ
hgm : AEStronglyMeasurable g μ
h_disj : Disjoint (Function.support f) (Function.support g)
hPf : P (MemLp.toLp f hf)
hPg : P (MemLp.toLp g hg)
s_f : Set α := Function.support (AEStronglyMeasurable.mk f hfm)
hs_f : MeasurableSet s_f
hs_f_eq : s_f =ᵐ[μ] Function.support f
s_g : Set α := Function.support (AEStronglyMeasurable.mk g hgm)
hs_g : MeasurableSet s_g
hs_g_eq : s_g =ᵐ[μ] Function.support g
h_inter_empty : s_f ∩ s_g =ᵐ[μ] ∅
f' : α → F := (s_f \ s_g).indicator (AEStronglyMeasurable.mk f hfm)
this : s_f \ s_g =ᵐ[μ] s_f
⊢ s_f.indicator (AEStronglyMeasurable.mk f hfm) =ᵐ[μ] f

Tactic:
rw [Set.indicator_support]

Goal state after:
α : 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 μ),
    StronglyMeasurable f →
      StronglyMeasurable 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 g : α → F
hf : MemLp f p μ
hg : MemLp g p μ
hfm : AEStronglyMeasurable f μ
hgm : AEStronglyMeasurable g μ
h_disj : Disjoint (Function.support f) (Function.support g)
hPf : P (MemLp.toLp f hf)
hPg : P (MemLp.toLp g hg)
s_f : Set α := Function.support (AEStronglyMeasurable.mk f hfm)
hs_f : MeasurableSet s_f
hs_f_eq : s_f =ᵐ[μ] Function.support f
s_g : Set α := Function.support (AEStronglyMeasurable.mk g hgm)
hs_g : MeasurableSet s_g
hs_g_eq : s_g =ᵐ[μ] Function.support g
h_inter_empty : s_f ∩ s_g =ᵐ[μ] ∅
f' : α → F := (s_f \ s_g).indicator (AEStronglyMeasurable.mk f hfm)
this : s_f \ s_g =ᵐ[μ] s_f
⊢ AEStronglyMeasurable.mk f hfm =ᵐ[μ] f