awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable (goal)
Goal:
α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst : NormedAddCommGroup F
m m0 : MeasurableSpace α
μ : Measure α
inst_1 : Fact (1 ≤ p)
inst_2 : NormedSpace ℝ F
hm : m ≤ m0
hp_ne_top : p ≠ ∞
P : ↥(Lp F p μ) → Prop
h_ind :
  ∀ (c : F) {s : Set α} (hs : MeasurableSet s) (hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
    P (↑(simpleFunc.indicatorConst p (s := s) ⋯ ⋯ c) : ↥(Lp F p μ))
h_add :
  ∀ ⦃f g : α → F⦄ (hf : MemLp f p μ) (hg : MemLp g p μ),
    AEStronglyMeasurable f μ →
      AEStronglyMeasurable g μ →
        Disjoint (Function.support f) (Function.support g) →
          P (MemLp.toLp f hf) → P (MemLp.toLp g hg) → P (MemLp.toLp f hf + MemLp.toLp g hg)
h_closed : IsClosed (X := ↥(lpMeas F ℝ m p μ)) {f : ↥(lpMeas F ℝ m p μ) | P (↑f : ↥(Lp F p μ))}
f_1 : ↥(Lp F p μ)
hf_1 : AEStronglyMeasurable (↑(↑f_1 : α →ₘ[μ] F) : α → F) μ
f' : ↥(lpMeas F ℝ m p μ) :=
  Subtype.mk (p := fun (x : ↥(Lp F p μ)) ↦ Membership.mem (γ := Submodule ℝ ↥(Lp F p μ)) (lpMeas F ℝ m p μ) x) f_1 hf_1
g_1 : ↥(Lp F p (μ.trim hm)) := (lpMeasToLpTrimLie F ℝ p μ hm : (a : ↥(lpMeas F ℝ m p μ)) → ↥(Lp F p (μ.trim hm))) f'
hfg :
  f' = (LinearIsometryEquiv.symm (lpMeasToLpTrimLie F ℝ p μ hm) : (a : ↥(Lp F p (μ.trim hm))) → ↥(lpMeas F ℝ m p μ)) g_1
f g : α → F
hf : MemLp f p (μ.trim hm)
hg : MemLp g p (μ.trim hm)
h_disj : Disjoint (Function.support f) (Function.support g)
hfP :
  P
    (↑((LinearIsometryEquiv.symm (lpMeasToLpTrimLie F ℝ p μ hm) : (a : ↥(Lp F p (μ.trim hm))) → ↥(lpMeas F ℝ m p μ))
          (MemLp.toLp f hf)) :
      ↥(Lp F p μ))
hgP :
  P
    (↑((LinearIsometryEquiv.symm (lpMeasToLpTrimLie F ℝ p μ hm) : (a : ↥(Lp F p (μ.trim hm))) → ↥(lpMeas F ℝ m p μ))
          (MemLp.toLp g hg)) :
      ↥(Lp F p μ))
⊢ P
    (↑((LinearIsometryEquiv.symm (lpMeasToLpTrimLie F ℝ p μ hm) : (a : ↥(Lp F p (μ.trim hm))) → ↥(lpMeas F ℝ m p μ))
          (MemLp.toLp f hf + MemLp.toLp g hg)) :
      ↥(Lp F p μ))
have refine_2 : P
  (↑(HAdd.hAdd (α := ↥(lpMeas F ℝ m p μ)) (β := ↥(lpMeas F ℝ m p μ))
        ((LinearIsometryEquiv.symm (lpMeasToLpTrimLie F ℝ p μ hm) : (a : ↥(Lp F p (μ.trim hm))) → ↥(lpMeas F ℝ m p μ))
            (MemLp.toLp f hf) :
          ↥(lpMeas F ℝ m p μ))
        ((LinearIsometryEquiv.symm (lpMeasToLpTrimLie F ℝ p μ hm) : (a : ↥(Lp F p (μ.trim hm))) → ↥(lpMeas F ℝ m p μ))
            (MemLp.toLp g hg) :
          ↥(lpMeas F ℝ m p μ))) :
    ↥(Lp F p μ))
Tactic: rw [LinearIsometryEquiv.map_add]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable (goal)
Goal:
α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst : NormedAddCommGroup F
m m0 : MeasurableSpace α
μ : Measure α
inst_1 : Fact (1 ≤ p)
inst_2 : NormedSpace ℝ F
hm : m ≤ m0
hp_ne_top : p ≠ ∞
P : ↥(Lp F p μ) → Prop
h_ind :
  ∀ (c : F) {s : Set α} (hs : MeasurableSet s) (hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
    P (↑(simpleFunc.indicatorConst p (s := s) ⋯ ⋯ c) : ↥(Lp F p μ))
h_add :
  ∀ ⦃f g : α → F⦄ (hf : MemLp f p μ) (hg : MemLp g p μ),
    AEStronglyMeasurable f μ →
      AEStronglyMeasurable g μ →
        Disjoint (Function.support f) (Function.support g) →
          P (MemLp.toLp f hf) → P (MemLp.toLp g hg) → P (MemLp.toLp f hf + MemLp.toLp g hg)
h_closed : IsClosed (X := ↥(lpMeas F ℝ m p μ)) {f : ↥(lpMeas F ℝ m p μ) | P (↑f : ↥(Lp F p μ))}
f_1 : ↥(Lp F p μ)
hf_1 : AEStronglyMeasurable (↑(↑f_1 : α →ₘ[μ] F) : α → F) μ
f' : ↥(lpMeas F ℝ m p μ) :=
  Subtype.mk (p := fun (x : ↥(Lp F p μ)) ↦ Membership.mem (γ := Submodule ℝ ↥(Lp F p μ)) (lpMeas F ℝ m p μ) x) f_1 hf_1
g_1 : ↥(Lp F p (μ.trim hm)) := (lpMeasToLpTrimLie F ℝ p μ hm : (a : ↥(lpMeas F ℝ m p μ)) → ↥(Lp F p (μ.trim hm))) f'
hfg :
  f' = (LinearIsometryEquiv.symm (lpMeasToLpTrimLie F ℝ p μ hm) : (a : ↥(Lp F p (μ.trim hm))) → ↥(lpMeas F ℝ m p μ)) g_1
f g : α → F
hf : MemLp f p (μ.trim hm)
hg : MemLp g p (μ.trim hm)
h_disj : Disjoint (Function.support f) (Function.support g)
hfP :
  P
    (↑((LinearIsometryEquiv.symm (lpMeasToLpTrimLie F ℝ p μ hm) : (a : ↥(Lp F p (μ.trim hm))) → ↥(lpMeas F ℝ m p μ))
          (MemLp.toLp f hf)) :
      ↥(Lp F p μ))
hgP :
  P
    (↑((LinearIsometryEquiv.symm (lpMeasToLpTrimLie F ℝ p μ hm) : (a : ↥(Lp F p (μ.trim hm))) → ↥(lpMeas F ℝ m p μ))
          (MemLp.toLp g hg)) :
      ↥(Lp F p μ))
⊢ P
    (↑(HAdd.hAdd (α := ↥(lpMeas F ℝ m p μ)) (β := ↥(lpMeas F ℝ m p μ))
          ((LinearIsometryEquiv.symm (lpMeasToLpTrimLie F ℝ p μ hm) : (a : ↥(Lp F p (μ.trim hm))) → ↥(lpMeas F ℝ m p μ))
              (MemLp.toLp f hf) :
            ↥(lpMeas F ℝ m p μ))
          ((LinearIsometryEquiv.symm (lpMeasToLpTrimLie F ℝ p μ hm) : (a : ↥(Lp F p (μ.trim hm))) → ↥(lpMeas F ℝ m p μ))
              (MemLp.toLp g hg) :
            ↥(lpMeas F ℝ m p μ))) :
      ↥(Lp F p μ))
have refine_2 : P
  (HAdd.hAdd (α := ↥(Lp F p μ))
    (↑((LinearIsometryEquiv.symm (lpMeasToLpTrimLie F ℝ p μ hm) : (a : ↥(Lp F p (μ.trim hm))) → ↥(lpMeas F ℝ m p μ))
          (MemLp.toLp f hf)) :
      ↥(Lp F p μ))
    (↑((LinearIsometryEquiv.symm (lpMeasToLpTrimLie F ℝ p μ hm) : (a : ↥(Lp F p (μ.trim hm))) → ↥(lpMeas F ℝ m p μ))
          (MemLp.toLp g hg)) :
      ↥(Lp F p μ)))
Tactic: push_cast
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable (goal)
Goal:
α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst : NormedAddCommGroup F
m m0 : MeasurableSpace α
μ : Measure α
inst_1 : Fact (1 ≤ p)
inst_2 : NormedSpace ℝ F
hm : m ≤ m0
hp_ne_top : p ≠ ∞
P : ↥(Lp F p μ) → Prop
h_ind :
  ∀ (c : F) {s : Set α} (hs : MeasurableSet s) (hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
    P (↑(simpleFunc.indicatorConst p (s := s) ⋯ ⋯ c) : ↥(Lp F p μ))
h_add :
  ∀ ⦃f g : α → F⦄ (hf : MemLp f p μ) (hg : MemLp g p μ),
    AEStronglyMeasurable f μ →
      AEStronglyMeasurable g μ →
        Disjoint (Function.support f) (Function.support g) →
          P (MemLp.toLp f hf) → P (MemLp.toLp g hg) → P (MemLp.toLp f hf + MemLp.toLp g hg)
h_closed : IsClosed (X := ↥(lpMeas F ℝ m p μ)) {f : ↥(lpMeas F ℝ m p μ) | P (↑f : ↥(Lp F p μ))}
f_1 : ↥(Lp F p μ)
hf_1 : AEStronglyMeasurable (↑(↑f_1 : α →ₘ[μ] F) : α → F) μ
f' : ↥(lpMeas F ℝ m p μ) :=
  Subtype.mk (p := fun (x : ↥(Lp F p μ)) ↦ Membership.mem (γ := Submodule ℝ ↥(Lp F p μ)) (lpMeas F ℝ m p μ) x) f_1 hf_1
g_1 : ↥(Lp F p (μ.trim hm)) := (lpMeasToLpTrimLie F ℝ p μ hm : (a : ↥(lpMeas F ℝ m p μ)) → ↥(Lp F p (μ.trim hm))) f'
hfg :
  f' = (LinearIsometryEquiv.symm (lpMeasToLpTrimLie F ℝ p μ hm) : (a : ↥(Lp F p (μ.trim hm))) → ↥(lpMeas F ℝ m p μ)) g_1
f g : α → F
hf : MemLp f p (μ.trim hm)
hg : MemLp g p (μ.trim hm)
h_disj : Disjoint (Function.support f) (Function.support g)
hfP :
  P
    (↑((LinearIsometryEquiv.symm (lpMeasToLpTrimLie F ℝ p μ hm) : (a : ↥(Lp F p (μ.trim hm))) → ↥(lpMeas F ℝ m p μ))
          (MemLp.toLp f hf)) :
      ↥(Lp F p μ))
hgP :
  P
    (↑((LinearIsometryEquiv.symm (lpMeasToLpTrimLie F ℝ p μ hm) : (a : ↥(Lp F p (μ.trim hm))) → ↥(lpMeas F ℝ m p μ))
          (MemLp.toLp g hg)) :
      ↥(Lp F p μ))
⊢ P
    (HAdd.hAdd (α := ↥(Lp F p μ))
      (↑((LinearIsometryEquiv.symm (lpMeasToLpTrimLie F ℝ p μ hm) : (a : ↥(Lp F p (μ.trim hm))) → ↥(lpMeas F ℝ m p μ))
            (MemLp.toLp f hf)) :
        ↥(Lp F p μ))
      (↑((LinearIsometryEquiv.symm (lpMeasToLpTrimLie F ℝ p μ hm) : (a : ↥(Lp F p (μ.trim hm))) → ↥(lpMeas F ℝ m p μ))
            (MemLp.toLp g hg)) :
        ↥(Lp F p μ)))
have refine_2 : ∀
  (h_eq :
    ∀ (f : α → F) (hf : MemLp f p (μ.trim hm)),
      (↑((LinearIsometryEquiv.symm (lpMeasToLpTrimLie F ℝ p μ hm) : (a : ↥(Lp F p (μ.trim hm))) → ↥(lpMeas F ℝ m p μ))
              (MemLp.toLp f hf)) :
          ↥(Lp F p μ)) =
        MemLp.toLp f sorry),
  P
    (HAdd.hAdd (α := ↥(Lp F p μ))
      (↑((LinearIsometryEquiv.symm (lpMeasToLpTrimLie F ℝ p μ hm) : (a : ↥(Lp F p (μ.trim hm))) → ↥(lpMeas F ℝ m p μ))
            (MemLp.toLp f hf)) :
        ↥(Lp F p μ))
      (↑((LinearIsometryEquiv.symm (lpMeasToLpTrimLie F ℝ p μ hm) : (a : ↥(Lp F p (μ.trim hm))) → ↥(lpMeas F ℝ m p μ))
            (MemLp.toLp g hg)) :
        ↥(Lp F p μ)))
Tactic: have h_eq :
      ∀ (f : α → F) (hf : MemLp f p (μ.trim hm)),
        ((lpMeasToLpTrimLie F ℝ p μ hm).symm (MemLp.toLp f hf) : Lp F p μ) =
          (memLp_of_memLp_trim hm hf).toLp f :=
      lpMeasToLpTrimLie_symm_toLp hm
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable (goal)
Goal:
α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst : NormedAddCommGroup F
m m0 : MeasurableSpace α
μ : Measure α
inst_1 : Fact (1 ≤ p)
inst_2 : NormedSpace ℝ F
hm : m ≤ m0
hp_ne_top : p ≠ ∞
P : ↥(Lp F p μ) → Prop
h_ind :
  ∀ (c : F) {s : Set α} (hs : MeasurableSet s) (hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
    P (↑(simpleFunc.indicatorConst p (s := s) ⋯ ⋯ c) : ↥(Lp F p μ))
h_add :
  ∀ ⦃f g : α → F⦄ (hf : MemLp f p μ) (hg : MemLp g p μ),
    AEStronglyMeasurable f μ →
      AEStronglyMeasurable g μ →
        Disjoint (Function.support f) (Function.support g) →
          P (MemLp.toLp f hf) → P (MemLp.toLp g hg) → P (MemLp.toLp f hf + MemLp.toLp g hg)
h_closed : IsClosed (X := ↥(lpMeas F ℝ m p μ)) {f : ↥(lpMeas F ℝ m p μ) | P (↑f : ↥(Lp F p μ))}
f_1 : ↥(Lp F p μ)
hf_1 : AEStronglyMeasurable (↑(↑f_1 : α →ₘ[μ] F) : α → F) μ
f' : ↥(lpMeas F ℝ m p μ) :=
  Subtype.mk (p := fun (x : ↥(Lp F p μ)) ↦ Membership.mem (γ := Submodule ℝ ↥(Lp F p μ)) (lpMeas F ℝ m p μ) x) f_1 hf_1
g_1 : ↥(Lp F p (μ.trim hm)) := (lpMeasToLpTrimLie F ℝ p μ hm : (a : ↥(lpMeas F ℝ m p μ)) → ↥(Lp F p (μ.trim hm))) f'
hfg :
  f' = (LinearIsometryEquiv.symm (lpMeasToLpTrimLie F ℝ p μ hm) : (a : ↥(Lp F p (μ.trim hm))) → ↥(lpMeas F ℝ m p μ)) g_1
f g : α → F
hf : MemLp f p (μ.trim hm)
hg : MemLp g p (μ.trim hm)
h_disj : Disjoint (Function.support f) (Function.support g)
hfP : P (MemLp.toLp f ⋯)
hgP :
  P
    (↑((LinearIsometryEquiv.symm (lpMeasToLpTrimLie F ℝ p μ hm) : (a : ↥(Lp F p (μ.trim hm))) → ↥(lpMeas F ℝ m p μ))
          (MemLp.toLp g hg)) :
      ↥(Lp F p μ))
h_eq :
  ∀ (f : α → F) (hf : MemLp f p (μ.trim hm)),
    (↑((LinearIsometryEquiv.symm (lpMeasToLpTrimLie F ℝ p μ hm) : (a : ↥(Lp F p (μ.trim hm))) → ↥(lpMeas F ℝ m p μ))
            (MemLp.toLp f hf)) :
        ↥(Lp F p μ)) =
      MemLp.toLp f ⋯
⊢ P
    (MemLp.toLp f ⋯ +
      (↑((LinearIsometryEquiv.symm (lpMeasToLpTrimLie F ℝ p μ hm) : (a : ↥(Lp F p (μ.trim hm))) → ↥(lpMeas F ℝ m p μ))
            (MemLp.toLp g hg)) :
        ↥(Lp F p μ)))
have refine_2 : ∀ (hgP : P (MemLp.toLp g sorry))
  (h_eq :
    ∀ (f : α → F) (hf : MemLp f p (μ.trim hm)),
      (↑((LinearIsometryEquiv.symm (lpMeasToLpTrimLie F ℝ p μ hm) : (a : ↥(Lp F p (μ.trim hm))) → ↥(lpMeas F ℝ m p μ))
              (MemLp.toLp f hf)) :
          ↥(Lp F p μ)) =
        MemLp.toLp f sorry),
  P (MemLp.toLp f sorry + MemLp.toLp g sorry)
Tactic: rw [h_eq g hg] at hgP ⊢
Cleared hypotheses: hgP, h_eq
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable (goal)
Goal:
α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst : NormedAddCommGroup F
m m0 : MeasurableSpace α
μ : Measure α
inst_1 : Fact (1 ≤ p)
inst_2 : NormedSpace ℝ F
hm : m ≤ m0
hp_ne_top : p ≠ ∞
P : ↥(Lp F p μ) → Prop
h_ind :
  ∀ (c : F) {s : Set α} (hs : MeasurableSet s) (hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
    P (↑(simpleFunc.indicatorConst p (s := s) ⋯ ⋯ c) : ↥(Lp F p μ))
h_add :
  ∀ ⦃f g : α → F⦄ (hf : MemLp f p μ) (hg : MemLp g p μ),
    AEStronglyMeasurable f μ →
      AEStronglyMeasurable g μ →
        Disjoint (Function.support f) (Function.support g) →
          P (MemLp.toLp f hf) → P (MemLp.toLp g hg) → P (MemLp.toLp f hf + MemLp.toLp g hg)
h_closed : IsClosed (X := ↥(lpMeas F ℝ m p μ)) {f : ↥(lpMeas F ℝ m p μ) | P (↑f : ↥(Lp F p μ))}
f : ↥(Lp F p μ)
hf : AEStronglyMeasurable (↑(↑f : α →ₘ[μ] F) : α → F) μ
f' : ↥(lpMeas F ℝ m p μ) :=
  Subtype.mk (p := fun (x : ↥(Lp F p μ)) ↦ Membership.mem (γ := Submodule ℝ ↥(Lp F p μ)) (lpMeas F ℝ m p μ) x) f hf
g : ↥(Lp F p (μ.trim hm)) := (lpMeasToLpTrimLie F ℝ p μ hm : (a : ↥(lpMeas F ℝ m p μ)) → ↥(Lp F p (μ.trim hm))) f'
hfg :
  f' = (LinearIsometryEquiv.symm (lpMeasToLpTrimLie F ℝ p μ hm) : (a : ↥(Lp F p (μ.trim hm))) → ↥(lpMeas F ℝ m p μ)) g
⊢ IsClosed (X := ↥(Lp F p (μ.trim hm)))
    {f : ↥(Lp F p (μ.trim hm)) |
      (fun (g : ↥(Lp F p (μ.trim hm))) ↦
          P
            (↑((LinearIsometryEquiv.symm (lpMeasToLpTrimLie F ℝ p μ hm) :
                    (a : ↥(Lp F p (μ.trim hm))) → ↥(lpMeas F ℝ m p μ))
                  g) :
              ↥(Lp F p μ)))
        f}
have refine_3 : IsClosed (X := ↥(Lp F p (μ.trim hm)))
  (Set.preimage (β := ↥(lpMeas F ℝ m p μ))
    (⇑(LinearIsometryEquiv.symm (lpMeasToLpTrimLie F ℝ p μ hm)) : (a : ↥(Lp F p (μ.trim hm))) → ↥(lpMeas F ℝ m p μ))
    {g : ↥(lpMeas F ℝ m p μ) | P (↑g : ↥(Lp F p μ))})
Tactic: change IsClosed ((lpMeasToLpTrimLie F ℝ p μ hm).symm ⁻¹' {g : lpMeas F ℝ m p μ | P ↑g})
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable (goal)
Goal:
α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst : NormedAddCommGroup F
m m0 : MeasurableSpace α
μ : Measure α
inst_1 : Fact (1 ≤ p)
inst_2 : NormedSpace ℝ F
hm : m ≤ m0
hp_ne_top : p ≠ ∞
P : ↥(Lp F p μ) → Prop
h_ind :
  ∀ (c : F) {s : Set α} (hs : MeasurableSet s) (hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
    P (↑(simpleFunc.indicatorConst p (s := s) ⋯ ⋯ c) : ↥(Lp F p μ))
h_add :
  ∀ ⦃f g : α → F⦄ (hf : MemLp f p μ) (hg : MemLp g p μ),
    StronglyMeasurable f →
      StronglyMeasurable g →
        Disjoint (Function.support f) (Function.support g) →
          P (MemLp.toLp f hf) → P (MemLp.toLp g hg) → P (MemLp.toLp f hf + MemLp.toLp g hg)
h_closed : IsClosed (X := ↥(lpMeas F ℝ m p μ)) {f : ↥(lpMeas F ℝ m p μ) | P (↑f : ↥(Lp F p μ))}
f : ↥(Lp F p μ)
hf : AEStronglyMeasurable (↑(↑f : α →ₘ[μ] F) : α → F) μ
⊢ P f
have suffices : ∀ ⦃f g : α → F⦄ (hf : MemLp f p μ) (hg : MemLp g p μ),
  AEStronglyMeasurable f μ →
    AEStronglyMeasurable g μ →
      Disjoint (Function.support f) (Function.support g) →
        P (MemLp.toLp f hf) → P (MemLp.toLp g hg) → P (MemLp.toLp f hf + MemLp.toLp g hg)
Tactic: suffices h_add_ae :
    ∀ ⦃f g⦄, ∀ hf : MemLp f p μ, ∀ hg : MemLp g p μ, AEStronglyMeasurable[m] f μ →
      AEStronglyMeasurable[m] g μ → Disjoint (Function.support f) (Function.support g) →
        P (hf.toLp f) → P (hg.toLp g) → P (hf.toLp f + hg.toLp g) from
    Lp.induction_stronglyMeasurable_aux hm hp_ne_top _ h_ind h_add_ae h_closed f hf
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable (hypothesis)
Goal:
α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst : NormedAddCommGroup F
m m0 : MeasurableSpace α
μ : Measure α
inst_1 : Fact (1 ≤ p)
inst_2 : NormedSpace ℝ F
hm : m ≤ m0
hp_ne_top : p ≠ ∞
P : ↥(Lp F p μ) → Prop
h_ind :
  ∀ (c : F) {s : Set α} (hs : MeasurableSet s) (hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
    P (↑(simpleFunc.indicatorConst p (s := s) ⋯ ⋯ c) : ↥(Lp F p μ))
h_add :
  ∀ ⦃f g : α → F⦄ (hf : MemLp f p μ) (hg : MemLp g p μ),
    StronglyMeasurable f →
      StronglyMeasurable g →
        Disjoint (Function.support f) (Function.support g) →
          P (MemLp.toLp f hf) → P (MemLp.toLp g hg) → P (MemLp.toLp f hf + MemLp.toLp g hg)
h_closed : IsClosed (X := ↥(lpMeas F ℝ m p μ)) {f : ↥(lpMeas F ℝ m p μ) | P (↑f : ↥(Lp F p μ))}
f_1 : ↥(Lp F p μ)
hf_1 : AEStronglyMeasurable (↑(↑f_1 : α →ₘ[μ] F) : α → F) μ
f g : α → F
hf : MemLp f p μ
hg : MemLp g p μ
hfm : AEStronglyMeasurable f μ
hgm : AEStronglyMeasurable g μ
h_disj : Disjoint (Function.support f) (Function.support g)
hPf : P (MemLp.toLp f hf)
hPg : P (MemLp.toLp g hg)
s_f : Set α := Function.support (AEStronglyMeasurable.mk f hfm)
⊢ P (MemLp.toLp f hf + MemLp.toLp g hg)
have hs_f : MeasurableSet s_f
Tactic: have hs_f : MeasurableSet[m] s_f := hfm.stronglyMeasurable_mk.measurableSet_support
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable (hypothesis)
Goal:
α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst : NormedAddCommGroup F
m m0 : MeasurableSpace α
μ : Measure α
inst_1 : Fact (1 ≤ p)
inst_2 : NormedSpace ℝ F
hm : m ≤ m0
hp_ne_top : p ≠ ∞
P : ↥(Lp F p μ) → Prop
h_ind :
  ∀ (c : F) {s : Set α} (hs : MeasurableSet s) (hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
    P (↑(simpleFunc.indicatorConst p (s := s) ⋯ ⋯ c) : ↥(Lp F p μ))
h_add :
  ∀ ⦃f g : α → F⦄ (hf : MemLp f p μ) (hg : MemLp g p μ),
    StronglyMeasurable f →
      StronglyMeasurable g →
        Disjoint (Function.support f) (Function.support g) →
          P (MemLp.toLp f hf) → P (MemLp.toLp g hg) → P (MemLp.toLp f hf + MemLp.toLp g hg)
h_closed : IsClosed (X := ↥(lpMeas F ℝ m p μ)) {f : ↥(lpMeas F ℝ m p μ) | P (↑f : ↥(Lp F p μ))}
f_1 : ↥(Lp F p μ)
hf_1 : AEStronglyMeasurable (↑(↑f_1 : α →ₘ[μ] F) : α → F) μ
f g : α → F
hf : MemLp f p μ
hg : MemLp g p μ
hfm : AEStronglyMeasurable f μ
hgm : AEStronglyMeasurable g μ
h_disj : Disjoint (Function.support f) (Function.support g)
hPf : P (MemLp.toLp f hf)
hPg : P (MemLp.toLp g hg)
s_f : Set α := Function.support (AEStronglyMeasurable.mk f hfm)
hs_f : MeasurableSet s_f
⊢ P (MemLp.toLp f hf + MemLp.toLp g hg)
have hs_f_eq : s_f =ᶠ[ae μ] Function.support f
Tactic: have hs_f_eq : s_f =ᵐ[μ] Function.support f := hfm.ae_eq_mk.symm.support
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable (hypothesis)
Goal:
α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst : NormedAddCommGroup F
m m0 : MeasurableSpace α
μ : Measure α
inst_1 : Fact (1 ≤ p)
inst_2 : NormedSpace ℝ F
hm : m ≤ m0
hp_ne_top : p ≠ ∞
P : ↥(Lp F p μ) → Prop
h_ind :
  ∀ (c : F) {s : Set α} (hs : MeasurableSet s) (hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
    P (↑(simpleFunc.indicatorConst p (s := s) ⋯ ⋯ c) : ↥(Lp F p μ))
h_add :
  ∀ ⦃f g : α → F⦄ (hf : MemLp f p μ) (hg : MemLp g p μ),
    StronglyMeasurable f →
      StronglyMeasurable g →
        Disjoint (Function.support f) (Function.support g) →
          P (MemLp.toLp f hf) → P (MemLp.toLp g hg) → P (MemLp.toLp f hf + MemLp.toLp g hg)
h_closed : IsClosed (X := ↥(lpMeas F ℝ m p μ)) {f : ↥(lpMeas F ℝ m p μ) | P (↑f : ↥(Lp F p μ))}
f_1 : ↥(Lp F p μ)
hf_1 : AEStronglyMeasurable (↑(↑f_1 : α →ₘ[μ] F) : α → F) μ
f g : α → F
hf : MemLp f p μ
hg : MemLp g p μ
hfm : AEStronglyMeasurable f μ
hgm : AEStronglyMeasurable g μ
h_disj : Disjoint (Function.support f) (Function.support g)
hPf : P (MemLp.toLp f hf)
hPg : P (MemLp.toLp g hg)
s_f : Set α := Function.support (AEStronglyMeasurable.mk f hfm)
hs_f : MeasurableSet s_f
hs_f_eq : s_f =ᶠ[ae μ] Function.support f
s_g : Set α := Function.support (AEStronglyMeasurable.mk g hgm)
⊢ P (MemLp.toLp f hf + MemLp.toLp g hg)
have hs_g : MeasurableSet s_g
Tactic: have hs_g : MeasurableSet[m] s_g := hgm.stronglyMeasurable_mk.measurableSet_support
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable (hypothesis)
Goal:
α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst : NormedAddCommGroup F
m m0 : MeasurableSpace α
μ : Measure α
inst_1 : Fact (1 ≤ p)
inst_2 : NormedSpace ℝ F
hm : m ≤ m0
hp_ne_top : p ≠ ∞
P : ↥(Lp F p μ) → Prop
h_ind :
  ∀ (c : F) {s : Set α} (hs : MeasurableSet s) (hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
    P (↑(simpleFunc.indicatorConst p (s := s) ⋯ ⋯ c) : ↥(Lp F p μ))
h_add :
  ∀ ⦃f g : α → F⦄ (hf : MemLp f p μ) (hg : MemLp g p μ),
    StronglyMeasurable f →
      StronglyMeasurable g →
        Disjoint (Function.support f) (Function.support g) →
          P (MemLp.toLp f hf) → P (MemLp.toLp g hg) → P (MemLp.toLp f hf + MemLp.toLp g hg)
h_closed : IsClosed (X := ↥(lpMeas F ℝ m p μ)) {f : ↥(lpMeas F ℝ m p μ) | P (↑f : ↥(Lp F p μ))}
f_1 : ↥(Lp F p μ)
hf_1 : AEStronglyMeasurable (↑(↑f_1 : α →ₘ[μ] F) : α → F) μ
f g : α → F
hf : MemLp f p μ
hg : MemLp g p μ
hfm : AEStronglyMeasurable f μ
hgm : AEStronglyMeasurable g μ
h_disj : Disjoint (Function.support f) (Function.support g)
hPf : P (MemLp.toLp f hf)
hPg : P (MemLp.toLp g hg)
s_f : Set α := Function.support (AEStronglyMeasurable.mk f hfm)
hs_f : MeasurableSet s_f
hs_f_eq : s_f =ᶠ[ae μ] Function.support f
s_g : Set α := Function.support (AEStronglyMeasurable.mk g hgm)
hs_g : MeasurableSet s_g
⊢ P (MemLp.toLp f hf + MemLp.toLp g hg)
have hs_g_eq : s_g =ᶠ[ae μ] Function.support g
Tactic: have hs_g_eq : s_g =ᵐ[μ] Function.support g := hgm.ae_eq_mk.symm.support
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable (goal)
Goal:
α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst : NormedAddCommGroup F
m m0 : MeasurableSpace α
μ : Measure α
inst_1 : Fact (1 ≤ p)
inst_2 : NormedSpace ℝ F
hm : m ≤ m0
hp_ne_top : p ≠ ∞
P : ↥(Lp F p μ) → Prop
h_ind :
  ∀ (c : F) {s : Set α} (hs : MeasurableSet s) (hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
    P (↑(simpleFunc.indicatorConst p (s := s) ⋯ ⋯ c) : ↥(Lp F p μ))
h_add :
  ∀ ⦃f g : α → F⦄ (hf : MemLp f p μ) (hg : MemLp g p μ),
    StronglyMeasurable f →
      StronglyMeasurable g →
        Disjoint (Function.support f) (Function.support g) →
          P (MemLp.toLp f hf) → P (MemLp.toLp g hg) → P (MemLp.toLp f hf + MemLp.toLp g hg)
h_closed : IsClosed (X := ↥(lpMeas F ℝ m p μ)) {f : ↥(lpMeas F ℝ m p μ) | P (↑f : ↥(Lp F p μ))}
f_1 : ↥(Lp F p μ)
hf_1 : AEStronglyMeasurable (↑(↑f_1 : α →ₘ[μ] F) : α → F) μ
f g : α → F
hf : MemLp f p μ
hg : MemLp g p μ
hfm : AEStronglyMeasurable f μ
hgm : AEStronglyMeasurable g μ
h_disj : Disjoint (Function.support f) (Function.support g)
hPf : P (MemLp.toLp f hf)
hPg : P (MemLp.toLp g hg)
s_f : Set α := Function.support (AEStronglyMeasurable.mk f hfm)
hs_f : MeasurableSet s_f
hs_f_eq : s_f =ᶠ[ae μ] Function.support f
s_g : Set α := Function.support (AEStronglyMeasurable.mk g hgm)
hs_g : MeasurableSet s_g
hs_g_eq : s_g =ᶠ[ae μ] Function.support g
⊢ s_f ∩ s_g =ᶠ[ae μ] ∅
have refine : Function.support f ∩ Function.support g =ᶠ[ae μ] ∅
Tactic: refine (hs_f_eq.inter hs_g_eq).trans ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable (goal)
Goal:
α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst : NormedAddCommGroup F
m m0 : MeasurableSpace α
μ : Measure α
inst_1 : Fact (1 ≤ p)
inst_2 : NormedSpace ℝ F
hm : m ≤ m0
hp_ne_top : p ≠ ∞
P : ↥(Lp F p μ) → Prop
h_ind :
  ∀ (c : F) {s : Set α} (hs : MeasurableSet s) (hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
    P (↑(simpleFunc.indicatorConst p (s := s) ⋯ ⋯ c) : ↥(Lp F p μ))
h_add :
  ∀ ⦃f g : α → F⦄ (hf : MemLp f p μ) (hg : MemLp g p μ),
    StronglyMeasurable f →
      StronglyMeasurable g →
        Disjoint (Function.support f) (Function.support g) →
          P (MemLp.toLp f hf) → P (MemLp.toLp g hg) → P (MemLp.toLp f hf + MemLp.toLp g hg)
h_closed : IsClosed (X := ↥(lpMeas F ℝ m p μ)) {f : ↥(lpMeas F ℝ m p μ) | P (↑f : ↥(Lp F p μ))}
f_1 : ↥(Lp F p μ)
hf_1 : AEStronglyMeasurable (↑(↑f_1 : α →ₘ[μ] F) : α → F) μ
f g : α → F
hf : MemLp f p μ
hg : MemLp g p μ
hfm : AEStronglyMeasurable f μ
hgm : AEStronglyMeasurable g μ
h_disj : Disjoint (Function.support f) (Function.support g)
hPf : P (MemLp.toLp f hf)
hPg : P (MemLp.toLp g hg)
s_f : Set α := Function.support (AEStronglyMeasurable.mk f hfm)
hs_f : MeasurableSet s_f
hs_f_eq : s_f =ᶠ[ae μ] Function.support f
s_g : Set α := Function.support (AEStronglyMeasurable.mk g hgm)
hs_g : MeasurableSet s_g
hs_g_eq : s_g =ᶠ[ae μ] Function.support g
this : Function.support f ∩ Function.support g = ∅
⊢ Function.support f ∩ Function.support g =ᶠ[ae μ] ∅
have rw : (ae μ).EventuallyEq (β := Prop) ∅ ∅
Tactic: rw [this]