awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
Goal:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
F : Type u_5
inst_3 : NormedAddCommGroup F
inst_4 : CompleteSpace F
inst_5 : NormedSpace ℝ F
inst_6 : IsFiniteMeasure μ
hm : m ≤ m₀
hf_int : Integrable f μ
T : E →L[ℝ] F
a : F
hp :
  (fun (x : α) ↦ HAdd.hAdd (α := F) ((T : (a : E) → F) (μ[f | m] x) : F) a) =ᶠ[ae μ]
    HAdd.hAdd (α := α → F) μ[(⇑T : (a : E) → F) ∘ f | m] μ[fun (y : α) ↦ a | m]
⊢ EventuallyEq.{u_1, u_5} (β := F) (ae μ) (fun (x : α) ↦ HAdd.hAdd (α := F) ((T : (a : E) → F) (μ[f | m] x) : F) a)
    μ[fun (y : α) ↦ HAdd.hAdd (α := F) ((T : (a : E) → F) (f y) : F) a | m]

Tactic:
exact hp.trans (condExp_add (T.integrable_comp hf_int) (integrable_const a) m).symm

Premises used: Filter.EventuallyEq.trans, MeasureTheory.condExp_add, ContinuousLinearMap.integrable_comp, MeasureTheory.integrable_const, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
Goal:
α : Type u_1
E : Type u_3
𝕜 : Type u_4
inst : RCLike 𝕜
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : CompleteSpace E
inst_4 : InnerProductSpace 𝕜 E
hm : m ≤ m₀
hf1 : Integrable f μ
hf2 : MemLp f 2 μ
inst_5 : SigmaFinite (μ.trim hm)
⊢ (↑(↑(↑((condExpL2 E 𝕜 hm : (a : ↥(Lp E 2 μ)) → ↥(lpMeas E 𝕜 m 2 μ)) (toLp f hf2)) : ↥(Lp E 2 μ)) : α →ₘ[μ] E) :
      α → E) =ᶠ[ae μ]
    μ[f | m]

Tactic:
ae_eq_condExp_of_forall_setIntegral_eq hm hf1
    (fun s hs htop ↦ integrableOn_condExpL2_of_measure_ne_top hm htop.ne _) (fun s hs htop ↦ ?_)
    (aestronglyMeasurable_condExpL2 hm _)

Premises used: MeasureTheory.aestronglyMeasurable_condExpL2, MeasureTheory.MemLp.toLp, MeasureTheory.integrableOn_condExpL2_of_measure_ne_top, MeasureTheory.ae_eq_condExp_of_forall_setIntegral_eq, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
Goal:
α : Type u_1
E : Type u_3
𝕜 : Type u_4
inst : RCLike 𝕜
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : CompleteSpace E
inst_4 : InnerProductSpace 𝕜 E
hm : m ≤ m₀
hf1 : Integrable f μ
hf2 : MemLp f 2 μ
inst_5 : SigmaFinite (μ.trim hm)
refine :
  ∀ (s : Set α) (hs : MeasurableSet s) (htop : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
    Eq.{u_3 + 1} (α := E)
      (∫ (x : α) in s,
        (↑(↑(↑((condExpL2 E 𝕜 hm : (a : ↥(Lp E 2 μ)) → ↥(lpMeas E 𝕜 m 2 μ)) (toLp f hf2)) : ↥(Lp E 2 μ)) : α →ₘ[μ] E) :
            α → E)
          x ∂μ)
      (∫ (x : α) in s, f x ∂μ)
⊢ (↑(↑(↑((condExpL2 E 𝕜 hm : (a : ↥(Lp E 2 μ)) → ↥(lpMeas E 𝕜 m 2 μ)) (toLp f hf2)) : ↥(Lp E 2 μ)) : α →ₘ[μ] E) :
      α → E) =ᶠ[ae μ]
    μ[f | m]

Tactic:
refine ae_eq_condExp_of_forall_setIntegral_eq hm hf1
    (fun s hs htop ↦ integrableOn_condExpL2_of_measure_ne_top hm htop.ne _) (fun s hs htop ↦ ?_)
    (aestronglyMeasurable_condExpL2 hm _)

Premises used: MeasureTheory.aestronglyMeasurable_condExpL2, MeasureTheory.integrableOn_condExpL2_of_measure_ne_top, MeasureTheory.ae_eq_condExp_of_forall_setIntegral_eq, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
Goal:
α : Type u_1
E : Type u_3
𝕜 : Type u_4
inst : RCLike 𝕜
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : CompleteSpace E
inst_4 : InnerProductSpace 𝕜 E
hm : m ≤ m₀
hf1 : Integrable f μ
hf2 : MemLp f 2 μ
inst_5 : SigmaFinite (μ.trim hm)
s : Set α
hs : MeasurableSet s
htop : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
rw : Eq.{u_3 + 1} (α := E) (∫ (x : α) in s, (↑(↑(toLp f hf2) : α →ₘ[μ] E) : α → E) x ∂μ) (∫ (x : α) in s, f x ∂μ)
⊢ Eq.{u_3 + 1} (α := E)
    (∫ (x : α) in s,
      (↑(↑(↑((condExpL2 E 𝕜 hm : (a : ↥(Lp E 2 μ)) → ↥(lpMeas E 𝕜 m 2 μ)) (toLp f hf2)) : ↥(Lp E 2 μ)) : α →ₘ[μ] E) :
          α → E)
        x ∂μ)
    (∫ (x : α) in s, f x ∂μ)

Tactic:
rw [integral_condExpL2_eq hm (hf2.toLp _) hs htop.ne]

Premises used: MeasureTheory.integral_condExpL2_eq, MeasureTheory.MemLp.toLp, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
Goal:
α : Type u_1
E : Type u_3
𝕜 : Type u_4
inst : RCLike 𝕜
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : CompleteSpace E
inst_4 : InnerProductSpace 𝕜 E
hm : m ≤ m₀
hf1 : Integrable f μ
hf2 : MemLp f 2 μ
inst_5 : SigmaFinite (μ.trim hm)
s : Set α
hs : MeasurableSet s
htop : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : α) in s, (↑(↑(toLp f hf2) : α →ₘ[μ] E) : α → E) x ∂μ) (∫ (x : α) in s, f x ∂μ)

Tactic:
setIntegral_congr_ae (hm _ hs) ?_

Premises used: MeasureTheory.setIntegral_congr_ae
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
Goal:
α : Type u_1
E : Type u_3
𝕜 : Type u_4
inst : RCLike 𝕜
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : CompleteSpace E
inst_4 : InnerProductSpace 𝕜 E
hm : m ≤ m₀
hf1 : Integrable f μ
hf2 : MemLp f 2 μ
inst_5 : SigmaFinite (μ.trim hm)
s : Set α
hs : MeasurableSet s
htop : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
refine : ∀ᵐ (x : α) ∂μ, x ∈ s → (↑(↑(toLp f hf2) : α →ₘ[μ] E) : α → E) x = f x
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : α) in s, (↑(↑(toLp f hf2) : α →ₘ[μ] E) : α → E) x ∂μ) (∫ (x : α) in s, f x ∂μ)

Tactic:
refine setIntegral_congr_ae (hm _ hs) ?_

Premises used: MeasureTheory.setIntegral_congr_ae
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
Goal:
α : Type u_1
E : Type u_3
𝕜 : Type u_4
inst : RCLike 𝕜
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : CompleteSpace E
inst_4 : InnerProductSpace 𝕜 E
hm : m ≤ m₀
hf1 : Integrable f μ
hf2 : MemLp f 2 μ
inst_5 : SigmaFinite (μ.trim hm)
s : Set α
hs : MeasurableSet s
htop : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ω : α
hω : (↑(↑(toLp f hf2) : α →ₘ[μ] E) : α → E) ω = f ω
h : ω ∈ s → (↑(↑(toLp f hf2) : α →ₘ[μ] E) : α → E) ω = f ω
⊢ ω ∈ s → (↑(↑(toLp f hf2) : α →ₘ[μ] E) : α → E) ω = f ω

Tactic:
_
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
Goal:
α : Type u_1
E : Type u_3
𝕜 : Type u_4
inst : RCLike 𝕜
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : CompleteSpace E
inst_4 : InnerProductSpace 𝕜 E
hm : m ≤ m₀
hf1 : Integrable f μ
hf2 : MemLp f 2 μ
inst_5 : SigmaFinite (μ.trim hm)
s : Set α
hs : MeasurableSet s
htop : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ω : α
hω : (↑(↑(toLp f hf2) : α →ₘ[μ] E) : α → E) ω = f ω
h : ω ∈ s
⊢ (↑(↑(toLp f hf2) : α →ₘ[μ] E) : α → E) ω = f ω

Tactic:
hω
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
Goal:
α : Type u_1
E : Type u_3
𝕜 : Type u_4
inst : RCLike 𝕜
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : CompleteSpace E
inst_4 : InnerProductSpace 𝕜 E
hm : m ≤ m₀
hf1 : Integrable f μ
hf2 : MemLp f 2 μ
inst_5 : SigmaFinite (μ.trim hm)
s : Set α
hs : MeasurableSet s
htop : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
h :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x : α |
        Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ (↑(↑(toLp f hf2) : α →ₘ[μ] E) : α → E) x = f x) x} x →
          Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ x ∈ s → (↑(↑(toLp f hf2) : α →ₘ[μ] E) : α → E) x = f x) x}
            x}
      a
h₁ h₂ :
  ∀ (ω : α) (hω : (↑(↑(toLp f hf2) : α →ₘ[μ] E) : α → E) ω = f ω),
    ω ∈ s → (↑(↑(toLp f hf2) : α →ₘ[μ] E) : α → E) ω = f ω
⊢ ∀ᵐ (x : α) ∂μ, x ∈ s → (↑(↑(toLp f hf2) : α →ₘ[μ] E) : α → E) x = f x

Tactic:
filter_upwards [hf2.coeFn_toLp] with ω hω _ using hω

Premises used: MeasureTheory.MemLp.coeFn_toLp
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
Goal:
α : Type u_1
E : Type u_3
𝕜 : Type u_4
inst : RCLike 𝕜
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : CompleteSpace E
inst_4 : InnerProductSpace 𝕜 E
hm : m ≤ m₀
hf : MemLp f 2 μ
inst_5 : IsFiniteMeasure μ
⊢ (↑(↑(↑((condExpL2 E 𝕜 hm : (a : ↥(Lp E 2 μ)) → ↥(lpMeas E 𝕜 m 2 μ)) (toLp f hf)) : ↥(Lp E 2 μ)) : α →ₘ[μ] E) :
      α → E) =ᶠ[ae μ]
    μ[f | m]

Tactic:
hf.condExpL2_ae_eq_condExp' hm (memLp_one_iff_integrable.1 <| hf.mono_exponent one_le_two)

Premises used: MeasureTheory.MemLp.mono_exponent, MeasureTheory.MemLp.condExpL2_ae_eq_condExp', Iff.mp, one_le_two, MeasureTheory.memLp_one_iff_integrable
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
Goal:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : CompleteSpace E
pos : ∀ (hm : m ≤ m₀), eLpNorm μ[f | m] 2 μ ≤ eLpNorm f 2 μ
neg : ∀ (hm : ¬m ≤ m₀), eLpNorm μ[f | m] 2 μ ≤ eLpNorm f 2 μ
⊢ eLpNorm μ[f | m] 2 μ ≤ eLpNorm f 2 μ

Tactic:
by_cases hm : m ≤ m₀
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
Goal:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : CompleteSpace E
hm : ¬m ≤ m₀
⊢ eLpNorm μ[f | m] 2 μ ≤ eLpNorm f 2 μ

Tactic:
simp [condExp_of_not_le hm]

Premises used: MeasureTheory.condExp_of_not_le
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
Goal:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : CompleteSpace E
hm : m ≤ m₀
pos : ∀ (hfμ : SigmaFinite (μ.trim hm)), eLpNorm μ[f | m] 2 μ ≤ eLpNorm f 2 μ
neg : ∀ (hfμ : ¬SigmaFinite (μ.trim hm)), eLpNorm μ[f | m] 2 μ ≤ eLpNorm f 2 μ
⊢ eLpNorm μ[f | m] 2 μ ≤ eLpNorm f 2 μ

Tactic:
by_cases hfμ : SigmaFinite (μ.trim hm)

Premises used: MeasureTheory.SigmaFinite, MeasureTheory.Measure.trim
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
Goal:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : CompleteSpace E
hm : m ≤ m₀
hfμ : ¬SigmaFinite (μ.trim hm)
neg : eLpNorm.{u_1, u_3} (ε := E) 0 2 μ ≤ eLpNorm f 2 μ
⊢ eLpNorm μ[f | m] 2 μ ≤ eLpNorm f 2 μ

Tactic:
rw [condExp_of_not_sigmaFinite hm hfμ]

Premises used: MeasureTheory.condExp_of_not_sigmaFinite
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
Goal:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : CompleteSpace E
hm : m ≤ m₀
hfμ : ¬SigmaFinite (μ.trim hm)
⊢ eLpNorm.{u_1, u_3} (ε := E) 0 2 μ ≤ eLpNorm f 2 μ

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
Goal:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : CompleteSpace E
hm : m ≤ m₀
hfμ : SigmaFinite (μ.trim hm)
pos : ∀ (hfi : Integrable f μ), eLpNorm μ[f | m] 2 μ ≤ eLpNorm f 2 μ
neg : ∀ (hfi : ¬Integrable f μ), eLpNorm μ[f | m] 2 μ ≤ eLpNorm f 2 μ
⊢ eLpNorm μ[f | m] 2 μ ≤ eLpNorm f 2 μ

Tactic:
by_cases hfi : Integrable f μ

Premises used: MeasureTheory.Integrable
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
Goal:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : CompleteSpace E
hm : m ≤ m₀
hfμ : SigmaFinite (μ.trim hm)
hfi : ¬Integrable f μ
neg : eLpNorm.{u_1, u_3} (ε := E) 0 2 μ ≤ eLpNorm f 2 μ
⊢ eLpNorm μ[f | m] 2 μ ≤ eLpNorm f 2 μ

Tactic:
rw [condExp_of_not_integrable hfi]

Premises used: MeasureTheory.condExp_of_not_integrable
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
Goal:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : CompleteSpace E
hm : m ≤ m₀
hfμ : SigmaFinite (μ.trim hm)
hfi : ¬Integrable f μ
⊢ eLpNorm.{u_1, u_3} (ε := E) 0 2 μ ≤ eLpNorm f 2 μ

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
Goal:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : CompleteSpace E
hm : m ≤ m₀
hfμ : SigmaFinite (μ.trim hm)
hfi : Integrable f μ
pos : ∀ (hf : eLpNorm f 2 μ = ∞), eLpNorm μ[f | m] 2 μ ≤ eLpNorm f 2 μ
pos₁ : ∀ (hf : eLpNorm f 2 μ ≠ ∞), eLpNorm μ[f | m] 2 μ ≤ eLpNorm f 2 μ
⊢ eLpNorm μ[f | m] 2 μ ≤ eLpNorm f 2 μ

Tactic:
obtain hf | hf := eq_or_ne (eLpNorm f 2 μ) ∞

Premises used: eq_or_ne, Top.top, OfNat.ofNat, MeasureTheory.eLpNorm
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
Goal:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : CompleteSpace E
hm : m ≤ m₀
hfμ : SigmaFinite (μ.trim hm)
hfi : Integrable f μ
hf : eLpNorm f 2 μ = ∞
⊢ eLpNorm μ[f | m] 2 μ ≤ eLpNorm f 2 μ

Tactic:
simp [hf]
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
Goal:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : CompleteSpace E
hm : m ≤ m₀
hfμ : SigmaFinite (μ.trim hm)
hfi : Integrable f μ
hf : eLpNorm f 2 μ ≠ ∞
⊢ MemLp f 2 μ

Tactic:
replace hf : MemLp f 2 μ := ⟨hfi.1, Ne.lt_top' fun a ↦ hf a.symm⟩
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
Goal:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : CompleteSpace E
hm : m ≤ m₀
hfμ : SigmaFinite (μ.trim hm)
hfi : Integrable f μ
hf : MemLp f 2 μ
pos :
  eLpNorm.{u_1, u_3} (ε := E)
      (↑(↑(↑((condExpL2 E ℝ hm : (a : ↥(Lp E 2 μ)) → ↥(lpMeas E ℝ m 2 μ)) (MemLp.toLp f hf)) : ↥(Lp E 2 μ)) :
            α →ₘ[μ] E) :
        α → E)
      2 μ ≤
    eLpNorm f 2 μ
⊢ eLpNorm μ[f | m] 2 μ ≤ eLpNorm f 2 μ

Tactic:
rw [← eLpNorm_congr_ae (hf.condExpL2_ae_eq_condExp' (𝕜 := ℝ) hm hfi)]

Premises used: MeasureTheory.MemLp.condExpL2_ae_eq_condExp', MeasureTheory.eLpNorm_congr_ae
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
Goal:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : CompleteSpace E
hm : m ≤ m₀
hfμ : SigmaFinite (μ.trim hm)
hfi : Integrable f μ
hf : MemLp f 2 μ
⊢ eLpNorm.{u_1, u_3} (ε := E)
      (↑(↑(↑((condExpL2 E ℝ hm : (a : ↥(Lp E 2 μ)) → ↥(lpMeas E ℝ m 2 μ)) (MemLp.toLp f hf)) : ↥(Lp E 2 μ)) :
            α →ₘ[μ] E) :
        α → E)
      2 μ ≤
    eLpNorm f 2 μ

Tactic:
le_trans (eLpNorm_condExpL2_le hm _) ?_

Premises used: MeasureTheory.eLpNorm_condExpL2_le, le_trans
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
Goal:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : CompleteSpace E
hm : m ≤ m₀
hfμ : SigmaFinite (μ.trim hm)
hfi : Integrable f μ
hf : MemLp f 2 μ
pos : eLpNorm (↑(↑(MemLp.toLp f hf) : α →ₘ[μ] E) : α → E) 2 μ ≤ eLpNorm f 2 μ
⊢ eLpNorm.{u_1, u_3} (ε := E)
      (↑(↑(↑((condExpL2 E ℝ hm : (a : ↥(Lp E 2 μ)) → ↥(lpMeas E ℝ m 2 μ)) (MemLp.toLp f hf)) : ↥(Lp E 2 μ)) :
            α →ₘ[μ] E) :
        α → E)
      2 μ ≤
    eLpNorm f 2 μ

Tactic:
refine le_trans (eLpNorm_condExpL2_le hm _) ?_

Premises used: MeasureTheory.eLpNorm_condExpL2_le, le_trans
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
Goal:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : CompleteSpace E
hm : m ≤ m₀
hfμ : SigmaFinite (μ.trim hm)
hfi : Integrable f μ
hf : MemLp f 2 μ
pos pos₁ : eLpNorm f 2 μ ≤ eLpNorm f 2 μ
⊢ eLpNorm (↑(↑(MemLp.toLp f hf) : α →ₘ[μ] E) : α → E) 2 μ ≤ eLpNorm f 2 μ

Tactic:
rw [eLpNorm_congr_ae hf.coeFn_toLp]

Premises used: MeasureTheory.MemLp.coeFn_toLp, MeasureTheory.eLpNorm_congr_ae
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
Goal:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : CompleteSpace E
hf : MemLp f 2 μ
pos : ∀ (hm : m ≤ m₀), MemLp μ[f | m] 2 μ
neg : ∀ (hm : ¬m ≤ m₀), MemLp μ[f | m] 2 μ
⊢ MemLp μ[f | m] 2 μ

Tactic:
by_cases hm : m ≤ m₀
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
Goal:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : CompleteSpace E
hf : MemLp f 2 μ
hm : m ≤ m₀
⊢ MemLp μ[f | m] 2 μ

Tactic:
⟨(stronglyMeasurable_condExp.mono hm).aestronglyMeasurable,
      eLpNorm_condExp_le.trans_lt hf.eLpNorm_lt_top⟩

Premises used: MeasureTheory.eLpNorm_condExp_le, MeasureTheory.StronglyMeasurable.aestronglyMeasurable, MeasureTheory.MemLp, MeasureTheory.stronglyMeasurable_condExp, MeasureTheory.StronglyMeasurable.mono, And.intro, MeasureTheory.MemLp.eLpNorm_lt_top, LE.le.trans_lt
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
Goal:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : CompleteSpace E
hf : MemLp f 2 μ
hm : m ≤ m₀
⊢ MemLp μ[f | m] 2 μ

Tactic:
exact ⟨(stronglyMeasurable_condExp.mono hm).aestronglyMeasurable,
      eLpNorm_condExp_le.trans_lt hf.eLpNorm_lt_top⟩
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
Goal:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : CompleteSpace E
hf : MemLp f 2 μ
hm : ¬m ≤ m₀
⊢ MemLp μ[f | m] 2 μ

Tactic:
simp [condExp_of_not_le hm]

Premises used: MeasureTheory.condExp_of_not_le
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
Goal:
α : Type u_1
m m₀ : MeasurableSpace α
μ : Measure α
R : Type u_5
inst : NormedRing R
inst_1 : NormedSpace ℝ R
inst_2 : CompleteSpace R
n : ℕ
inst_3 : n.AtLeastTwo
f : α → R
⊢ μ[OfNat.ofNat n * f | m] =ᶠ[ae μ] OfNat.ofNat n * μ[f | m]

Tactic:
simpa [Nat.cast_smul_eq_nsmul] using condExp_smul (μ := μ) (m := m) (n : ℝ) f

Premises used: MeasureTheory.condExp_smul, Nat.cast, Nat.cast_smul_eq_nsmul
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
Goal:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
hm : m ≤ m₀
inst_2 : SigmaFinite (μ.trim hm)
fs : ℕ → α → E
f : α → E
bound_fs : α → ℝ
hfs_meas : ∀ (n : ℕ), AEStronglyMeasurable (fs n) μ
h_int_bound_fs : Integrable bound_fs μ
hfs_bound : ∀ (n : ℕ), ∀ᵐ (x : α) ∂μ, ‖fs n x‖ ≤ bound_fs x
hfs : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ fs n x) atTop (𝓝 (f x))
⊢ Tendsto (β := ↥(Lp E 1 μ)) (fun (n : ℕ) ↦ condExpL1 hm μ (fs n)) atTop (𝓝 (condExpL1 hm μ f))

Tactic:
tendsto_setToFun_of_dominated_convergence _ bound_fs hfs_meas h_int_bound_fs hfs_bound hfs

Premises used: Set.Mem, MeasureTheory.condExpL1, MeasureTheory.tendsto_setToFun_of_dominated_convergence
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
Goal:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
fs gs : ℕ → α → E
f g : α → E
hfs_int : ∀ (n : ℕ), Integrable (fs n) μ
hgs_int : ∀ (n : ℕ), Integrable (gs n) μ
hfs : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ fs n x) atTop (𝓝 (f x))
hgs : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ gs n x) atTop (𝓝 (g x))
bound_fs : α → ℝ
h_int_bound_fs : Integrable bound_fs μ
bound_gs : α → ℝ
h_int_bound_gs : Integrable bound_gs μ
hfs_bound : ∀ (n : ℕ), ∀ᵐ (x : α) ∂μ, ‖fs n x‖ ≤ bound_fs x
hgs_bound : ∀ (n : ℕ), ∀ᵐ (x : α) ∂μ, ‖gs n x‖ ≤ bound_gs x
hfg : ∀ (n : ℕ), μ[fs n | m] =ᶠ[ae μ] μ[gs n | m]
pos : ∀ (hm : m ≤ m₀), μ[f | m] =ᶠ[ae μ] μ[g | m]
neg : ∀ (hm : ¬m ≤ m₀), μ[f | m] =ᶠ[ae μ] μ[g | m]
⊢ μ[f | m] =ᶠ[ae μ] μ[g | m]

Tactic:
by_cases hm : m ≤ m₀
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
Goal:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
fs gs : ℕ → α → E
f g : α → E
hfs_int : ∀ (n : ℕ), Integrable (fs n) μ
hgs_int : ∀ (n : ℕ), Integrable (gs n) μ
hfs : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ fs n x) atTop (𝓝 (f x))
hgs : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ gs n x) atTop (𝓝 (g x))
bound_fs : α → ℝ
h_int_bound_fs : Integrable bound_fs μ
bound_gs : α → ℝ
h_int_bound_gs : Integrable bound_gs μ
hfs_bound : ∀ (n : ℕ), ∀ᵐ (x : α) ∂μ, ‖fs n x‖ ≤ bound_fs x
hgs_bound : ∀ (n : ℕ), ∀ᵐ (x : α) ∂μ, ‖gs n x‖ ≤ bound_gs x
hfg : ∀ (n : ℕ), μ[fs n | m] =ᶠ[ae μ] μ[gs n | m]
hm : ¬m ≤ m₀
neg : EventuallyEq.{u_1, u_3} (β := E) (ae μ) 0 0
⊢ μ[f | m] =ᶠ[ae μ] μ[g | m]

Tactic:
simp_rw [condExp_of_not_le hm]

Premises used: MeasureTheory.condExp_of_not_le
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
Goal:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
fs gs : ℕ → α → E
f g : α → E
hfs_int : ∀ (n : ℕ), Integrable (fs n) μ
hgs_int : ∀ (n : ℕ), Integrable (gs n) μ
hfs : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ fs n x) atTop (𝓝 (f x))
hgs : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ gs n x) atTop (𝓝 (g x))
bound_fs : α → ℝ
h_int_bound_fs : Integrable bound_fs μ
bound_gs : α → ℝ
h_int_bound_gs : Integrable bound_gs μ
hfs_bound : ∀ (n : ℕ), ∀ᵐ (x : α) ∂μ, ‖fs n x‖ ≤ bound_fs x
hgs_bound : ∀ (n : ℕ), ∀ᵐ (x : α) ∂μ, ‖gs n x‖ ≤ bound_gs x
hfg : ∀ (n : ℕ), μ[fs n | m] =ᶠ[ae μ] μ[gs n | m]
hm : ¬m ≤ m₀
⊢ EventuallyEq.{u_1, u_3} (β := E) (ae μ) 0 0

Tactic:
rfl
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
Goal:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
fs gs : ℕ → α → E
f g : α → E
hfs_int : ∀ (n : ℕ), Integrable (fs n) μ
hgs_int : ∀ (n : ℕ), Integrable (gs n) μ
hfs : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ fs n x) atTop (𝓝 (f x))
hgs : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ gs n x) atTop (𝓝 (g x))
bound_fs : α → ℝ
h_int_bound_fs : Integrable bound_fs μ
bound_gs : α → ℝ
h_int_bound_gs : Integrable bound_gs μ
hfs_bound : ∀ (n : ℕ), ∀ᵐ (x : α) ∂μ, ‖fs n x‖ ≤ bound_fs x
hgs_bound : ∀ (n : ℕ), ∀ᵐ (x : α) ∂μ, ‖gs n x‖ ≤ bound_gs x
hfg : ∀ (n : ℕ), μ[fs n | m] =ᶠ[ae μ] μ[gs n | m]
hm : m ≤ m₀
pos : ∀ (hμm : SigmaFinite (μ.trim hm)), μ[f | m] =ᶠ[ae μ] μ[g | m]
neg : ∀ (hμm : ¬SigmaFinite (μ.trim hm)), μ[f | m] =ᶠ[ae μ] μ[g | m]
⊢ μ[f | m] =ᶠ[ae μ] μ[g | m]

Tactic:
by_cases hμm : SigmaFinite (μ.trim hm)

Premises used: MeasureTheory.SigmaFinite, MeasureTheory.Measure.trim
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
Goal:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
fs gs : ℕ → α → E
f g : α → E
hfs_int : ∀ (n : ℕ), Integrable (fs n) μ
hgs_int : ∀ (n : ℕ), Integrable (gs n) μ
hfs : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ fs n x) atTop (𝓝 (f x))
hgs : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ gs n x) atTop (𝓝 (g x))
bound_fs : α → ℝ
h_int_bound_fs : Integrable bound_fs μ
bound_gs : α → ℝ
h_int_bound_gs : Integrable bound_gs μ
hfs_bound : ∀ (n : ℕ), ∀ᵐ (x : α) ∂μ, ‖fs n x‖ ≤ bound_fs x
hgs_bound : ∀ (n : ℕ), ∀ᵐ (x : α) ∂μ, ‖gs n x‖ ≤ bound_gs x
hfg : ∀ (n : ℕ), μ[fs n | m] =ᶠ[ae μ] μ[gs n | m]
hm : m ≤ m₀
hμm : ¬SigmaFinite (μ.trim hm)
neg : EventuallyEq.{u_1, u_3} (β := E) (ae μ) 0 0
⊢ μ[f | m] =ᶠ[ae μ] μ[g | m]

Tactic:
simp_rw [condExp_of_not_sigmaFinite hm hμm]

Premises used: MeasureTheory.condExp_of_not_sigmaFinite