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)
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
rw :
  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 μ))
⊢ (condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) (↑f : ↥(Lp F' 1 μ)) = (↑f : ↥(Lp F' 1 μ))

Tactic:
rw [hfg]
-- 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)
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 μ))

Tactic:
@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

Premises used: Real, LinearIsometryEquiv.symm, MeasureTheory.lpMeasToLpTrimLie, MeasureTheory.condExpL1CLM, MeasureTheory.Lp.induction, OfNat.ofNat, Subtype.val, Eq, DFunLike.coe, ENNReal.coe_ne_top
-- 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)
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∞)
refine_1 :
  Eq (α := ↥(Lp F' 1 μ)) ((condExpInd F' hm μ s : (a : F') → ↥(Lp F' 1 μ)) c : ↥(Lp F' 1 μ))
    (indicatorConstLp (s := s) 1 ⋯ ⋯ c : ↥(Lp F' 1 μ))
⊢ 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 μ))

Tactic:
rw [@Lp.simpleFunc.coe_indicatorConst _ _ m, lpMeasToLpTrimLie_symm_indicator hs hμs.ne c,
      condExpL1CLM_indicatorConstLp]

Premises used: MeasureTheory.condExpL1CLM_indicatorConstLp, MeasureTheory.lpMeasToLpTrimLie_symm_indicator, MeasureTheory.Lp.simpleFunc.coe_indicatorConst, LT.lt.ne
-- 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)
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 μ)) ((condExpInd F' hm μ s : (a : F') → ↥(Lp F' 1 μ)) c : ↥(Lp F' 1 μ))
    (indicatorConstLp (s := s) 1 ⋯ ⋯ c : ↥(Lp F' 1 μ))

Tactic:
condExpInd_of_measurable hs ((le_trim hm).trans_lt hμs).ne c

Premises used: MeasureTheory.condExpInd_of_measurable, MeasureTheory.le_trim, LE.le.trans_lt, LT.lt.ne
-- 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)
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 μ)) ((condExpInd F' hm μ s : (a : F') → ↥(Lp F' 1 μ)) c : ↥(Lp F' 1 μ))
    (indicatorConstLp (s := s) 1 ⋯ ⋯ c : ↥(Lp F' 1 μ))

Tactic:
exact condExpInd_of_measurable hs ((le_trim hm).trans_lt hμs).ne c

Premises used: MeasureTheory.condExpInd_of_measurable, MeasureTheory.le_trim, LE.le.trans_lt, LT.lt.ne
-- 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)
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}

Tactic:
isClosed_eq ?_ ?_

Premises used: setOf, isClosed_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)
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 μ))
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 μ))
⊢ 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}

Tactic:
refine isClosed_eq ?_ ?_

Premises used: isClosed_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)
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 μ))

Tactic:
(condExpL1CLM F' hm μ).continuous.comp (continuous_induced_dom.comp ?_)

Premises used: Continuous.comp, MeasureTheory.condExpL1CLM, ContinuousLinearMap.continuous, continuous_induced_dom
-- 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)
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 (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 μ))
⊢ 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 (condExpL1CLM F' hm μ).continuous.comp (continuous_induced_dom.comp ?_)

Premises used: Continuous.comp, MeasureTheory.condExpL1CLM, ContinuousLinearMap.continuous, continuous_induced_dom
-- 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)
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 (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:
LinearIsometryEquiv.continuous _

Premises used: Set.Mem, LinearIsometryEquiv.continuous
-- 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)
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 (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:
exact LinearIsometryEquiv.continuous _

Premises used: LinearIsometryEquiv.continuous
-- 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)
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 μ))

Tactic:
continuous_induced_dom.comp ?_

Premises used: Continuous.comp, continuous_induced_dom
-- 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)
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 (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 μ))
⊢ 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 continuous_induced_dom.comp ?_

Premises used: Continuous.comp, continuous_induced_dom
-- 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)
inst_3 : CompleteSpace F'
f : ↥(Lp F' 1 μ)
hfm : AEStronglyMeasurable (↑(↑f : α →ₘ[μ] F') : α → F') μ
⊢ (condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) f = f

Tactic:
condExpL1CLM_lpMeas (⟨f, hfm⟩ : lpMeas F' ℝ m 1 μ)

Premises used: Subtype.mk, MeasureTheory.condExpL1CLM_lpMeas
-- 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 : ¬Integrable f μ
⊢ Eq (α := ↥(Lp F' 1 μ)) (condExpL1 hm μ f) 0

Tactic:
setToFun_undef (dominatedFinMeasAdditive_condExpInd F' hm μ) hf

Premises used: MeasureTheory.setToFun_undef, Set.Mem, MeasureTheory.dominatedFinMeasAdditive_condExpInd, MeasureTheory.condExpL1
-- 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'
hf : Integrable f μ
⊢ Eq (α := ↥(Lp F' 1 μ)) (condExpL1 hm μ f)
    ((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) (Integrable.toL1 f hf))

Tactic:
setToFun_eq (dominatedFinMeasAdditive_condExpInd F' hm μ) hf

Premises used: Set.Mem, MeasureTheory.dominatedFinMeasAdditive_condExpInd, MeasureTheory.condExpL1, MeasureTheory.setToFun_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)
⊢ Eq (α := ↥(Lp F' 1 μ)) (condExpL1 hm μ 0) 0

Tactic:
setToFun_zero _

Premises used: Set.Mem, MeasureTheory.condExpL1, MeasureTheory.setToFun_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 α
f : α → F'
hm : m ≤ m0
⊢ Eq (α := ↥(Lp F' 1 0)) (condExpL1 hm 0 f) 0

Tactic:
setToFun_measure_zero _ rfl

Premises used: Set.Mem, MeasureTheory.setToFun_measure_zero, MeasureTheory.condExpL1, rfl
-- 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_1 : m ≤ m0
inst_2 : SigmaFinite (μ.trim hm_1)
f g : α → F'
hm : m ≤ m0
h : f =ᶠ[ae μ] g
⊢ Eq (α := ↥(Lp F' 1 μ)) (condExpL1 hm μ f) (condExpL1 hm μ g)

Tactic:
setToFun_congr_ae _ h

Premises used: Set.Mem, MeasureTheory.condExpL1, MeasureTheory.setToFun_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'
pos : ∀ (hF' : CompleteSpace ↥(Lp F' 1 μ)), AEStronglyMeasurable (↑(↑(condExpL1 hm μ f) : α →ₘ[μ] F') : α → F') μ
neg : ∀ (hF' : ¬CompleteSpace ↥(Lp F' 1 μ)), AEStronglyMeasurable (↑(↑(condExpL1 hm μ f) : α →ₘ[μ] F') : α → F') μ
⊢ AEStronglyMeasurable (↑(↑(condExpL1 hm μ f) : α →ₘ[μ] F') : α → F') μ

Tactic:
by_cases hF' : CompleteSpace (Lp F' 1 μ)

Premises used: CompleteSpace, Membership.mem, Subtype, MeasureTheory.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 μ)
neg : AEStronglyMeasurable.{u_1, u_3} (β := F') (↑0 : α → F') μ
⊢ AEStronglyMeasurable (↑(↑(condExpL1 hm μ f) : α →ₘ[μ] F') : α → F') μ

Tactic:
simp only [condExpL1, setToFun, hF', ↓reduceDIte, ZeroMemClass.coe_zero]

Premises used: MeasureTheory.condExpL1, reduceDIte, ZeroMemClass.coe_zero, MeasureTheory.setToFun
-- 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 μ)
neg : EventuallyEq.{u_1, u_3} (β := F') (ae μ) 0 (↑0 : α → F')
⊢ AEStronglyMeasurable.{u_1, u_3} (β := F') (↑0 : α → 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 μ)
⊢ 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 μ)
⊢ 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 μ)
pos : ∀ (hf : Integrable f μ), AEStronglyMeasurable (↑(↑(condExpL1 hm μ f) : α →ₘ[μ] F') : α → F') μ
neg : ∀ (hf : ¬Integrable f μ), AEStronglyMeasurable (↑(↑(condExpL1 hm μ f) : α →ₘ[μ] F') : α → F') μ
⊢ AEStronglyMeasurable (↑(↑(condExpL1 hm μ f) : α →ₘ[μ] F') : α → F') μ

Tactic:
by_cases hf : Integrable f μ

Premises used: MeasureTheory.Integrable
-- 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 μ
neg : AEStronglyMeasurable.{u_1, u_3} (β := F') (↑(↑0 : α →ₘ[μ] F') : α → F') μ
⊢ AEStronglyMeasurable (↑(↑(condExpL1 hm μ f) : α →ₘ[μ] F') : α → F') μ

Tactic:
rw [condExpL1_undef hf]

Premises used: MeasureTheory.condExpL1_undef
-- 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 μ
⊢ AEStronglyMeasurable.{u_1, u_3} (β := F') (↑(↑0 : α →ₘ[μ] F') : α → F') μ

Tactic:
stronglyMeasurable_zero.aestronglyMeasurable.congr (coeFn_zero ..).symm

Premises used: MeasureTheory.AEStronglyMeasurable.congr, MeasureTheory.StronglyMeasurable.aestronglyMeasurable, MeasureTheory.Lp.coeFn_zero, MeasureTheory.stronglyMeasurable_zero, 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 μ
⊢ AEStronglyMeasurable.{u_1, u_3} (β := F') (↑(↑0 : α →ₘ[μ] F') : α → F') μ

Tactic:
exact stronglyMeasurable_zero.aestronglyMeasurable.congr (coeFn_zero ..).symm

Premises used: MeasureTheory.AEStronglyMeasurable.congr, MeasureTheory.StronglyMeasurable.aestronglyMeasurable, MeasureTheory.Lp.coeFn_zero, MeasureTheory.stronglyMeasurable_zero, 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 μ
pos : ∀ (hf' : f =ᶠ[ae μ] 0), AEStronglyMeasurable (↑(↑(condExpL1 hm μ f) : α →ₘ[μ] F') : α → F') μ
neg : ∀ (hf' : ¬f =ᶠ[ae μ] 0), AEStronglyMeasurable (↑(↑(condExpL1 hm μ f) : α →ₘ[μ] F') : α → F') μ
⊢ AEStronglyMeasurable (↑(↑(condExpL1 hm μ f) : α →ₘ[μ] F') : α → F') μ

Tactic:
by_cases hf' : f =ᵐ[μ] 0