awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1 (goal)
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)
inst_3 : CompleteSpace F'
f : ↥(lpMeas F' ℝ m 1 μ)
g : ↥(Lp F' 1 (μ.trim hm)) := (lpMeasToLpTrimLie F' ℝ 1 μ hm : (a : ↥(lpMeas F' ℝ m 1 μ)) → ↥(Lp F' 1 (μ.trim hm))) f
hfg :
  f = (LinearIsometryEquiv.symm (lpMeasToLpTrimLie F' ℝ 1 μ hm) : (a : ↥(Lp F' 1 (μ.trim hm))) → ↥(lpMeas F' ℝ m 1 μ)) g
⊢ Eq (α := ↥(Lp F' 1 μ))
    ((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ))
      (↑((LinearIsometryEquiv.symm (lpMeasToLpTrimLie F' ℝ 1 μ hm) :
              (a : ↥(Lp F' 1 (μ.trim hm))) → ↥(lpMeas F' ℝ m 1 μ))
            g) :
        ↥(Lp F' 1 μ)))
    (↑((LinearIsometryEquiv.symm (lpMeasToLpTrimLie F' ℝ 1 μ hm) : (a : ↥(Lp F' 1 (μ.trim hm))) → ↥(lpMeas F' ℝ m 1 μ))
          g) :
      ↥(Lp F' 1 μ))
have refine_1 : ∀ (c : F') {s : Set α} (hs : MeasurableSet s)
  (hμs : LT.lt (α := ℝ≥0∞) ((μ.trim hm : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
  (fun (g : ↥(Lp F' 1 (μ.trim hm))) ↦
      Eq (α := ↥(Lp F' 1 μ))
        ((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ))
          (↑((LinearIsometryEquiv.symm (lpMeasToLpTrimLie F' ℝ 1 μ hm) :
                  (a : ↥(Lp F' 1 (μ.trim hm))) → ↥(lpMeas F' ℝ m 1 μ))
                g) :
            ↥(Lp F' 1 μ)))
        (↑((LinearIsometryEquiv.symm (lpMeasToLpTrimLie F' ℝ 1 μ hm) :
                (a : ↥(Lp F' 1 (μ.trim hm))) → ↥(lpMeas F' ℝ m 1 μ))
              g) :
          ↥(Lp F' 1 μ)))
    (↑(simpleFunc.indicatorConst 1 (s := s) hs sorry c) : ↥(Lp F' 1 (μ.trim hm)))
Tactic: refine @Lp.induction α F' m _ 1 (μ.trim hm) _ ENNReal.coe_ne_top (fun g : α →₁[μ.trim hm] F' =>
    condExpL1CLM F' hm μ ((lpMeasToLpTrimLie F' ℝ 1 μ hm).symm g : α →₁[μ] F') =
    ↑((lpMeasToLpTrimLie F' ℝ 1 μ hm).symm g)) ?_ ?_ ?_ g
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1 (goal)
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)
inst_3 : CompleteSpace F'
f : ↥(lpMeas F' ℝ m 1 μ)
g : ↥(Lp F' 1 (μ.trim hm)) := (lpMeasToLpTrimLie F' ℝ 1 μ hm : (a : ↥(lpMeas F' ℝ m 1 μ)) → ↥(Lp F' 1 (μ.trim hm))) f
hfg :
  f = (LinearIsometryEquiv.symm (lpMeasToLpTrimLie F' ℝ 1 μ hm) : (a : ↥(Lp F' 1 (μ.trim hm))) → ↥(lpMeas F' ℝ m 1 μ)) g
c : F'
s : Set α
hs : MeasurableSet s
hμs : LT.lt (α := ℝ≥0∞) ((μ.trim hm : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Eq (α := ↥(Lp F' 1 μ))
    ((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ))
      (↑((LinearIsometryEquiv.symm (lpMeasToLpTrimLie F' ℝ 1 μ hm) :
              (a : ↥(Lp F' 1 (μ.trim hm))) → ↥(lpMeas F' ℝ m 1 μ))
            (↑(simpleFunc.indicatorConst 1 (s := s) hs ⋯ c) : ↥(Lp F' 1 (μ.trim hm)))) :
        ↥(Lp F' 1 μ)))
    (↑((LinearIsometryEquiv.symm (lpMeasToLpTrimLie F' ℝ 1 μ hm) : (a : ↥(Lp F' 1 (μ.trim hm))) → ↥(lpMeas F' ℝ m 1 μ))
          (↑(simpleFunc.indicatorConst 1 (s := s) hs ⋯ c) : ↥(Lp F' 1 (μ.trim hm)))) :
      ↥(Lp F' 1 μ))
have refine_1 : Eq (α := ↥(Lp F' 1 μ)) ((condExpInd F' hm μ s : (a : F') → ↥(Lp F' 1 μ)) c : ↥(Lp F' 1 μ))
  (indicatorConstLp (s := s) 1 sorry sorry c : ↥(Lp F' 1 μ))
Tactic: rw [@Lp.simpleFunc.coe_indicatorConst _ _ m, lpMeasToLpTrimLie_symm_indicator hs hμs.ne c,
      condExpL1CLM_indicatorConstLp]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1 (goal)
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)
inst_3 : CompleteSpace F'
f : ↥(lpMeas F' ℝ m 1 μ)
g : ↥(Lp F' 1 (μ.trim hm)) := (lpMeasToLpTrimLie F' ℝ 1 μ hm : (a : ↥(lpMeas F' ℝ m 1 μ)) → ↥(Lp F' 1 (μ.trim hm))) f
hfg :
  f = (LinearIsometryEquiv.symm (lpMeasToLpTrimLie F' ℝ 1 μ hm) : (a : ↥(Lp F' 1 (μ.trim hm))) → ↥(lpMeas F' ℝ m 1 μ)) g
⊢ IsClosed (X := ↥(Lp F' 1 (μ.trim hm)))
    {f : ↥(Lp F' 1 (μ.trim hm)) |
      (fun (g : ↥(Lp F' 1 (μ.trim hm))) ↦
          Eq (α := ↥(Lp F' 1 μ))
            ((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ))
              (↑((LinearIsometryEquiv.symm (lpMeasToLpTrimLie F' ℝ 1 μ hm) :
                      (a : ↥(Lp F' 1 (μ.trim hm))) → ↥(lpMeas F' ℝ m 1 μ))
                    g) :
                ↥(Lp F' 1 μ)))
            (↑((LinearIsometryEquiv.symm (lpMeasToLpTrimLie F' ℝ 1 μ hm) :
                    (a : ↥(Lp F' 1 (μ.trim hm))) → ↥(lpMeas F' ℝ m 1 μ))
                  g) :
              ↥(Lp F' 1 μ)))
        f}
have refine_3 : Continuous (Y := ↥(Lp F' 1 μ)) fun (f : ↥(Lp F' 1 (μ.trim hm))) ↦
  (condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ))
    (↑((LinearIsometryEquiv.symm (lpMeasToLpTrimLie F' ℝ 1 μ hm) : (a : ↥(Lp F' 1 (μ.trim hm))) → ↥(lpMeas F' ℝ m 1 μ))
          f) :
      ↥(Lp F' 1 μ))
Tactic: refine isClosed_eq ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1 (goal)
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)
inst_3 : CompleteSpace F'
f : ↥(lpMeas F' ℝ m 1 μ)
g : ↥(Lp F' 1 (μ.trim hm)) := (lpMeasToLpTrimLie F' ℝ 1 μ hm : (a : ↥(lpMeas F' ℝ m 1 μ)) → ↥(Lp F' 1 (μ.trim hm))) f
hfg :
  f = (LinearIsometryEquiv.symm (lpMeasToLpTrimLie F' ℝ 1 μ hm) : (a : ↥(Lp F' 1 (μ.trim hm))) → ↥(lpMeas F' ℝ m 1 μ)) g
refine_3 :
  Continuous (Y := ↥(Lp F' 1 μ)) fun (f : ↥(Lp F' 1 (μ.trim hm))) ↦
    (condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ))
      (↑((LinearIsometryEquiv.symm (lpMeasToLpTrimLie F' ℝ 1 μ hm) :
              (a : ↥(Lp F' 1 (μ.trim hm))) → ↥(lpMeas F' ℝ m 1 μ))
            f) :
        ↥(Lp F' 1 μ))
⊢ IsClosed (X := ↥(Lp F' 1 (μ.trim hm)))
    {f : ↥(Lp F' 1 (μ.trim hm)) |
      (fun (g : ↥(Lp F' 1 (μ.trim hm))) ↦
          Eq (α := ↥(Lp F' 1 μ))
            ((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ))
              (↑((LinearIsometryEquiv.symm (lpMeasToLpTrimLie F' ℝ 1 μ hm) :
                      (a : ↥(Lp F' 1 (μ.trim hm))) → ↥(lpMeas F' ℝ m 1 μ))
                    g) :
                ↥(Lp F' 1 μ)))
            (↑((LinearIsometryEquiv.symm (lpMeasToLpTrimLie F' ℝ 1 μ hm) :
                    (a : ↥(Lp F' 1 (μ.trim hm))) → ↥(lpMeas F' ℝ m 1 μ))
                  g) :
              ↥(Lp F' 1 μ)))
        f}
have refine_3₁ : Continuous (Y := ↥(Lp F' 1 μ)) fun (f : ↥(Lp F' 1 (μ.trim hm))) ↦
  (↑((LinearIsometryEquiv.symm (lpMeasToLpTrimLie F' ℝ 1 μ hm) : (a : ↥(Lp F' 1 (μ.trim hm))) → ↥(lpMeas F' ℝ m 1 μ))
        f) :
    ↥(Lp F' 1 μ))
Tactic: refine isClosed_eq ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1 (goal)
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)
inst_3 : CompleteSpace F'
f : ↥(lpMeas F' ℝ m 1 μ)
g : ↥(Lp F' 1 (μ.trim hm)) := (lpMeasToLpTrimLie F' ℝ 1 μ hm : (a : ↥(lpMeas F' ℝ m 1 μ)) → ↥(Lp F' 1 (μ.trim hm))) f
hfg :
  f = (LinearIsometryEquiv.symm (lpMeasToLpTrimLie F' ℝ 1 μ hm) : (a : ↥(Lp F' 1 (μ.trim hm))) → ↥(lpMeas F' ℝ m 1 μ)) g
⊢ Continuous (Y := ↥(Lp F' 1 μ)) fun (f : ↥(Lp F' 1 (μ.trim hm))) ↦
    (condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ))
      (↑((LinearIsometryEquiv.symm (lpMeasToLpTrimLie F' ℝ 1 μ hm) :
              (a : ↥(Lp F' 1 (μ.trim hm))) → ↥(lpMeas F' ℝ m 1 μ))
            f) :
        ↥(Lp F' 1 μ))
have refine_3 : Continuous (X := ↥(Lp F' 1 (μ.trim hm))) (Y := ↥(lpMeas F' ℝ m 1 μ))
  (⇑(LinearIsometryEquiv.symm (lpMeasToLpTrimLie F' ℝ 1 μ hm)) : (a : ↥(Lp F' 1 (μ.trim hm))) → ↥(lpMeas F' ℝ m 1 μ))
Tactic: refine (condExpL1CLM F' hm μ).continuous.comp (continuous_induced_dom.comp ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1 (goal)
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)
inst_3 : CompleteSpace F'
f : ↥(lpMeas F' ℝ m 1 μ)
g : ↥(Lp F' 1 (μ.trim hm)) := (lpMeasToLpTrimLie F' ℝ 1 μ hm : (a : ↥(lpMeas F' ℝ m 1 μ)) → ↥(Lp F' 1 (μ.trim hm))) f
hfg :
  f = (LinearIsometryEquiv.symm (lpMeasToLpTrimLie F' ℝ 1 μ hm) : (a : ↥(Lp F' 1 (μ.trim hm))) → ↥(lpMeas F' ℝ m 1 μ)) g
⊢ Continuous (Y := ↥(Lp F' 1 μ)) fun (f : ↥(Lp F' 1 (μ.trim hm))) ↦
    (↑((LinearIsometryEquiv.symm (lpMeasToLpTrimLie F' ℝ 1 μ hm) : (a : ↥(Lp F' 1 (μ.trim hm))) → ↥(lpMeas F' ℝ m 1 μ))
          f) :
      ↥(Lp F' 1 μ))
have refine_3 : Continuous (X := ↥(Lp F' 1 (μ.trim hm))) (Y := ↥(lpMeas F' ℝ m 1 μ))
  (⇑(LinearIsometryEquiv.symm (lpMeasToLpTrimLie F' ℝ 1 μ hm)) : (a : ↥(Lp F' 1 (μ.trim hm))) → ↥(lpMeas F' ℝ m 1 μ))
Tactic: refine continuous_induced_dom.comp ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1 (goal)
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'
⊢ AEStronglyMeasurable (↑(↑(condExpL1 hm μ f) : α →ₘ[μ] F') : α → F') μ
have pos : ∀ (hF' : CompleteSpace ↥(Lp F' 1 μ)), AEStronglyMeasurable (↑(↑(condExpL1 hm μ f) : α →ₘ[μ] F') : α → F') μ
Tactic: by_cases hF' : CompleteSpace (Lp F' 1 μ)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1 (goal)
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'
pos : ∀ (hF' : CompleteSpace ↥(Lp F' 1 μ)), AEStronglyMeasurable (↑(↑(condExpL1 hm μ f) : α →ₘ[μ] F') : α → F') μ
⊢ AEStronglyMeasurable (↑(↑(condExpL1 hm μ f) : α →ₘ[μ] F') : α → F') μ
have neg : ∀ (hF' : ¬CompleteSpace ↥(Lp F' 1 μ)), AEStronglyMeasurable (↑(↑(condExpL1 hm μ f) : α →ₘ[μ] F') : α → F') μ
Tactic: by_cases hF' : CompleteSpace (Lp F' 1 μ)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1 (goal)
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 μ)
⊢ AEStronglyMeasurable (↑(↑(condExpL1 hm μ f) : α →ₘ[μ] F') : α → F') μ
have neg : AEStronglyMeasurable.{u_1, u_3} (β := F') (↑0 : α → F') μ
Tactic: simp only [condExpL1, setToFun, hF', ↓reduceDIte, ZeroMemClass.coe_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1 (goal)
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 μ)
⊢ AEStronglyMeasurable.{u_1, u_3} (β := F') (↑0 : α → F') μ
have neg : EventuallyEq.{u_1, u_3} (β := F') (ae μ) 0 (↑0 : α → F')
Tactic: apply stronglyMeasurable_zero.aestronglyMeasurable.congr
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1 (goal)
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 μ)
⊢ AEStronglyMeasurable (↑(↑(condExpL1 hm μ f) : α →ₘ[μ] F') : α → F') μ
have pos : ∀ (hf : Integrable f μ), AEStronglyMeasurable (↑(↑(condExpL1 hm μ f) : α →ₘ[μ] F') : α → F') μ
Tactic: by_cases hf : Integrable f μ
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1 (goal)
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 μ)
pos : ∀ (hf : Integrable f μ), AEStronglyMeasurable (↑(↑(condExpL1 hm μ f) : α →ₘ[μ] F') : α → F') μ
⊢ AEStronglyMeasurable (↑(↑(condExpL1 hm μ f) : α →ₘ[μ] F') : α → F') μ
have neg : ∀ (hf : ¬Integrable f μ), AEStronglyMeasurable (↑(↑(condExpL1 hm μ f) : α →ₘ[μ] F') : α → F') μ
Tactic: by_cases hf : Integrable f μ
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1 (goal)
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 μ
⊢ AEStronglyMeasurable (↑(↑(condExpL1 hm μ f) : α →ₘ[μ] F') : α → F') μ
have neg : AEStronglyMeasurable.{u_1, u_3} (β := F') (↑(↑0 : α →ₘ[μ] F') : α → F') μ
Tactic: rw [condExpL1_undef hf]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1 (goal)
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 μ
⊢ AEStronglyMeasurable (↑(↑(condExpL1 hm μ f) : α →ₘ[μ] F') : α → F') μ
have pos : ∀ (hf' : f =ᶠ[ae μ] 0), AEStronglyMeasurable (↑(↑(condExpL1 hm μ f) : α →ₘ[μ] F') : α → F') μ
Tactic: by_cases hf' : f =ᵐ[μ] 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1 (goal)
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 μ
pos : ∀ (hf' : f =ᶠ[ae μ] 0), AEStronglyMeasurable (↑(↑(condExpL1 hm μ f) : α →ₘ[μ] F') : α → F') μ
⊢ AEStronglyMeasurable (↑(↑(condExpL1 hm μ f) : α →ₘ[μ] F') : α → F') μ
have neg : ∀ (hf' : ¬f =ᶠ[ae μ] 0), AEStronglyMeasurable (↑(↑(condExpL1 hm μ f) : α →ₘ[μ] F') : α → F') μ
Tactic: by_cases hf' : f =ᵐ[μ] 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1 (goal)
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
⊢ AEStronglyMeasurable (↑(↑(condExpL1 hm μ f) : α →ₘ[μ] F') : α → F') μ
have pos : 0 =ᶠ[ae μ] (↑(↑(condExpL1 hm μ f) : α →ₘ[μ] F') : α → F')
Tactic: apply stronglyMeasurable_zero.aestronglyMeasurable.congr
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1 (goal)
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
⊢ 0 =ᶠ[ae μ] (↑(↑(condExpL1 hm μ f) : α →ₘ[μ] F') : α → F')
have pos : EventuallyEq.{u_1, u_3} (β := F') (ae μ) 0 (↑0 : α → F')
Tactic: simp only [condExpL1_congr_ae hm hf', condExpL1_zero, ZeroMemClass.coe_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1 (goal)
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 μ)
have apply : Integrable.toL1 f hf ≠ 0
Tactic: apply nontrivial_of_ne (hf.toL1 f) 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1 (hypothesis)
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'
have this : 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'
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1 (hypothesis)
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
⊢ AEStronglyMeasurable (↑(↑(condExpL1 hm μ f) : α →ₘ[μ] F') : α → F') μ
have this : 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 μ
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1 (goal)
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 (↑(↑(condExpL1 hm μ f) : α →ₘ[μ] F') : α → F') μ
have neg : AEStronglyMeasurable.{u_1, u_3} (β := F')
  (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) (Integrable.toL1 f hf)) : α →ₘ[μ] F') : α → F') μ
Tactic: rw [condExpL1_eq hf]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1 (goal)
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, (↑(↑(condExpL1 hm μ f) : α →ₘ[μ] F') : α → F') x ∂μ) (∫ (x : α) in s, f x ∂μ)
have 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 ∂μ)
Tactic: simp_rw [condExpL1_eq hf]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1 (goal)
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,
      (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) (Integrable.toL1 f hf)) : α →ₘ[μ] F') : α → F')
        x ∂μ)
    (∫ (x : α) in s, f x ∂μ)
have rw : Eq.{u_3 + 1} (α := F') (∫ (x : α) in s, (↑(↑(Integrable.toL1 f hf) : α →ₘ[μ] F') : α → F') x ∂μ)
  (∫ (x : α) in s, f x ∂μ)
Tactic: rw [setIntegral_condExpL1CLM (hf.toL1 f) hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1 (goal)
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)
have 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 μ))
Tactic: refine setToFun_smul _ ?_ c f
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1 (goal)
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 μ
⊢ (↑(↑(condExpL1 hm μ f) : α →ₘ[μ] F') : α → F') =ᶠ[ae μ] f
have rw : (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) (Integrable.toL1 f hfi)) : α →ₘ[μ] F') :
    α → F') =ᶠ[ae μ]
  f
Tactic: rw [condExpL1_eq hfi]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1 (goal)
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
have refine : (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) (Integrable.toL1 f hfi)) : α →ₘ[μ] F') :
    α → F') =ᶠ[ae μ]
  (↑(↑(Integrable.toL1 f hfi) : α →ₘ[μ] F') : α → F')
Tactic: refine EventuallyEq.trans ?_ (Integrable.coeFn_toL1 hfi)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1 (goal)
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 μ]
    (↑(↑(Integrable.toL1 f hfi) : α →ₘ[μ] F') : α → F')
have hfm₁ : AEStronglyMeasurable (↑(↑(Integrable.toL1 f hfi) : α →ₘ[μ] F') : α → F') μ
Tactic: rw [condExpL1CLM_of_aestronglyMeasurable']
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1 (goal)
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
⊢ (↑(↑(condExpL1 hm μ f) : α →ₘ[μ] E) : α → E) ≤ᶠ[ae μ] (↑(↑(condExpL1 hm μ g) : α →ₘ[μ] E) : α → E)
have rw : LE.le (α := ↥(Lp E 1 μ)) (condExpL1 hm μ f) (condExpL1 hm μ g)
Tactic: rw [coeFn_le]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1 (hypothesis)
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
⊢ LE.le (α := ↥(Lp E 1 μ)) (condExpL1 hm μ f) (condExpL1 hm μ g)
have 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 μ))
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
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2 (goal)
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 μ)
⊢ eLpNorm.{u_1, u_2} (ε := E)
      (↑(↑(↑((condExpL2 E 𝕜 hm : (a : ↥(Lp E 2 μ)) → ↥(lpMeas E 𝕜 m 2 μ)) f) : ↥(Lp E 2 μ)) : α →ₘ[μ] E) : α → E) 2 μ ≤
    eLpNorm (↑(↑f : α →ₘ[μ] E) : α → E) 2 μ
have rw : norm (E := ↥(lpMeas E 𝕜 m 2 μ)) ((condExpL2 E 𝕜 hm : (a : ↥(Lp E 2 μ)) → ↥(lpMeas E 𝕜 m 2 μ)) f : ↥(lpMeas E 𝕜 m 2 μ)) ≤
  ‖f‖
Tactic: rw [← ENNReal.toReal_le_toReal (Lp.eLpNorm_ne_top _) (Lp.eLpNorm_ne_top _), ←
    Lp.norm_def, ← Lp.norm_def, Submodule.norm_coe]