awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
Goal:
α : Type u_1
F' : Type u_3
inst : NormedAddCommGroup F'
inst_1 : NormedSpace ℝ F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst_2 : SigmaFinite (μ.trim hm)
f : α → F'
hF' : CompleteSpace ↥(Lp F' 1 μ)
hf : Integrable f μ
hf' : f =ᶠ[ae μ] 0
pos : 0 =ᶠ[ae μ] (↑(↑(condExpL1 hm μ f) : α →ₘ[μ] F') : α → F')
⊢ AEStronglyMeasurable (↑(↑(condExpL1 hm μ f) : α →ₘ[μ] F') : α → F') μ

Tactic:
apply stronglyMeasurable_zero.aestronglyMeasurable.congr

Premises used: MeasureTheory.AEStronglyMeasurable.congr, MeasureTheory.StronglyMeasurable.aestronglyMeasurable, MeasureTheory.stronglyMeasurable_zero
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
Goal:
α : Type u_1
F' : Type u_3
inst : NormedAddCommGroup F'
inst_1 : NormedSpace ℝ F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst_2 : SigmaFinite (μ.trim hm)
f : α → F'
hF' : CompleteSpace ↥(Lp F' 1 μ)
hf : Integrable f μ
hf' : f =ᶠ[ae μ] 0
pos : EventuallyEq.{u_1, u_3} (β := F') (ae μ) 0 (↑0 : α → F')
⊢ 0 =ᶠ[ae μ] (↑(↑(condExpL1 hm μ f) : α →ₘ[μ] F') : α → F')

Tactic:
simp only [condExpL1_congr_ae hm hf', condExpL1_zero, ZeroMemClass.coe_zero]

Premises used: ZeroMemClass.coe_zero, MeasureTheory.condExpL1_zero, MeasureTheory.condExpL1_congr_ae
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
Goal:
α : Type u_1
F' : Type u_3
inst : NormedAddCommGroup F'
inst_1 : NormedSpace ℝ F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst_2 : SigmaFinite (μ.trim hm)
f : α → F'
hF' : CompleteSpace ↥(Lp F' 1 μ)
hf : Integrable f μ
hf' : f =ᶠ[ae μ] 0
⊢ EventuallyEq.{u_1, u_3} (β := F') (ae μ) 0 (↑0 : α → F')

Tactic:
(coeFn_zero _ 1 _).symm

Premises used: MeasureTheory.Lp.coeFn_zero, OfNat.ofNat, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
Goal:
α : Type u_1
F' : Type u_3
inst : NormedAddCommGroup F'
inst_1 : NormedSpace ℝ F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst_2 : SigmaFinite (μ.trim hm)
f : α → F'
hF' : CompleteSpace ↥(Lp F' 1 μ)
hf : Integrable f μ
hf' : f =ᶠ[ae μ] 0
⊢ EventuallyEq.{u_1, u_3} (β := F') (ae μ) 0 (↑0 : α → F')

Tactic:
exact (coeFn_zero _ 1 _).symm

Premises used: MeasureTheory.Lp.coeFn_zero, OfNat.ofNat, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
Goal:
α : Type u_1
F' : Type u_3
inst : NormedAddCommGroup F'
inst_1 : NormedSpace ℝ F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst_2 : SigmaFinite (μ.trim hm)
f : α → F'
hF' : CompleteSpace ↥(Lp F' 1 μ)
hf : Integrable f μ
hf' : ¬f =ᶠ[ae μ] 0
apply : Integrable.toL1 f hf ≠ 0
⊢ Nontrivial ↥(Lp F' 1 μ)

Tactic:
apply nontrivial_of_ne (hf.toL1 f) 0

Premises used: nontrivial_of_ne, MeasureTheory.Integrable.toL1, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
Goal:
α : Type u_1
F' : Type u_3
inst : NormedAddCommGroup F'
inst_1 : NormedSpace ℝ F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst_2 : SigmaFinite (μ.trim hm)
f : α → F'
hF' : CompleteSpace ↥(Lp F' 1 μ)
hf : Integrable f μ
hf' grw : ¬f =ᶠ[ae μ] 0
⊢ Integrable.toL1 f hf ≠ 0

Tactic:
grw [ne_eq, Lp.ext_iff, Integrable.coeFn_toL1, coeFn_zero]

Premises used: MeasureTheory.Lp.ext_iff, ne_eq, MeasureTheory.Integrable.coeFn_toL1, MeasureTheory.Lp.coeFn_zero
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
Goal:
α : Type u_1
F' : Type u_3
inst : NormedAddCommGroup F'
inst_1 : NormedSpace ℝ F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst_2 : SigmaFinite (μ.trim hm)
f : α → F'
hF' : CompleteSpace ↥(Lp F' 1 μ)
hf : Integrable f μ
hf' : ¬f =ᶠ[ae μ] 0
⊢ ¬f =ᶠ[ae μ] 0

Tactic:
hf'
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
Goal:
α : Type u_1
F' : Type u_3
inst : NormedAddCommGroup F'
inst_1 : NormedSpace ℝ F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst_2 : SigmaFinite (μ.trim hm)
f : α → F'
hF' : CompleteSpace ↥(Lp F' 1 μ)
hf : Integrable f μ
hf' : ¬f =ᶠ[ae μ] 0
⊢ ¬f =ᶠ[ae μ] 0

Tactic:
exact hf'
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
Goal:
α : Type u_1
F' : Type u_3
inst : NormedAddCommGroup F'
inst_1 : NormedSpace ℝ F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst_2 : SigmaFinite (μ.trim hm)
f : α → F'
hF' : CompleteSpace ↥(Lp F' 1 μ)
hf : Integrable f μ
hf' : ¬f =ᶠ[ae μ] 0
⊢ Nontrivial ↥(Lp F' 1 μ)

Tactic:
have : Nontrivial (Lp F' 1 μ) := by
      apply nontrivial_of_ne (hf.toL1 f) 0
      grw [ne_eq, Lp.ext_iff, Integrable.coeFn_toL1, coeFn_zero]
      exact hf'
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
Goal:
α : Type u_1
F' : Type u_3
inst : NormedAddCommGroup F'
inst_1 : NormedSpace ℝ F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst_2 : SigmaFinite (μ.trim hm)
f : α → F'
hF' : CompleteSpace ↥(Lp F' 1 μ)
hf : Integrable f μ
hf' : ¬f =ᶠ[ae μ] 0
this : Nontrivial ↥(Lp F' 1 μ)
⊢ CompleteSpace F'

Tactic:
completeSpace_of_completeSpace_Lp F' 1 μ

Premises used: MeasureTheory.completeSpace_of_completeSpace_Lp, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
Goal:
α : Type u_1
F' : Type u_3
inst : NormedAddCommGroup F'
inst_1 : NormedSpace ℝ F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst_2 : SigmaFinite (μ.trim hm)
f : α → F'
hF' : CompleteSpace ↥(Lp F' 1 μ)
hf : Integrable f μ
hf' : ¬f =ᶠ[ae μ] 0
this : Nontrivial ↥(Lp F' 1 μ)
⊢ CompleteSpace F'

Tactic:
exact completeSpace_of_completeSpace_Lp F' 1 μ

Premises used: MeasureTheory.completeSpace_of_completeSpace_Lp, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
Goal:
α : Type u_1
F' : Type u_3
inst : NormedAddCommGroup F'
inst_1 : NormedSpace ℝ F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst_2 : SigmaFinite (μ.trim hm)
f : α → F'
hF' : CompleteSpace ↥(Lp F' 1 μ)
hf : Integrable f μ
hf' : ¬f =ᶠ[ae μ] 0
⊢ CompleteSpace F'

Tactic:
have : CompleteSpace F' := by
    have : Nontrivial (Lp F' 1 μ) := by
      apply nontrivial_of_ne (hf.toL1 f) 0
      grw [ne_eq, Lp.ext_iff, Integrable.coeFn_toL1, coeFn_zero]
      exact hf'
    exact completeSpace_of_completeSpace_Lp F' 1 μ
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
Goal:
α : Type u_1
F' : Type u_3
inst : NormedAddCommGroup F'
inst_1 : NormedSpace ℝ F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst_2 : SigmaFinite (μ.trim hm)
f : α → F'
hF' : CompleteSpace ↥(Lp F' 1 μ)
hf : Integrable f μ
hf' : ¬f =ᶠ[ae μ] 0
this : CompleteSpace F'
neg :
  AEStronglyMeasurable.{u_1, u_3} (β := F')
    (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) (Integrable.toL1 f hf)) : α →ₘ[μ] F') : α → F') μ
⊢ AEStronglyMeasurable (↑(↑(condExpL1 hm μ f) : α →ₘ[μ] F') : α → F') μ

Tactic:
rw [condExpL1_eq hf]

Premises used: MeasureTheory.condExpL1_eq
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
Goal:
α : Type u_1
F' : Type u_3
inst : NormedAddCommGroup F'
inst_1 : NormedSpace ℝ F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst_2 : SigmaFinite (μ.trim hm)
f : α → F'
hF' : CompleteSpace ↥(Lp F' 1 μ)
hf : Integrable f μ
hf' : ¬f =ᶠ[ae μ] 0
this : CompleteSpace F'
⊢ AEStronglyMeasurable.{u_1, u_3} (β := F')
    (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) (Integrable.toL1 f hf)) : α →ₘ[μ] F') : α → F') μ

Tactic:
aestronglyMeasurable_condExpL1CLM _

Premises used: MeasureTheory.aestronglyMeasurable_condExpL1CLM
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
Goal:
α : Type u_1
F' : Type u_3
inst : NormedAddCommGroup F'
inst_1 : NormedSpace ℝ F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst_2 : SigmaFinite (μ.trim hm)
f : α → F'
hF' : CompleteSpace ↥(Lp F' 1 μ)
hf : Integrable f μ
hf' : ¬f =ᶠ[ae μ] 0
this : CompleteSpace F'
⊢ AEStronglyMeasurable.{u_1, u_3} (β := F')
    (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) (Integrable.toL1 f hf)) : α →ₘ[μ] F') : α → F') μ

Tactic:
exact aestronglyMeasurable_condExpL1CLM _

Premises used: MeasureTheory.aestronglyMeasurable_condExpL1CLM
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
Goal:
α : Type u_1
F' : Type u_3
inst : NormedAddCommGroup F'
inst_1 : NormedSpace ℝ F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst_2 : SigmaFinite (μ.trim hm)
f : α → F'
⊢ Integrable (↑(↑(condExpL1 hm μ f) : α →ₘ[μ] F') : α → F') μ

Tactic:
L1.integrable_coeFn _

Premises used: MeasureTheory.L1.integrable_coeFn
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
Goal:
α : Type u_1
F' : Type u_3
inst : NormedAddCommGroup F'
inst_1 : NormedSpace ℝ F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst_2 : SigmaFinite (μ.trim hm)
f : α → F'
s : Set α
inst_3 : CompleteSpace F'
hf : Integrable f μ
hs : MeasurableSet s
simp_rw :
  Eq.{u_3 + 1} (α := F')
    (∫ (x : α) in s,
      (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) (Integrable.toL1 f hf)) : α →ₘ[μ] F') : α → F')
        x ∂μ)
    (∫ (x : α) in s, f x ∂μ)
⊢ Eq.{u_3 + 1} (α := F') (∫ (x : α) in s, (↑(↑(condExpL1 hm μ f) : α →ₘ[μ] F') : α → F') x ∂μ) (∫ (x : α) in s, f x ∂μ)

Tactic:
simp_rw [condExpL1_eq hf]

Premises used: MeasureTheory.condExpL1_eq
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
Goal:
α : Type u_1
F' : Type u_3
inst : NormedAddCommGroup F'
inst_1 : NormedSpace ℝ F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst_2 : SigmaFinite (μ.trim hm)
f : α → F'
s : Set α
inst_3 : CompleteSpace F'
hf : Integrable f μ
hs : MeasurableSet s
rw :
  Eq.{u_3 + 1} (α := F') (∫ (x : α) in s, (↑(↑(Integrable.toL1 f hf) : α →ₘ[μ] F') : α → F') x ∂μ)
    (∫ (x : α) in s, f x ∂μ)
⊢ Eq.{u_3 + 1} (α := F')
    (∫ (x : α) in s,
      (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) (Integrable.toL1 f hf)) : α →ₘ[μ] F') : α → F')
        x ∂μ)
    (∫ (x : α) in s, f x ∂μ)

Tactic:
rw [setIntegral_condExpL1CLM (hf.toL1 f) hs]

Premises used: MeasureTheory.Integrable.toL1, MeasureTheory.setIntegral_condExpL1CLM
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
Goal:
α : Type u_1
F' : Type u_3
inst : NormedAddCommGroup F'
inst_1 : NormedSpace ℝ F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst_2 : SigmaFinite (μ.trim hm)
f : α → F'
s : Set α
inst_3 : CompleteSpace F'
hf : Integrable f μ
hs : MeasurableSet s
⊢ Eq.{u_3 + 1} (α := F') (∫ (x : α) in s, (↑(↑(Integrable.toL1 f hf) : α →ₘ[μ] F') : α → F') x ∂μ)
    (∫ (x : α) in s, f x ∂μ)

Tactic:
setIntegral_congr_ae (hm s hs) (hf.coeFn_toL1.mono fun x hx _ => hx)

Premises used: MeasureTheory.setIntegral_congr_ae, Filter.Eventually.mono, MeasureTheory.Integrable.coeFn_toL1
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
Goal:
α : Type u_1
F' : Type u_3
inst : NormedAddCommGroup F'
inst_1 : NormedSpace ℝ F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst_2 : SigmaFinite (μ.trim hm)
f : α → F'
s : Set α
inst_3 : CompleteSpace F'
hf : Integrable f μ
hs : MeasurableSet s
⊢ Eq.{u_3 + 1} (α := F') (∫ (x : α) in s, (↑(↑(Integrable.toL1 f hf) : α →ₘ[μ] F') : α → F') x ∂μ)
    (∫ (x : α) in s, f x ∂μ)

Tactic:
exact setIntegral_congr_ae (hm s hs) (hf.coeFn_toL1.mono fun x hx _ => hx)

Premises used: MeasureTheory.setIntegral_congr_ae, Filter.Eventually.mono, MeasureTheory.Integrable.coeFn_toL1
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
Goal:
α : Type u_1
F' : Type u_3
inst : NormedAddCommGroup F'
inst_1 : NormedSpace ℝ F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst_2 : SigmaFinite (μ.trim hm)
f g : α → F'
hf : Integrable f μ
hg : Integrable g μ
⊢ condExpL1 hm μ (f + g) = HAdd.hAdd (α := ↥(Lp F' 1 μ)) (condExpL1 hm μ f) (condExpL1 hm μ g)

Tactic:
setToFun_add _ hf hg

Premises used: Set.Mem, MeasureTheory.condExpL1, MeasureTheory.setToFun_add
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
Goal:
α : Type u_1
F' : Type u_3
inst : NormedAddCommGroup F'
inst_1 : NormedSpace ℝ F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst_2 : SigmaFinite (μ.trim hm)
f : α → F'
⊢ Eq (α := ↥(Lp F' 1 μ)) (condExpL1 hm μ (-f)) (-condExpL1 hm μ f)

Tactic:
setToFun_neg _ f

Premises used: Set.Mem, MeasureTheory.condExpL1, MeasureTheory.setToFun_neg
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
Goal:
α : Type u_1
F' : Type u_3
𝕜 : Type u_6
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup F'
inst_2 : NormedSpace 𝕜 F'
inst_3 : NormedSpace ℝ F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst_4 : SigmaFinite (μ.trim hm)
c : 𝕜
f : α → F'
⊢ condExpL1 hm μ (c • f) = HSMul.hSMul (β := ↥(Lp F' 1 μ)) c (condExpL1 hm μ f)

Tactic:
setToFun_smul _ ?_ c f

Premises used: Set.Mem, MeasureTheory.condExpL1, MeasureTheory.setToFun_smul
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
Goal:
α : Type u_1
F' : Type u_3
𝕜 : Type u_6
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup F'
inst_2 : NormedSpace 𝕜 F'
inst_3 : NormedSpace ℝ F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst_4 : SigmaFinite (μ.trim hm)
c : 𝕜
f : α → F'
refine :
  ∀ (c : 𝕜) (s : Set α) (x : F'),
    (condExpInd F' hm μ s : (a : F') → ↥(Lp F' 1 μ)) (c • x) =
      HSMul.hSMul (β := ↥(Lp F' 1 μ)) c ((condExpInd F' hm μ s : (a : F') → ↥(Lp F' 1 μ)) x : ↥(Lp F' 1 μ))
⊢ condExpL1 hm μ (c • f) = HSMul.hSMul (β := ↥(Lp F' 1 μ)) c (condExpL1 hm μ f)

Tactic:
refine setToFun_smul _ ?_ c f

Premises used: MeasureTheory.setToFun_smul
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
Goal:
α : Type u_1
F' : Type u_3
𝕜 : Type u_6
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup F'
inst_2 : NormedSpace 𝕜 F'
inst_3 : NormedSpace ℝ F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst_4 : SigmaFinite (μ.trim hm)
c : 𝕜
f : α → F'
⊢ ∀ (c : 𝕜) (s : Set α) (x : F'),
    (condExpInd F' hm μ s : (a : F') → ↥(Lp F' 1 μ)) (c • x) =
      HSMul.hSMul (β := ↥(Lp F' 1 μ)) c ((condExpInd F' hm μ s : (a : F') → ↥(Lp F' 1 μ)) x : ↥(Lp F' 1 μ))

Tactic:
fun c _ x => condExpInd_smul' c x

Premises used: MeasureTheory.condExpInd_smul'
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
Goal:
α : Type u_1
F' : Type u_3
𝕜 : Type u_6
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup F'
inst_2 : NormedSpace 𝕜 F'
inst_3 : NormedSpace ℝ F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst_4 : SigmaFinite (μ.trim hm)
c : 𝕜
f : α → F'
⊢ ∀ (c : 𝕜) (s : Set α) (x : F'),
    (condExpInd F' hm μ s : (a : F') → ↥(Lp F' 1 μ)) (c • x) =
      HSMul.hSMul (β := ↥(Lp F' 1 μ)) c ((condExpInd F' hm μ s : (a : F') → ↥(Lp F' 1 μ)) x : ↥(Lp F' 1 μ))

Tactic:
exact fun c _ x => condExpInd_smul' c x

Premises used: MeasureTheory.condExpInd_smul'
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
Goal:
α : Type u_1
F' : Type u_3
inst : NormedAddCommGroup F'
inst_1 : NormedSpace ℝ F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst_2 : SigmaFinite (μ.trim hm)
f g : α → F'
hf : Integrable f μ
hg : Integrable g μ
⊢ condExpL1 hm μ (f - g) = HSub.hSub (α := ↥(Lp F' 1 μ)) (condExpL1 hm μ f) (condExpL1 hm μ g)

Tactic:
setToFun_sub _ hf hg

Premises used: Set.Mem, MeasureTheory.condExpL1, MeasureTheory.setToFun_sub
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
Goal:
α : Type u_1
F' : Type u_3
inst : NormedAddCommGroup F'
inst_1 : NormedSpace ℝ F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst_2 : SigmaFinite (μ.trim hm)
f : α → F'
inst_3 : CompleteSpace F'
hfm : AEStronglyMeasurable f μ
hfi : Integrable f μ
rw :
  (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) (Integrable.toL1 f hfi)) : α →ₘ[μ] F') :
      α → F') =ᶠ[ae μ]
    f
⊢ (↑(↑(condExpL1 hm μ f) : α →ₘ[μ] F') : α → F') =ᶠ[ae μ] f

Tactic:
rw [condExpL1_eq hfi]

Premises used: MeasureTheory.condExpL1_eq
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
Goal:
α : Type u_1
F' : Type u_3
inst : NormedAddCommGroup F'
inst_1 : NormedSpace ℝ F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst_2 : SigmaFinite (μ.trim hm)
f : α → F'
inst_3 : CompleteSpace F'
hfm : AEStronglyMeasurable f μ
hfi : Integrable f μ
⊢ (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) (Integrable.toL1 f hfi)) : α →ₘ[μ] F') :
      α → F') =ᶠ[ae μ]
    f

Tactic:
EventuallyEq.trans ?_ (Integrable.coeFn_toL1 hfi)

Premises used: Filter.EventuallyEq.trans, MeasureTheory.Integrable.coeFn_toL1
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
Goal:
α : Type u_1
F' : Type u_3
inst : NormedAddCommGroup F'
inst_1 : NormedSpace ℝ F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst_2 : SigmaFinite (μ.trim hm)
f : α → F'
inst_3 : CompleteSpace F'
hfm : AEStronglyMeasurable f μ
hfi : Integrable f μ
refine :
  (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) (Integrable.toL1 f hfi)) : α →ₘ[μ] F') :
      α → F') =ᶠ[ae μ]
    (↑(↑(Integrable.toL1 f hfi) : α →ₘ[μ] F') : α → F')
⊢ (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) (Integrable.toL1 f hfi)) : α →ₘ[μ] F') :
      α → F') =ᶠ[ae μ]
    f

Tactic:
refine EventuallyEq.trans ?_ (Integrable.coeFn_toL1 hfi)

Premises used: Filter.EventuallyEq.trans, MeasureTheory.Integrable.coeFn_toL1
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
Goal:
α : Type u_1
F' : Type u_3
inst : NormedAddCommGroup F'
inst_1 : NormedSpace ℝ F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst_2 : SigmaFinite (μ.trim hm)
f : α → F'
inst_3 : CompleteSpace F'
hfm : AEStronglyMeasurable f μ
hfi : Integrable f μ
hfm₁ : AEStronglyMeasurable (↑(↑(Integrable.toL1 f hfi) : α →ₘ[μ] F') : α → F') μ
⊢ (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) (Integrable.toL1 f hfi)) : α →ₘ[μ] F') :
      α → F') =ᶠ[ae μ]
    (↑(↑(Integrable.toL1 f hfi) : α →ₘ[μ] F') : α → F')

Tactic:
rw [condExpL1CLM_of_aestronglyMeasurable']

Premises used: MeasureTheory.condExpL1CLM_of_aestronglyMeasurable'
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
Goal:
α : Type u_1
F' : Type u_3
inst : NormedAddCommGroup F'
inst_1 : NormedSpace ℝ F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst_2 : SigmaFinite (μ.trim hm)
f : α → F'
inst_3 : CompleteSpace F'
hfm : AEStronglyMeasurable f μ
hfi : Integrable f μ
⊢ AEStronglyMeasurable (↑(↑(Integrable.toL1 f hfi) : α →ₘ[μ] F') : α → F') μ

Tactic:
hfm.congr hfi.coeFn_toL1.symm

Premises used: MeasureTheory.AEStronglyMeasurable.congr, MeasureTheory.Integrable.coeFn_toL1, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
Goal:
α : Type u_1
F' : Type u_3
inst : NormedAddCommGroup F'
inst_1 : NormedSpace ℝ F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst_2 : SigmaFinite (μ.trim hm)
f : α → F'
inst_3 : CompleteSpace F'
hfm : AEStronglyMeasurable f μ
hfi : Integrable f μ
⊢ AEStronglyMeasurable (↑(↑(Integrable.toL1 f hfi) : α →ₘ[μ] F') : α → F') μ

Tactic:
exact hfm.congr hfi.coeFn_toL1.symm

Premises used: MeasureTheory.AEStronglyMeasurable.congr, MeasureTheory.Integrable.coeFn_toL1, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst : SigmaFinite (μ.trim hm)
E : Type u_7
inst_1 : NormedAddCommGroup E
inst_2 : PartialOrder E
inst_3 : ClosedIciTopology E
inst_4 : IsOrderedAddMonoid E
inst_5 : NormedSpace ℝ E
inst_6 : IsOrderedModule ℝ E
f g : α → E
hf : Integrable f μ
hg : Integrable g μ
hfg : f ≤ᶠ[ae μ] g
rw : LE.le (α := ↥(Lp E 1 μ)) (condExpL1 hm μ f) (condExpL1 hm μ g)
⊢ (↑(↑(condExpL1 hm μ f) : α →ₘ[μ] E) : α → E) ≤ᶠ[ae μ] (↑(↑(condExpL1 hm μ g) : α →ₘ[μ] E) : α → E)

Tactic:
rw [coeFn_le]

Premises used: MeasureTheory.Lp.coeFn_le
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst : SigmaFinite (μ.trim hm)
E : Type u_7
inst_1 : NormedAddCommGroup E
inst_2 : PartialOrder E
inst_3 : ClosedIciTopology E
inst_4 : IsOrderedAddMonoid E
inst_5 : NormedSpace ℝ E
inst_6 : IsOrderedModule ℝ E
f g : α → E
hf : Integrable f μ
hg : Integrable g μ
hfg : f ≤ᶠ[ae μ] g
⊢ ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        ∀ (x : E),
          0 ≤ x →
            LE.le (α := ↥(Lp E 1 μ)) (0 : ↥(Lp E 1 μ)) ((condExpInd E hm μ s : (a : E) → ↥(Lp E 1 μ)) x : ↥(Lp E 1 μ))

Tactic:
have h_nonneg : ∀ s, MeasurableSet s → μ s < ∞ → ∀ x : E, 0 ≤ x → 0 ≤ condExpInd E hm μ s x :=
    fun s hs hμs x hx => condExpInd_nonneg hs hμs.ne x hx
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst : SigmaFinite (μ.trim hm)
E : Type u_7
inst_1 : NormedAddCommGroup E
inst_2 : PartialOrder E
inst_3 : ClosedIciTopology E
inst_4 : IsOrderedAddMonoid E
inst_5 : NormedSpace ℝ E
inst_6 : IsOrderedModule ℝ E
f g : α → E
hf : Integrable f μ
hg : Integrable g μ
hfg : f ≤ᶠ[ae μ] g
h_nonneg :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        ∀ (x : E),
          0 ≤ x →
            LE.le (α := ↥(Lp E 1 μ)) (0 : ↥(Lp E 1 μ)) ((condExpInd E hm μ s : (a : E) → ↥(Lp E 1 μ)) x : ↥(Lp E 1 μ))
⊢ LE.le (α := ↥(Lp E 1 μ)) (condExpL1 hm μ f) (condExpL1 hm μ g)

Tactic:
setToFun_mono (dominatedFinMeasAdditive_condExpInd E hm μ) h_nonneg hf hg hfg

Premises used: Set.Mem, MeasureTheory.dominatedFinMeasAdditive_condExpInd, MeasureTheory.setToFun_mono
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst : SigmaFinite (μ.trim hm)
E : Type u_7
inst_1 : NormedAddCommGroup E
inst_2 : PartialOrder E
inst_3 : ClosedIciTopology E
inst_4 : IsOrderedAddMonoid E
inst_5 : NormedSpace ℝ E
inst_6 : IsOrderedModule ℝ E
f g : α → E
hf : Integrable f μ
hg : Integrable g μ
hfg : f ≤ᶠ[ae μ] g
h_nonneg :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        ∀ (x : E),
          0 ≤ x →
            LE.le (α := ↥(Lp E 1 μ)) (0 : ↥(Lp E 1 μ)) ((condExpInd E hm μ s : (a : E) → ↥(Lp E 1 μ)) x : ↥(Lp E 1 μ))
⊢ LE.le (α := ↥(Lp E 1 μ)) (condExpL1 hm μ f) (condExpL1 hm μ g)

Tactic:
exact setToFun_mono (dominatedFinMeasAdditive_condExpInd E hm μ) h_nonneg hf hg hfg

Premises used: MeasureTheory.dominatedFinMeasAdditive_condExpInd, MeasureTheory.setToFun_mono
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2
Goal:
α : Type u_1
E : Type u_2
𝕜 : Type u_7
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : CompleteSpace E
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : ↥(Lp E 2 μ)
⊢ AEStronglyMeasurable.{u_1, u_2} (β := E)
    (↑(↑(↑((condExpL2 E 𝕜 hm : (a : ↥(Lp E 2 μ)) → ↥(lpMeas E 𝕜 m 2 μ)) f) : ↥(Lp E 2 μ)) : α →ₘ[μ] E) : α → E) μ

Tactic:
lpMeas.aestronglyMeasurable _

Premises used: MeasureTheory.lpMeas.aestronglyMeasurable
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2
Goal:
α : Type u_1
E : Type u_2
𝕜 : Type u_7
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : CompleteSpace E
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
f : ↥(Lp E 2 μ)
⊢ IntegrableOn.{u_1, u_2} (ε := E)
    (↑(↑(↑((condExpL2 E 𝕜 hm : (a : ↥(Lp E 2 μ)) → ↥(lpMeas E 𝕜 m 2 μ)) f) : ↥(Lp E 2 μ)) : α →ₘ[μ] E) : α → E) s μ

Tactic:
integrableOn_Lp_of_measure_ne_top (condExpL2 E 𝕜 hm f : α →₂[μ] E) fact_one_le_two_ennreal.elim
    hμs

Premises used: fact_one_le_two_ennreal, MeasureTheory.integrableOn_Lp_of_measure_ne_top, MeasureTheory.condExpL2, Fact.elim, Subtype.val, DFunLike.coe