awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Unique (goal)
Goal:
α : Type u_1
E' : Type u_2
𝕜 : Type u_4
p : ℝ≥0∞
m m0 : MeasurableSpace α
μ : Measure α
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E'
inst_2 : InnerProductSpace 𝕜 E'
inst_3 : CompleteSpace E'
inst_4 : NormedSpace ℝ E'
hm : m ≤ m0
f : ↥(lpMeas E' 𝕜 m p μ)
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
hf_int_finite :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        IntegrableOn (↑(↑(↑f : ↥(Lp E' p μ)) : α →ₘ[μ] E') : α → E') s μ
hf_zero :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        Eq.{u_2 + 1} (α := E') (∫ (x : α) in s, (↑(↑(↑f : ↥(Lp E' p μ)) : α →ₘ[μ] E') : α → E') x ∂μ) 0
g : α → E'
hg_sm : FinStronglyMeasurable g (μ.trim hm)
hfg : (↑(↑(↑f : ↥(Lp E' p μ)) : α →ₘ[μ] E') : α → E') =ᶠ[ae μ] g
s : Set α
hs : MeasurableSet s
hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hfg_restrict : (↑(↑(↑f : ↥(Lp E' p μ)) : α →ₘ[μ] E') : α → E') =ᶠ[ae (μ.restrict s)] g
⊢ IntegrableOn g s μ
have refine_1 : Integrable (↑(↑(↑f : ↥(Lp E' p μ)) : α →ₘ[μ] E') : α → E') (μ.restrict s)
Tactic: rw [IntegrableOn, integrable_congr hfg_restrict.symm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Unique (hypothesis)
Goal:
α : Type u_1
E' : Type u_2
𝕜 : Type u_4
p : ℝ≥0∞
m m0 : MeasurableSpace α
μ : Measure α
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E'
inst_2 : InnerProductSpace 𝕜 E'
inst_3 : CompleteSpace E'
inst_4 : NormedSpace ℝ E'
hm : m ≤ m0
f : ↥(lpMeas E' 𝕜 m p μ)
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
hf_int_finite :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        IntegrableOn (↑(↑(↑f : ↥(Lp E' p μ)) : α →ₘ[μ] E') : α → E') s μ
hf_zero :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        Eq.{u_2 + 1} (α := E') (∫ (x : α) in s, (↑(↑(↑f : ↥(Lp E' p μ)) : α →ₘ[μ] E') : α → E') x ∂μ) 0
g : α → E'
hg_sm : FinStronglyMeasurable g (μ.trim hm)
hfg : (↑(↑(↑f : ↥(Lp E' p μ)) : α →ₘ[μ] E') : α → E') =ᶠ[ae μ] g
s : Set α
hs : MeasurableSet s
hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Eq.{u_2 + 1} (α := E') (∫ (x : α) in s, g x ∂μ) 0
have hfg_restrict : (↑(↑(↑f : ↥(Lp E' p μ)) : α →ₘ[μ] E') : α → E') =ᶠ[ae (μ.restrict s)] g
Tactic: have hfg_restrict : f =ᵐ[μ.restrict s] g := ae_restrict_of_ae hfg
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Unique (goal)
Goal:
α : Type u_1
E' : Type u_2
𝕜 : Type u_4
p : ℝ≥0∞
m m0 : MeasurableSpace α
μ : Measure α
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E'
inst_2 : InnerProductSpace 𝕜 E'
inst_3 : CompleteSpace E'
inst_4 : NormedSpace ℝ E'
hm : m ≤ m0
f : ↥(lpMeas E' 𝕜 m p μ)
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
hf_int_finite :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        IntegrableOn (↑(↑(↑f : ↥(Lp E' p μ)) : α →ₘ[μ] E') : α → E') s μ
hf_zero :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        Eq.{u_2 + 1} (α := E') (∫ (x : α) in s, (↑(↑(↑f : ↥(Lp E' p μ)) : α →ₘ[μ] E') : α → E') x ∂μ) 0
g : α → E'
hg_sm : FinStronglyMeasurable g (μ.trim hm)
hfg : (↑(↑(↑f : ↥(Lp E' p μ)) : α →ₘ[μ] E') : α → E') =ᶠ[ae μ] g
s : Set α
hs : MeasurableSet s
hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hfg_restrict : (↑(↑(↑f : ↥(Lp E' p μ)) : α →ₘ[μ] E') : α → E') =ᶠ[ae (μ.restrict s)] g
⊢ Eq.{u_2 + 1} (α := E') (∫ (x : α) in s, g x ∂μ) 0
have refine_2 : Eq.{u_2 + 1} (α := E') (∫ (a : α) in s, (↑(↑(↑f : ↥(Lp E' p μ)) : α →ₘ[μ] E') : α → E') a ∂μ) 0
Tactic: rw [integral_congr_ae hfg_restrict.symm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Unique (hypothesis)
Goal:
α : Type u_1
E' : Type u_2
𝕜 : Type u_4
p : ℝ≥0∞
m m0 : MeasurableSpace α
μ : Measure α
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E'
inst_2 : InnerProductSpace 𝕜 E'
inst_3 : CompleteSpace E'
inst_4 : NormedSpace ℝ E'
hm : m ≤ m0
f : ↥(Lp E' p μ)
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
hf_int_finite :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn (↑(↑f : α →ₘ[μ] E') : α → E') s μ
hf_zero :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        Eq.{u_2 + 1} (α := E') (∫ (x : α) in s, (↑(↑f : α →ₘ[μ] E') : α → E') x ∂μ) 0
hf_meas : AEStronglyMeasurable (↑(↑f : α →ₘ[μ] E') : α → E') μ
f_meas : ↥(lpMeas E' 𝕜 m p μ) :=
  Subtype.mk (p := fun (x : ↥(Lp E' p μ)) ↦ Membership.mem (γ := Submodule 𝕜 ↥(Lp E' p μ)) (lpMeas E' 𝕜 m p μ) x) f
    hf_meas
⊢ (↑(↑f : α →ₘ[μ] E') : α → E') =ᶠ[ae μ] 0
have hf_f_meas : (↑(↑f : α →ₘ[μ] E') : α → E') =ᶠ[ae μ] (↑(↑(↑f_meas : ↥(Lp E' p μ)) : α →ₘ[μ] E') : α → E')
Tactic: have hf_f_meas : f =ᵐ[μ] f_meas := by simp [f_meas]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Unique (goal)
Goal:
α : Type u_1
E' : Type u_2
𝕜 : Type u_4
p : ℝ≥0∞
m m0 : MeasurableSpace α
μ : Measure α
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E'
inst_2 : InnerProductSpace 𝕜 E'
inst_3 : CompleteSpace E'
inst_4 : NormedSpace ℝ E'
hm : m ≤ m0
f : ↥(Lp E' p μ)
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
hf_int_finite :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn (↑(↑f : α →ₘ[μ] E') : α → E') s μ
hf_zero :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        Eq.{u_2 + 1} (α := E') (∫ (x : α) in s, (↑(↑f : α →ₘ[μ] E') : α → E') x ∂μ) 0
hf_meas : AEStronglyMeasurable (↑(↑f : α →ₘ[μ] E') : α → E') μ
f_meas : ↥(lpMeas E' 𝕜 m p μ) :=
  Subtype.mk (p := fun (x : ↥(Lp E' p μ)) ↦ Membership.mem (γ := Submodule 𝕜 ↥(Lp E' p μ)) (lpMeas E' 𝕜 m p μ) x) f
    hf_meas
hf_f_meas : (↑(↑f : α →ₘ[μ] E') : α → E') =ᶠ[ae μ] (↑(↑(↑f_meas : ↥(Lp E' p μ)) : α →ₘ[μ] E') : α → E')
⊢ (↑(↑f : α →ₘ[μ] E') : α → E') =ᶠ[ae μ] 0
have refine : (↑(↑(↑f_meas : ↥(Lp E' p μ)) : α →ₘ[μ] E') : α → E') =ᶠ[ae μ] 0
Tactic: refine hf_f_meas.trans ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Unique (goal)
Goal:
α : Type u_1
E' : Type u_2
𝕜 : Type u_4
p : ℝ≥0∞
m m0 : MeasurableSpace α
μ : Measure α
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E'
inst_2 : InnerProductSpace 𝕜 E'
inst_3 : CompleteSpace E'
inst_4 : 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 →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn (↑(↑f : α →ₘ[μ] E') : α → E') s μ
hg_int_finite :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn (↑(↑g : α →ₘ[μ] E') : α → E') s μ
hfg :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        Eq.{u_2 + 1} (α := E') (∫ (x : α) in s, (↑(↑f : α →ₘ[μ] E') : α → E') x ∂μ)
          (∫ (x : α) in s, (↑(↑g : α →ₘ[μ] E') : α → E') x ∂μ)
hf_meas : AEStronglyMeasurable (↑(↑f : α →ₘ[μ] E') : α → E') μ
hg_meas : AEStronglyMeasurable (↑(↑g : α →ₘ[μ] E') : α → E') μ
h_sub : (↑(↑(f - g) : α →ₘ[μ] E') : α → E') =ᶠ[ae μ] 0
⊢ (↑(↑f : α →ₘ[μ] E') : α → E') =ᶠ[ae μ] (↑(↑g : α →ₘ[μ] E') : α → E')
have rw : (↑(↑f : α →ₘ[μ] E') : α → E') - (↑(↑g : α →ₘ[μ] E') : α → E') =ᶠ[ae μ] 0
Tactic: rw [← sub_ae_eq_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Unique (goal)
Goal:
α : Type u_1
E' : Type u_2
𝕜 : Type u_4
p : ℝ≥0∞
m m0 : MeasurableSpace α
μ : Measure α
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E'
inst_2 : InnerProductSpace 𝕜 E'
inst_3 : CompleteSpace E'
inst_4 : 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 →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn (↑(↑f : α →ₘ[μ] E') : α → E') s μ
hg_int_finite :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn (↑(↑g : α →ₘ[μ] E') : α → E') s μ
hfg :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        Eq.{u_2 + 1} (α := E') (∫ (x : α) in s, (↑(↑f : α →ₘ[μ] E') : α → E') x ∂μ)
          (∫ (x : α) in s, (↑(↑g : α →ₘ[μ] E') : α → E') x ∂μ)
hf_meas : AEStronglyMeasurable (↑(↑f : α →ₘ[μ] E') : α → E') μ
hg_meas : AEStronglyMeasurable (↑(↑g : α →ₘ[μ] E') : α → E') μ
⊢ (↑(↑f : α →ₘ[μ] E') : α → E') =ᶠ[ae μ] (↑(↑g : α →ₘ[μ] E') : α → E')
have suffices : (↑(↑(f - g) : α →ₘ[μ] E') : α → E') =ᶠ[ae μ] 0
Tactic: suffices h_sub : ⇑(f - g) =ᵐ[μ] 0 by
    rw [← sub_ae_eq_zero]; exact (Lp.coeFn_sub f g).symm.trans h_sub
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Unique (goal)
Goal:
α : Type u_1
E' : Type u_2
𝕜 : Type u_4
p : ℝ≥0∞
m m0 : MeasurableSpace α
μ : Measure α
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E'
inst_2 : InnerProductSpace 𝕜 E'
inst_3 : CompleteSpace E'
inst_4 : 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 →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn (↑(↑f : α →ₘ[μ] E') : α → E') s μ
hg_int_finite :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn (↑(↑g : α →ₘ[μ] E') : α → E') s μ
hfg :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        Eq.{u_2 + 1} (α := E') (∫ (x : α) in s, (↑(↑f : α →ₘ[μ] E') : α → E') x ∂μ)
          (∫ (x : α) in s, (↑(↑g : α →ₘ[μ] E') : α → E') x ∂μ)
hf_meas : AEStronglyMeasurable (↑(↑f : α →ₘ[μ] E') : α → E') μ
hg_meas : AEStronglyMeasurable (↑(↑g : α →ₘ[μ] E') : α → E') μ
s : Set α
hs : MeasurableSet s
hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Eq.{u_2 + 1} (α := E') (∫ (x : α) in s, (↑(↑(f - g) : α →ₘ[μ] E') : α → E') x ∂μ) 0
have rw : Eq.{u_2 + 1} (α := E') (∫ (a : α) in s, ((↑(↑f : α →ₘ[μ] E') : α → E') - (↑(↑g : α →ₘ[μ] E') : α → E')) a ∂μ) 0
Tactic: rw [integral_congr_ae (ae_restrict_of_ae (Lp.coeFn_sub f g))]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Unique (goal)
Goal:
α : Type u_1
E' : Type u_2
𝕜 : Type u_4
p : ℝ≥0∞
m m0 : MeasurableSpace α
μ : Measure α
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E'
inst_2 : InnerProductSpace 𝕜 E'
inst_3 : CompleteSpace E'
inst_4 : 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 →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn (↑(↑f : α →ₘ[μ] E') : α → E') s μ
hg_int_finite :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn (↑(↑g : α →ₘ[μ] E') : α → E') s μ
hfg :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        Eq.{u_2 + 1} (α := E') (∫ (x : α) in s, (↑(↑f : α →ₘ[μ] E') : α → E') x ∂μ)
          (∫ (x : α) in s, (↑(↑g : α →ₘ[μ] E') : α → E') x ∂μ)
hf_meas : AEStronglyMeasurable (↑(↑f : α →ₘ[μ] E') : α → E') μ
hg_meas : AEStronglyMeasurable (↑(↑g : α →ₘ[μ] E') : α → E') μ
s : Set α
hs : MeasurableSet s
hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Eq.{u_2 + 1} (α := E') (∫ (a : α) in s, ((↑(↑f : α →ₘ[μ] E') : α → E') - (↑(↑g : α →ₘ[μ] E') : α → E')) a ∂μ) 0
have rw : HSub.hSub (α := E') (∫ (a : α) in s, (↑(↑f : α →ₘ[μ] E') : α → E') a ∂μ)
    (∫ (a : α) in s, (↑(↑g : α →ₘ[μ] E') : α → E') a ∂μ) =
  0
Tactic: rw [integral_sub' (hf_int_finite s hs hμs) (hg_int_finite s hs hμs)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Unique (hypothesis)
Goal:
α : Type u_1
E' : Type u_2
𝕜 : Type u_4
p : ℝ≥0∞
m m0 : MeasurableSpace α
μ : Measure α
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E'
inst_2 : InnerProductSpace 𝕜 E'
inst_3 : CompleteSpace E'
inst_4 : 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 →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn (↑(↑f : α →ₘ[μ] E') : α → E') s μ
hg_int_finite :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn (↑(↑g : α →ₘ[μ] E') : α → E') s μ
hfg :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        Eq.{u_2 + 1} (α := E') (∫ (x : α) in s, (↑(↑f : α →ₘ[μ] E') : α → E') x ∂μ)
          (∫ (x : α) in s, (↑(↑g : α →ₘ[μ] E') : α → E') x ∂μ)
hf_meas : AEStronglyMeasurable (↑(↑f : α →ₘ[μ] E') : α → E') μ
hg_meas : AEStronglyMeasurable (↑(↑g : α →ₘ[μ] E') : α → E') μ
⊢ (↑(↑(f - g) : α →ₘ[μ] E') : α → E') =ᶠ[ae μ] 0
have hfg' : ∀ (s : Set α),
  MeasurableSet s →
    LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
      Eq.{u_2 + 1} (α := E') (∫ (x : α) in s, (↑(↑(f - g) : α →ₘ[μ] E') : α → E') x ∂μ) 0
Tactic: have hfg' : ∀ s : Set α, MeasurableSet[m] s → μ s < ∞ → (∫ x in s, (f - g) x ∂μ) = 0 := by
    intro s hs hμs
    rw [integral_congr_ae (ae_restrict_of_ae (Lp.coeFn_sub f g))]
    rw [integral_sub' (hf_int_finite s hs hμs) (hg_int_finite s hs hμs)]
    exact sub_eq_zero.mpr (hfg s hs hμs)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Unique (goal)
Goal:
α : Type u_1
E' : Type u_2
𝕜 : Type u_4
p : ℝ≥0∞
m m0 : MeasurableSpace α
μ : Measure α
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E'
inst_2 : InnerProductSpace 𝕜 E'
inst_3 : CompleteSpace E'
inst_4 : 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 →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn (↑(↑f : α →ₘ[μ] E') : α → E') s μ
hg_int_finite :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn (↑(↑g : α →ₘ[μ] E') : α → E') s μ
hfg :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        Eq.{u_2 + 1} (α := E') (∫ (x : α) in s, (↑(↑f : α →ₘ[μ] E') : α → E') x ∂μ)
          (∫ (x : α) in s, (↑(↑g : α →ₘ[μ] E') : α → E') x ∂μ)
hf_meas : AEStronglyMeasurable (↑(↑f : α →ₘ[μ] E') : α → E') μ
hg_meas : AEStronglyMeasurable (↑(↑g : α →ₘ[μ] E') : α → E') μ
hfg' :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        Eq.{u_2 + 1} (α := E') (∫ (x : α) in s, (↑(↑(f - g) : α →ₘ[μ] E') : α → E') x ∂μ) 0
s : Set α
hs : MeasurableSet s
hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ IntegrableOn (↑(↑(f - g) : α →ₘ[μ] E') : α → E') s μ
have rw : Integrable ((↑(↑f : α →ₘ[μ] E') : α → E') - (↑(↑g : α →ₘ[μ] E') : α → E')) (μ.restrict s)
Tactic: rw [IntegrableOn, integrable_congr (ae_restrict_of_ae (Lp.coeFn_sub f g))]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Unique (hypothesis)
Goal:
α : Type u_1
E' : Type u_2
𝕜 : Type u_4
p : ℝ≥0∞
m m0 : MeasurableSpace α
μ : Measure α
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E'
inst_2 : InnerProductSpace 𝕜 E'
inst_3 : CompleteSpace E'
inst_4 : 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 →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn (↑(↑f : α →ₘ[μ] E') : α → E') s μ
hg_int_finite :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn (↑(↑g : α →ₘ[μ] E') : α → E') s μ
hfg :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        Eq.{u_2 + 1} (α := E') (∫ (x : α) in s, (↑(↑f : α →ₘ[μ] E') : α → E') x ∂μ)
          (∫ (x : α) in s, (↑(↑g : α →ₘ[μ] E') : α → E') x ∂μ)
hf_meas : AEStronglyMeasurable (↑(↑f : α →ₘ[μ] E') : α → E') μ
hg_meas : AEStronglyMeasurable (↑(↑g : α →ₘ[μ] E') : α → E') μ
hfg' :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        Eq.{u_2 + 1} (α := E') (∫ (x : α) in s, (↑(↑(f - g) : α →ₘ[μ] E') : α → E') x ∂μ) 0
⊢ (↑(↑(f - g) : α →ₘ[μ] E') : α → E') =ᶠ[ae μ] 0
have hfg_int : ∀ (s : Set α),
  MeasurableSet s →
    LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
      IntegrableOn (↑(↑(f - g) : α →ₘ[μ] E') : α → E') s μ
Tactic: have hfg_int : ∀ s, MeasurableSet[m] s → μ s < ∞ → IntegrableOn (⇑(f - g)) s μ := by
    intro s hs hμs
    rw [IntegrableOn, integrable_congr (ae_restrict_of_ae (Lp.coeFn_sub f g))]
    exact (hf_int_finite s hs hμs).sub (hg_int_finite s hs hμs)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Unique (goal)
Goal:
α : Type u_1
F' : Type u_3
m m0 : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup F'
inst_1 : NormedSpace ℝ F'
inst_2 : CompleteSpace F'
hm : m ≤ m0
inst_3 : SigmaFinite (μ.trim hm)
f g : α → F'
hf_int_finite :
  ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn f s μ
hg_int_finite :
  ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn g s μ
hfg_eq :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        Eq.{u_3 + 1} (α := F') (∫ (x : α) in s, f x ∂μ) (∫ (x : α) in s, g x ∂μ)
hfm : AEStronglyMeasurable f μ
hgm : AEStronglyMeasurable g μ
⊢ f =ᶠ[ae μ] g
have rw : AEStronglyMeasurable.mk f hfm =ᶠ[ae (μ.trim hm)] AEStronglyMeasurable.mk g hgm
Tactic: rw [← ae_eq_trim_iff_of_aestronglyMeasurable hm hfm hgm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Unique (hypothesis)
Goal:
α : Type u_1
F' : Type u_3
m m0 : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup F'
inst_1 : NormedSpace ℝ F'
inst_2 : CompleteSpace F'
hm : m ≤ m0
inst_3 : SigmaFinite (μ.trim hm)
f g : α → F'
hf_int_finite :
  ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn f s μ
hg_int_finite :
  ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn g s μ
hfg_eq :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        Eq.{u_3 + 1} (α := F') (∫ (x : α) in s, f x ∂μ) (∫ (x : α) in s, g x ∂μ)
hfm : AEStronglyMeasurable f μ
hgm : AEStronglyMeasurable g μ
s : Set α
hs : MeasurableSet s
hμs : LT.lt (α := ℝ≥0∞) ((μ.trim hm : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ IntegrableOn (AEStronglyMeasurable.mk f hfm) s (μ.trim hm)
have hμs₁ : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: rw [trim_measurableSet_eq hm hs] at hμs
Cleared hypotheses: hμs
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Unique (goal)
Goal:
α : Type u_1
F' : Type u_3
m m0 : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup F'
inst_1 : NormedSpace ℝ F'
inst_2 : CompleteSpace F'
hm : m ≤ m0
inst_3 : SigmaFinite (μ.trim hm)
f g : α → F'
hf_int_finite :
  ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn f s μ
hg_int_finite :
  ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn g s μ
hfg_eq :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        Eq.{u_3 + 1} (α := F') (∫ (x : α) in s, f x ∂μ) (∫ (x : α) in s, g x ∂μ)
hfm : AEStronglyMeasurable f μ
hgm : AEStronglyMeasurable g μ
s : Set α
hs : MeasurableSet s
hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ IntegrableOn (AEStronglyMeasurable.mk f hfm) s (μ.trim hm)
have rw : Integrable (AEStronglyMeasurable.mk f hfm) ((μ.restrict s).trim hm)
Tactic: rw [IntegrableOn, restrict_trim hm _ hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Unique (goal)
Goal:
α : Type u_1
F' : Type u_3
m m0 : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup F'
inst_1 : NormedSpace ℝ F'
inst_2 : CompleteSpace F'
hm : m ≤ m0
inst_3 : SigmaFinite (μ.trim hm)
f g : α → F'
hf_int_finite :
  ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn f s μ
hg_int_finite :
  ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn g s μ
hfg_eq :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        Eq.{u_3 + 1} (α := F') (∫ (x : α) in s, f x ∂μ) (∫ (x : α) in s, g x ∂μ)
hfm : AEStronglyMeasurable f μ
hgm : AEStronglyMeasurable g μ
s : Set α
hs : MeasurableSet s
hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Integrable (AEStronglyMeasurable.mk f hfm) ((μ.restrict s).trim hm)
have refine : Integrable (AEStronglyMeasurable.mk f hfm) (μ.restrict s)
Tactic: refine Integrable.trim hm ?_ hfm.stronglyMeasurable_mk
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Unique (hypothesis)
Goal:
α : Type u_1
F' : Type u_3
m m0 : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup F'
inst_1 : NormedSpace ℝ F'
inst_2 : CompleteSpace F'
hm : m ≤ m0
inst_3 : SigmaFinite (μ.trim hm)
f g : α → F'
hf_int_finite :
  ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn f s μ
hg_int_finite :
  ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn g s μ
hfg_eq :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        Eq.{u_3 + 1} (α := F') (∫ (x : α) in s, f x ∂μ) (∫ (x : α) in s, g x ∂μ)
hfm : AEStronglyMeasurable f μ
hgm : AEStronglyMeasurable g μ
⊢ AEStronglyMeasurable.mk f hfm =ᶠ[ae (μ.trim hm)] AEStronglyMeasurable.mk g hgm
have hf_mk_int_finite : ∀ (s : Set α),
  MeasurableSet s →
    LT.lt (α := ℝ≥0∞) ((μ.trim hm : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
      IntegrableOn (AEStronglyMeasurable.mk f hfm) s (μ.trim hm)
Tactic: have hf_mk_int_finite (s) :
      MeasurableSet[m] s → μ.trim hm s < ∞ → @IntegrableOn _ _ m _ _ (hfm.mk f) s (μ.trim hm) := by
    intro hs hμs
    rw [trim_measurableSet_eq hm hs] at hμs
    rw [IntegrableOn, restrict_trim hm _ hs]
    refine Integrable.trim hm ?_ hfm.stronglyMeasurable_mk
    exact Integrable.congr (hf_int_finite s hs hμs) (ae_restrict_of_ae hfm.ae_eq_mk)