awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s t : Set α
hm : m ≤ m0
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ht : MeasurableSet t
hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
h_eq :
  ∫⁻ (x : α) in t, (↑(nnnorm (E := ℝ) ((↑(↑(indicatorConstLp (s := s) 2 hs hμs 1) : α →ₘ[μ] ℝ) : α → ℝ) x)) : ℝ≥0∞) ∂μ =
    ∫⁻ (x : α) in t, s.indicator (fun (x : α) ↦ 1) x ∂μ
⊢ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (1 : ℝ≥0∞) ((μ.restrict (s ∩ t) : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) =
    (μ : (a : Set α) → ℝ≥0∞) (s ∩ t)

Tactic:
simp only [one_mul, Set.univ_inter, MeasurableSet.univ, Measure.restrict_apply]

Premises used: MeasureTheory.Measure.restrict_apply, Set.univ_inter, one_mul, MeasurableSet.univ
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2
Goal:
α : Type u_1
E : Type u_2
𝕜 : Type u_7
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : CompleteSpace E
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : ↥(Lp E 2 μ)
c : E
⊢ MemLp.{u_1, u_7} (ε := 𝕜)
    (fun (a : α) ↦
      ⟪c,
        (↑(↑(↑((condExpL2 E 𝕜 hm : (a : ↥(Lp E 2 μ)) → ↥(lpMeas E 𝕜 m 2 μ)) f) : ↥(Lp E 2 μ)) : α →ₘ[μ] E) : α → E) a⟫)
    2 μ

Tactic:
MemLp.const_inner _ ?_

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

Tactic:
refine MemLp.const_inner _ ?_

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

Tactic:
Lp.memLp _

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

Tactic:
exact Lp.memLp _

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

Tactic:
have h_mem_Lp : MemLp (fun a => ⟪c, (condExpL2 E 𝕜 hm f : α → E) a⟫) 2 μ := by
    refine MemLp.const_inner _ ?_; exact Lp.memLp _
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2
Goal:
α : Type u_1
E : Type u_2
𝕜 : Type u_7
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : CompleteSpace E
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : ↥(Lp E 2 μ)
c : E
h_mem_Lp :
  MemLp.{u_1, u_7} (ε := 𝕜)
    (fun (a : α) ↦
      ⟪c,
        (↑(↑(↑((condExpL2 E 𝕜 hm : (a : ↥(Lp E 2 μ)) → ↥(lpMeas E 𝕜 m 2 μ)) f) : ↥(Lp E 2 μ)) : α →ₘ[μ] E) : α → E) a⟫)
    2 μ
⊢ EventuallyEq.{u_1, u_7} (β := 𝕜) (ae μ)
    (↑(↑(MemLp.toLp
              (fun (a : α) ↦
                ⟪c,
                  (↑(↑(↑((condExpL2 E 𝕜 hm : (a : ↥(Lp E 2 μ)) → ↥(lpMeas E 𝕜 m 2 μ)) f) : ↥(Lp E 2 μ)) : α →ₘ[μ] E) :
                      α → E)
                    a⟫)
              h_mem_Lp) :
          α →ₘ[μ] 𝕜) :
      α → 𝕜)
    fun (a : α) ↦
    ⟪c, (↑(↑(↑((condExpL2 E 𝕜 hm : (a : ↥(Lp E 2 μ)) → ↥(lpMeas E 𝕜 m 2 μ)) f) : ↥(Lp E 2 μ)) : α →ₘ[μ] E) : α → E) a⟫

Tactic:
have h_eq : h_mem_Lp.toLp _ =ᵐ[μ] fun a => ⟪c, (condExpL2 E 𝕜 hm f : α → E) a⟫ :=
    h_mem_Lp.coeFn_toLp
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2
Goal:
α : Type u_1
E : Type u_2
𝕜 : Type u_7
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : CompleteSpace E
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : ↥(Lp E 2 μ)
c : E
h_mem_Lp :
  MemLp.{u_1, u_7} (ε := 𝕜)
    (fun (a : α) ↦
      ⟪c,
        (↑(↑(↑((condExpL2 E 𝕜 hm : (a : ↥(Lp E 2 μ)) → ↥(lpMeas E 𝕜 m 2 μ)) f) : ↥(Lp E 2 μ)) : α →ₘ[μ] E) : α → E) a⟫)
    2 μ
h_eq :
  EventuallyEq.{u_1, u_7} (β := 𝕜) (ae μ)
    (↑(↑(MemLp.toLp
              (fun (a : α) ↦
                ⟪c,
                  (↑(↑(↑((condExpL2 E 𝕜 hm : (a : ↥(Lp E 2 μ)) → ↥(lpMeas E 𝕜 m 2 μ)) f) : ↥(Lp E 2 μ)) : α →ₘ[μ] E) :
                      α → E)
                    a⟫)
              h_mem_Lp) :
          α →ₘ[μ] 𝕜) :
      α → 𝕜)
    fun (a : α) ↦
    ⟪c, (↑(↑(↑((condExpL2 E 𝕜 hm : (a : ↥(Lp E 2 μ)) → ↥(lpMeas E 𝕜 m 2 μ)) f) : ↥(Lp E 2 μ)) : α →ₘ[μ] E) : α → E) a⟫
⊢ EventuallyEq.{u_1, u_7} (β := 𝕜) (ae μ)
    (↑(↑(↑((condExpL2 𝕜 𝕜 hm : (a : ↥(Lp 𝕜 2 μ)) → ↥(lpMeas 𝕜 𝕜 m 2 μ))
                  (MemLp.toLp (fun (a : α) ↦ ⟪c, (↑(↑f : α →ₘ[μ] E) : α → E) a⟫) ⋯)) :
              ↥(Lp 𝕜 2 μ)) :
          α →ₘ[μ] 𝕜) :
      α → 𝕜)
    fun (a : α) ↦
    ⟪c, (↑(↑(↑((condExpL2 E 𝕜 hm : (a : ↥(Lp E 2 μ)) → ↥(lpMeas E 𝕜 m 2 μ)) f) : ↥(Lp E 2 μ)) : α →ₘ[μ] E) : α → E) a⟫

Tactic:
EventuallyEq.trans ?_ h_eq

Premises used: Filter.EventuallyEq.trans
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2
Goal:
α : Type u_1
E : Type u_2
𝕜 : Type u_7
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : CompleteSpace E
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : ↥(Lp E 2 μ)
c : E
h_mem_Lp :
  MemLp.{u_1, u_7} (ε := 𝕜)
    (fun (a : α) ↦
      ⟪c,
        (↑(↑(↑((condExpL2 E 𝕜 hm : (a : ↥(Lp E 2 μ)) → ↥(lpMeas E 𝕜 m 2 μ)) f) : ↥(Lp E 2 μ)) : α →ₘ[μ] E) : α → E) a⟫)
    2 μ
h_eq :
  EventuallyEq.{u_1, u_7} (β := 𝕜) (ae μ)
    (↑(↑(MemLp.toLp
              (fun (a : α) ↦
                ⟪c,
                  (↑(↑(↑((condExpL2 E 𝕜 hm : (a : ↥(Lp E 2 μ)) → ↥(lpMeas E 𝕜 m 2 μ)) f) : ↥(Lp E 2 μ)) : α →ₘ[μ] E) :
                      α → E)
                    a⟫)
              h_mem_Lp) :
          α →ₘ[μ] 𝕜) :
      α → 𝕜)
    fun (a : α) ↦
    ⟪c, (↑(↑(↑((condExpL2 E 𝕜 hm : (a : ↥(Lp E 2 μ)) → ↥(lpMeas E 𝕜 m 2 μ)) f) : ↥(Lp E 2 μ)) : α →ₘ[μ] E) : α → E) a⟫
refine :
  EventuallyEq.{u_1, u_7} (β := 𝕜) (ae μ)
    (↑(↑(↑((condExpL2 𝕜 𝕜 hm : (a : ↥(Lp 𝕜 2 μ)) → ↥(lpMeas 𝕜 𝕜 m 2 μ))
                  (MemLp.toLp (fun (a : α) ↦ ⟪c, (↑(↑f : α →ₘ[μ] E) : α → E) a⟫) ⋯)) :
              ↥(Lp 𝕜 2 μ)) :
          α →ₘ[μ] 𝕜) :
      α → 𝕜)
    (↑(↑(MemLp.toLp
              (fun (a : α) ↦
                ⟪c,
                  (↑(↑(↑((condExpL2 E 𝕜 hm : (a : ↥(Lp E 2 μ)) → ↥(lpMeas E 𝕜 m 2 μ)) f) : ↥(Lp E 2 μ)) : α →ₘ[μ] E) :
                      α → E)
                    a⟫)
              h_mem_Lp) :
          α →ₘ[μ] 𝕜) :
      α → 𝕜)
⊢ EventuallyEq.{u_1, u_7} (β := 𝕜) (ae μ)
    (↑(↑(↑((condExpL2 𝕜 𝕜 hm : (a : ↥(Lp 𝕜 2 μ)) → ↥(lpMeas 𝕜 𝕜 m 2 μ))
                  (MemLp.toLp (fun (a : α) ↦ ⟪c, (↑(↑f : α →ₘ[μ] E) : α → E) a⟫) ⋯)) :
              ↥(Lp 𝕜 2 μ)) :
          α →ₘ[μ] 𝕜) :
      α → 𝕜)
    fun (a : α) ↦
    ⟪c, (↑(↑(↑((condExpL2 E 𝕜 hm : (a : ↥(Lp E 2 μ)) → ↥(lpMeas E 𝕜 m 2 μ)) f) : ↥(Lp E 2 μ)) : α →ₘ[μ] E) : α → E) a⟫

Tactic:
refine EventuallyEq.trans ?_ h_eq

Premises used: Filter.EventuallyEq.trans
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2
Goal:
α : Type u_1
E : Type u_2
𝕜 : Type u_7
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : CompleteSpace E
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : ↥(Lp E 2 μ)
c : E
h_mem_Lp :
  MemLp.{u_1, u_7} (ε := 𝕜)
    (fun (a : α) ↦
      ⟪c,
        (↑(↑(↑((condExpL2 E 𝕜 hm : (a : ↥(Lp E 2 μ)) → ↥(lpMeas E 𝕜 m 2 μ)) f) : ↥(Lp E 2 μ)) : α →ₘ[μ] E) : α → E) a⟫)
    2 μ
h_eq :
  EventuallyEq.{u_1, u_7} (β := 𝕜) (ae μ)
    (↑(↑(MemLp.toLp
              (fun (a : α) ↦
                ⟪c,
                  (↑(↑(↑((condExpL2 E 𝕜 hm : (a : ↥(Lp E 2 μ)) → ↥(lpMeas E 𝕜 m 2 μ)) f) : ↥(Lp E 2 μ)) : α →ₘ[μ] E) :
                      α → E)
                    a⟫)
              h_mem_Lp) :
          α →ₘ[μ] 𝕜) :
      α → 𝕜)
    fun (a : α) ↦
    ⟪c, (↑(↑(↑((condExpL2 E 𝕜 hm : (a : ↥(Lp E 2 μ)) → ↥(lpMeas E 𝕜 m 2 μ)) f) : ↥(Lp E 2 μ)) : α →ₘ[μ] E) : α → E) a⟫
⊢ EventuallyEq.{u_1, u_7} (β := 𝕜) (ae μ)
    (↑(↑(↑((condExpL2 𝕜 𝕜 hm : (a : ↥(Lp 𝕜 2 μ)) → ↥(lpMeas 𝕜 𝕜 m 2 μ))
                  (MemLp.toLp (fun (a : α) ↦ ⟪c, (↑(↑f : α →ₘ[μ] E) : α → E) a⟫) ⋯)) :
              ↥(Lp 𝕜 2 μ)) :
          α →ₘ[μ] 𝕜) :
      α → 𝕜)
    (↑(↑(MemLp.toLp
              (fun (a : α) ↦
                ⟪c,
                  (↑(↑(↑((condExpL2 E 𝕜 hm : (a : ↥(Lp E 2 μ)) → ↥(lpMeas E 𝕜 m 2 μ)) f) : ↥(Lp E 2 μ)) : α →ₘ[μ] E) :
                      α → E)
                    a⟫)
              h_mem_Lp) :
          α →ₘ[μ] 𝕜) :
      α → 𝕜)

Tactic:
Lp.ae_eq_of_forall_setIntegral_eq' 𝕜 hm _ _ two_ne_zero ENNReal.coe_ne_top
    (fun s _ hμs => integrableOn_condExpL2_of_measure_ne_top hm hμs.ne _) ?_ ?_ ?_ ?_

Premises used: MeasureTheory.MemLp.const_inner, MeasureTheory.Lp.memLp, Inner.inner, MeasureTheory.AEEqFun.cast, MeasureTheory.Lp.ae_eq_of_forall_setIntegral_eq', two_ne_zero, MeasureTheory.MemLp.toLp, MeasureTheory.integrableOn_condExpL2_of_measure_ne_top, Subtype.val, LT.lt.ne, ENNReal.coe_ne_top
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2
Goal:
α : Type u_1
E : Type u_2
𝕜 : Type u_7
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : CompleteSpace E
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : ↥(Lp E 2 μ)
c : E
h_mem_Lp :
  MemLp.{u_1, u_7} (ε := 𝕜)
    (fun (a : α) ↦
      ⟪c,
        (↑(↑(↑((condExpL2 E 𝕜 hm : (a : ↥(Lp E 2 μ)) → ↥(lpMeas E 𝕜 m 2 μ)) f) : ↥(Lp E 2 μ)) : α →ₘ[μ] E) : α → E) a⟫)
    2 μ
h_eq :
  EventuallyEq.{u_1, u_7} (β := 𝕜) (ae μ)
    (↑(↑(MemLp.toLp
              (fun (a : α) ↦
                ⟪c,
                  (↑(↑(↑((condExpL2 E 𝕜 hm : (a : ↥(Lp E 2 μ)) → ↥(lpMeas E 𝕜 m 2 μ)) f) : ↥(Lp E 2 μ)) : α →ₘ[μ] E) :
                      α → E)
                    a⟫)
              h_mem_Lp) :
          α →ₘ[μ] 𝕜) :
      α → 𝕜)
    fun (a : α) ↦
    ⟪c, (↑(↑(↑((condExpL2 E 𝕜 hm : (a : ↥(Lp E 2 μ)) → ↥(lpMeas E 𝕜 m 2 μ)) f) : ↥(Lp E 2 μ)) : α →ₘ[μ] E) : α → E) a⟫
s : Set α
refine_1 :
  MeasurableSet s →
    LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
      IntegrableOn.{u_1, u_7} (ε := 𝕜)
        (↑(↑(MemLp.toLp
                  (fun (a : α) ↦
                    ⟪c,
                      (↑(↑(↑((condExpL2 E 𝕜 hm : (a : ↥(Lp E 2 μ)) → ↥(lpMeas E 𝕜 m 2 μ)) f) : ↥(Lp E 2 μ)) :
                              α →ₘ[μ] E) :
                          α → E)
                        a⟫)
                  h_mem_Lp) :
              α →ₘ[μ] 𝕜) :
          α → 𝕜)
        s μ
⊢ MeasurableSet s →
    LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
      IntegrableOn.{u_1, u_7} (ε := 𝕜)
        (↑(↑(MemLp.toLp
                  (fun (a : α) ↦
                    ⟪c,
                      (↑(↑(↑((condExpL2 E 𝕜 hm : (a : ↥(Lp E 2 μ)) → ↥(lpMeas E 𝕜 m 2 μ)) f) : ↥(Lp E 2 μ)) :
                              α →ₘ[μ] E) :
                          α → E)
                        a⟫)
                  h_mem_Lp) :
              α →ₘ[μ] 𝕜) :
          α → 𝕜)
        s μ

Tactic:
_
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2
Goal:
α : Type u_1
E : Type u_2
𝕜 : Type u_7
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : CompleteSpace E
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : ↥(Lp E 2 μ)
c : E
h_mem_Lp :
  MemLp.{u_1, u_7} (ε := 𝕜)
    (fun (a : α) ↦
      ⟪c,
        (↑(↑(↑((condExpL2 E 𝕜 hm : (a : ↥(Lp E 2 μ)) → ↥(lpMeas E 𝕜 m 2 μ)) f) : ↥(Lp E 2 μ)) : α →ₘ[μ] E) : α → E) a⟫)
    2 μ
h_eq :
  EventuallyEq.{u_1, u_7} (β := 𝕜) (ae μ)
    (↑(↑(MemLp.toLp
              (fun (a : α) ↦
                ⟪c,
                  (↑(↑(↑((condExpL2 E 𝕜 hm : (a : ↥(Lp E 2 μ)) → ↥(lpMeas E 𝕜 m 2 μ)) f) : ↥(Lp E 2 μ)) : α →ₘ[μ] E) :
                      α → E)
                    a⟫)
              h_mem_Lp) :
          α →ₘ[μ] 𝕜) :
      α → 𝕜)
    fun (a : α) ↦
    ⟪c, (↑(↑(↑((condExpL2 E 𝕜 hm : (a : ↥(Lp E 2 μ)) → ↥(lpMeas E 𝕜 m 2 μ)) f) : ↥(Lp E 2 μ)) : α →ₘ[μ] E) : α → E) a⟫
s : Set α
h : MeasurableSet s
hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
refine_1 :
  Integrable.{u_7, u_1} (ε := 𝕜)
    (fun (a : α) ↦
      ⟪c,
        (↑(↑(↑((condExpL2 E 𝕜 hm : (a : ↥(Lp E 2 μ)) → ↥(lpMeas E 𝕜 m 2 μ)) f) : ↥(Lp E 2 μ)) : α →ₘ[μ] E) : α → E) a⟫)
    (μ.restrict s)
⊢ IntegrableOn.{u_1, u_7} (ε := 𝕜)
    (↑(↑(MemLp.toLp
              (fun (a : α) ↦
                ⟪c,
                  (↑(↑(↑((condExpL2 E 𝕜 hm : (a : ↥(Lp E 2 μ)) → ↥(lpMeas E 𝕜 m 2 μ)) f) : ↥(Lp E 2 μ)) : α →ₘ[μ] E) :
                      α → E)
                    a⟫)
              h_mem_Lp) :
          α →ₘ[μ] 𝕜) :
      α → 𝕜)
    s μ

Tactic:
rw [IntegrableOn, integrable_congr (ae_restrict_of_ae h_eq)]

Premises used: MeasureTheory.integrable_congr, MeasureTheory.IntegrableOn, MeasureTheory.ae_restrict_of_ae
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2
Goal:
α : Type u_1
E : Type u_2
𝕜 : Type u_7
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : CompleteSpace E
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : ↥(Lp E 2 μ)
c : E
h_mem_Lp :
  MemLp.{u_1, u_7} (ε := 𝕜)
    (fun (a : α) ↦
      ⟪c,
        (↑(↑(↑((condExpL2 E 𝕜 hm : (a : ↥(Lp E 2 μ)) → ↥(lpMeas E 𝕜 m 2 μ)) f) : ↥(Lp E 2 μ)) : α →ₘ[μ] E) : α → E) a⟫)
    2 μ
h_eq :
  EventuallyEq.{u_1, u_7} (β := 𝕜) (ae μ)
    (↑(↑(MemLp.toLp
              (fun (a : α) ↦
                ⟪c,
                  (↑(↑(↑((condExpL2 E 𝕜 hm : (a : ↥(Lp E 2 μ)) → ↥(lpMeas E 𝕜 m 2 μ)) f) : ↥(Lp E 2 μ)) : α →ₘ[μ] E) :
                      α → E)
                    a⟫)
              h_mem_Lp) :
          α →ₘ[μ] 𝕜) :
      α → 𝕜)
    fun (a : α) ↦
    ⟪c, (↑(↑(↑((condExpL2 E 𝕜 hm : (a : ↥(Lp E 2 μ)) → ↥(lpMeas E 𝕜 m 2 μ)) f) : ↥(Lp E 2 μ)) : α →ₘ[μ] E) : α → E) a⟫
s : Set α
h : MeasurableSet s
hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Integrable.{u_7, u_1} (ε := 𝕜)
    (fun (a : α) ↦
      ⟪c,
        (↑(↑(↑((condExpL2 E 𝕜 hm : (a : ↥(Lp E 2 μ)) → ↥(lpMeas E 𝕜 m 2 μ)) f) : ↥(Lp E 2 μ)) : α →ₘ[μ] E) : α → E) a⟫)
    (μ.restrict s)

Tactic:
(integrableOn_condExpL2_of_measure_ne_top hm hμs.ne _).const_inner _

Premises used: MeasureTheory.integrableOn_condExpL2_of_measure_ne_top, MeasureTheory.Integrable.const_inner, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2
Goal:
α : Type u_1
E : Type u_2
𝕜 : Type u_7
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : CompleteSpace E
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : ↥(Lp E 2 μ)
c : E
h_mem_Lp :
  MemLp.{u_1, u_7} (ε := 𝕜)
    (fun (a : α) ↦
      ⟪c,
        (↑(↑(↑((condExpL2 E 𝕜 hm : (a : ↥(Lp E 2 μ)) → ↥(lpMeas E 𝕜 m 2 μ)) f) : ↥(Lp E 2 μ)) : α →ₘ[μ] E) : α → E) a⟫)
    2 μ
h_eq :
  EventuallyEq.{u_1, u_7} (β := 𝕜) (ae μ)
    (↑(↑(MemLp.toLp
              (fun (a : α) ↦
                ⟪c,
                  (↑(↑(↑((condExpL2 E 𝕜 hm : (a : ↥(Lp E 2 μ)) → ↥(lpMeas E 𝕜 m 2 μ)) f) : ↥(Lp E 2 μ)) : α →ₘ[μ] E) :
                      α → E)
                    a⟫)
              h_mem_Lp) :
          α →ₘ[μ] 𝕜) :
      α → 𝕜)
    fun (a : α) ↦
    ⟪c, (↑(↑(↑((condExpL2 E 𝕜 hm : (a : ↥(Lp E 2 μ)) → ↥(lpMeas E 𝕜 m 2 μ)) f) : ↥(Lp E 2 μ)) : α →ₘ[μ] E) : α → E) a⟫
s : Set α
h : MeasurableSet s
hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Integrable.{u_7, u_1} (ε := 𝕜)
    (fun (a : α) ↦
      ⟪c,
        (↑(↑(↑((condExpL2 E 𝕜 hm : (a : ↥(Lp E 2 μ)) → ↥(lpMeas E 𝕜 m 2 μ)) f) : ↥(Lp E 2 μ)) : α →ₘ[μ] E) : α → E) a⟫)
    (μ.restrict s)

Tactic:
exact (integrableOn_condExpL2_of_measure_ne_top hm hμs.ne _).const_inner _

Premises used: MeasureTheory.integrableOn_condExpL2_of_measure_ne_top, MeasureTheory.Integrable.const_inner, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2
Goal:
α : Type u_1
E : Type u_2
𝕜 : Type u_7
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : CompleteSpace E
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : ↥(Lp E 2 μ)
c : E
h_mem_Lp :
  MemLp.{u_1, u_7} (ε := 𝕜)
    (fun (a : α) ↦
      ⟪c,
        (↑(↑(↑((condExpL2 E 𝕜 hm : (a : ↥(Lp E 2 μ)) → ↥(lpMeas E 𝕜 m 2 μ)) f) : ↥(Lp E 2 μ)) : α →ₘ[μ] E) : α → E) a⟫)
    2 μ
h_eq :
  EventuallyEq.{u_1, u_7} (β := 𝕜) (ae μ)
    (↑(↑(MemLp.toLp
              (fun (a : α) ↦
                ⟪c,
                  (↑(↑(↑((condExpL2 E 𝕜 hm : (a : ↥(Lp E 2 μ)) → ↥(lpMeas E 𝕜 m 2 μ)) f) : ↥(Lp E 2 μ)) : α →ₘ[μ] E) :
                      α → E)
                    a⟫)
              h_mem_Lp) :
          α →ₘ[μ] 𝕜) :
      α → 𝕜)
    fun (a : α) ↦
    ⟪c, (↑(↑(↑((condExpL2 E 𝕜 hm : (a : ↥(Lp E 2 μ)) → ↥(lpMeas E 𝕜 m 2 μ)) f) : ↥(Lp E 2 μ)) : α →ₘ[μ] E) : α → E) a⟫
⊢ AEStronglyMeasurable.{u_1, u_7} (β := 𝕜)
    (↑(↑(↑((condExpL2 𝕜 𝕜 hm : (a : ↥(Lp 𝕜 2 μ)) → ↥(lpMeas 𝕜 𝕜 m 2 μ))
                  (MemLp.toLp (fun (a : α) ↦ ⟪c, (↑(↑f : α →ₘ[μ] E) : α → E) a⟫) ⋯)) :
              ↥(Lp 𝕜 2 μ)) :
          α →ₘ[μ] 𝕜) :
      α → 𝕜)
    μ

Tactic:
lpMeas.aestronglyMeasurable _

Premises used: MeasureTheory.lpMeas.aestronglyMeasurable
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2
Goal:
α : Type u_1
E : Type u_2
𝕜 : Type u_7
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : CompleteSpace E
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : ↥(Lp E 2 μ)
c : E
h_mem_Lp :
  MemLp.{u_1, u_7} (ε := 𝕜)
    (fun (a : α) ↦
      ⟪c,
        (↑(↑(↑((condExpL2 E 𝕜 hm : (a : ↥(Lp E 2 μ)) → ↥(lpMeas E 𝕜 m 2 μ)) f) : ↥(Lp E 2 μ)) : α →ₘ[μ] E) : α → E) a⟫)
    2 μ
h_eq :
  EventuallyEq.{u_1, u_7} (β := 𝕜) (ae μ)
    (↑(↑(MemLp.toLp
              (fun (a : α) ↦
                ⟪c,
                  (↑(↑(↑((condExpL2 E 𝕜 hm : (a : ↥(Lp E 2 μ)) → ↥(lpMeas E 𝕜 m 2 μ)) f) : ↥(Lp E 2 μ)) : α →ₘ[μ] E) :
                      α → E)
                    a⟫)
              h_mem_Lp) :
          α →ₘ[μ] 𝕜) :
      α → 𝕜)
    fun (a : α) ↦
    ⟪c, (↑(↑(↑((condExpL2 E 𝕜 hm : (a : ↥(Lp E 2 μ)) → ↥(lpMeas E 𝕜 m 2 μ)) f) : ↥(Lp E 2 μ)) : α →ₘ[μ] E) : α → E) a⟫
⊢ AEStronglyMeasurable.{u_1, u_7} (β := 𝕜)
    (↑(↑(↑((condExpL2 𝕜 𝕜 hm : (a : ↥(Lp 𝕜 2 μ)) → ↥(lpMeas 𝕜 𝕜 m 2 μ))
                  (MemLp.toLp (fun (a : α) ↦ ⟪c, (↑(↑f : α →ₘ[μ] E) : α → E) a⟫) ⋯)) :
              ↥(Lp 𝕜 2 μ)) :
          α →ₘ[μ] 𝕜) :
      α → 𝕜)
    μ

Tactic:
exact lpMeas.aestronglyMeasurable _

Premises used: MeasureTheory.lpMeas.aestronglyMeasurable
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2
Goal:
α : Type u_1
E : Type u_2
𝕜 : Type u_7
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : CompleteSpace E
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : ↥(Lp E 2 μ)
c : E
h_mem_Lp :
  MemLp.{u_1, u_7} (ε := 𝕜)
    (fun (a : α) ↦
      ⟪c,
        (↑(↑(↑((condExpL2 E 𝕜 hm : (a : ↥(Lp E 2 μ)) → ↥(lpMeas E 𝕜 m 2 μ)) f) : ↥(Lp E 2 μ)) : α →ₘ[μ] E) : α → E) a⟫)
    2 μ
h_eq :
  EventuallyEq.{u_1, u_7} (β := 𝕜) (ae μ)
    (↑(↑(MemLp.toLp
              (fun (a : α) ↦
                ⟪c,
                  (↑(↑(↑((condExpL2 E 𝕜 hm : (a : ↥(Lp E 2 μ)) → ↥(lpMeas E 𝕜 m 2 μ)) f) : ↥(Lp E 2 μ)) : α →ₘ[μ] E) :
                      α → E)
                    a⟫)
              h_mem_Lp) :
          α →ₘ[μ] 𝕜) :
      α → 𝕜)
    fun (a : α) ↦
    ⟪c, (↑(↑(↑((condExpL2 E 𝕜 hm : (a : ↥(Lp E 2 μ)) → ↥(lpMeas E 𝕜 m 2 μ)) f) : ↥(Lp E 2 μ)) : α →ₘ[μ] E) : α → E) a⟫
⊢ AEStronglyMeasurable.{u_1, u_7} (β := 𝕜)
    (↑(↑(MemLp.toLp
              (fun (a : α) ↦
                ⟪c,
                  (↑(↑(↑((condExpL2 E 𝕜 hm : (a : ↥(Lp E 2 μ)) → ↥(lpMeas E 𝕜 m 2 μ)) f) : ↥(Lp E 2 μ)) : α →ₘ[μ] E) :
                      α → E)
                    a⟫)
              h_mem_Lp) :
          α →ₘ[μ] 𝕜) :
      α → 𝕜)
    μ

Tactic:
AEStronglyMeasurable.congr ?_ h_eq.symm

Premises used: MeasureTheory.AEStronglyMeasurable.congr, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2
Goal:
α : Type u_1
E : Type u_2
𝕜 : Type u_7
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : CompleteSpace E
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : ↥(Lp E 2 μ)
c : E
h_mem_Lp :
  MemLp.{u_1, u_7} (ε := 𝕜)
    (fun (a : α) ↦
      ⟪c,
        (↑(↑(↑((condExpL2 E 𝕜 hm : (a : ↥(Lp E 2 μ)) → ↥(lpMeas E 𝕜 m 2 μ)) f) : ↥(Lp E 2 μ)) : α →ₘ[μ] E) : α → E) a⟫)
    2 μ
h_eq :
  EventuallyEq.{u_1, u_7} (β := 𝕜) (ae μ)
    (↑(↑(MemLp.toLp
              (fun (a : α) ↦
                ⟪c,
                  (↑(↑(↑((condExpL2 E 𝕜 hm : (a : ↥(Lp E 2 μ)) → ↥(lpMeas E 𝕜 m 2 μ)) f) : ↥(Lp E 2 μ)) : α →ₘ[μ] E) :
                      α → E)
                    a⟫)
              h_mem_Lp) :
          α →ₘ[μ] 𝕜) :
      α → 𝕜)
    fun (a : α) ↦
    ⟪c, (↑(↑(↑((condExpL2 E 𝕜 hm : (a : ↥(Lp E 2 μ)) → ↥(lpMeas E 𝕜 m 2 μ)) f) : ↥(Lp E 2 μ)) : α →ₘ[μ] E) : α → E) a⟫
refine_4 :
  AEStronglyMeasurable.{u_1, u_7} (β := 𝕜)
    (fun (a : α) ↦
      ⟪c,
        (↑(↑(↑((condExpL2 E 𝕜 hm : (a : ↥(Lp E 2 μ)) → ↥(lpMeas E 𝕜 m 2 μ)) f) : ↥(Lp E 2 μ)) : α →ₘ[μ] E) : α → E) a⟫)
    μ
⊢ AEStronglyMeasurable.{u_1, u_7} (β := 𝕜)
    (↑(↑(MemLp.toLp
              (fun (a : α) ↦
                ⟪c,
                  (↑(↑(↑((condExpL2 E 𝕜 hm : (a : ↥(Lp E 2 μ)) → ↥(lpMeas E 𝕜 m 2 μ)) f) : ↥(Lp E 2 μ)) : α →ₘ[μ] E) :
                      α → E)
                    a⟫)
              h_mem_Lp) :
          α →ₘ[μ] 𝕜) :
      α → 𝕜)
    μ

Tactic:
refine AEStronglyMeasurable.congr ?_ h_eq.symm

Premises used: MeasureTheory.AEStronglyMeasurable.congr, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2
Goal:
α : Type u_1
E : Type u_2
𝕜 : Type u_7
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : CompleteSpace E
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : ↥(Lp E 2 μ)
c : E
h_mem_Lp :
  MemLp.{u_1, u_7} (ε := 𝕜)
    (fun (a : α) ↦
      ⟪c,
        (↑(↑(↑((condExpL2 E 𝕜 hm : (a : ↥(Lp E 2 μ)) → ↥(lpMeas E 𝕜 m 2 μ)) f) : ↥(Lp E 2 μ)) : α →ₘ[μ] E) : α → E) a⟫)
    2 μ
h_eq :
  EventuallyEq.{u_1, u_7} (β := 𝕜) (ae μ)
    (↑(↑(MemLp.toLp
              (fun (a : α) ↦
                ⟪c,
                  (↑(↑(↑((condExpL2 E 𝕜 hm : (a : ↥(Lp E 2 μ)) → ↥(lpMeas E 𝕜 m 2 μ)) f) : ↥(Lp E 2 μ)) : α →ₘ[μ] E) :
                      α → E)
                    a⟫)
              h_mem_Lp) :
          α →ₘ[μ] 𝕜) :
      α → 𝕜)
    fun (a : α) ↦
    ⟪c, (↑(↑(↑((condExpL2 E 𝕜 hm : (a : ↥(Lp E 2 μ)) → ↥(lpMeas E 𝕜 m 2 μ)) f) : ↥(Lp E 2 μ)) : α →ₘ[μ] E) : α → E) a⟫
⊢ AEStronglyMeasurable.{u_1, u_7} (β := 𝕜)
    (fun (a : α) ↦
      ⟪c,
        (↑(↑(↑((condExpL2 E 𝕜 hm : (a : ↥(Lp E 2 μ)) → ↥(lpMeas E 𝕜 m 2 μ)) f) : ↥(Lp E 2 μ)) : α →ₘ[μ] E) : α → E) a⟫)
    μ

Tactic:
(lpMeas.aestronglyMeasurable _).const_inner

Premises used: MeasureTheory.AEStronglyMeasurable.const_inner, MeasureTheory.lpMeas.aestronglyMeasurable