awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
inst_4 : IsFiniteMeasure μ
f : ↥(Lp E 2 μ)
⊢ Integrable.{u_2, u_1} (ε := E)
    (↑(↑(↑((condExpL2 E 𝕜 hm : (a : ↥(Lp E 2 μ)) → ↥(lpMeas E 𝕜 m 2 μ)) f) : ↥(Lp E 2 μ)) : α →ₘ[μ] E) : α → E) μ

Tactic:
integrableOn_univ.mp <| integrableOn_condExpL2_of_measure_ne_top hm (measure_ne_top _ _) f

Premises used: MeasureTheory.measure_ne_top, Iff.mp, MeasureTheory.integrableOn_condExpL2_of_measure_ne_top, MeasureTheory.integrableOn_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
⊢ norm (E := ↥(Lp E 2 μ) →L[𝕜] ↥(lpMeas E 𝕜 m 2 μ)) (condExpL2 E 𝕜 hm) ≤ 1

Tactic:
haveI : Fact (m ≤ m0) := ⟨hm⟩
  Submodule.orthogonalProjection_norm_le _

Premises used: Set.Mem, setOf, MeasureTheory.condExpL2, MeasureTheory.lpMeas, OfNat.ofNat, Submodule.orthogonalProjection_norm_le
-- 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 μ)
⊢ norm (E := ↥(lpMeas E 𝕜 m 2 μ))
      ((condExpL2 E 𝕜 hm : (a : ↥(Lp E 2 μ)) → ↥(lpMeas E 𝕜 m 2 μ)) f : ↥(lpMeas E 𝕜 m 2 μ)) ≤
    ‖f‖

Tactic:
((@condExpL2 _ E 𝕜 _ _ _ _ _ _ μ hm).le_opNorm f).trans
    (mul_le_of_le_one_left (norm_nonneg _) (norm_condExpL2_le_one hm))

Premises used: ContinuousLinearMap.le_opNorm, MeasureTheory.condExpL2, mul_le_of_le_one_left, LE.le.trans, norm_nonneg, MeasureTheory.norm_condExpL2_le_one
-- 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 μ)
rw :
  norm (E := ↥(lpMeas E 𝕜 m 2 μ))
      ((condExpL2 E 𝕜 hm : (a : ↥(Lp E 2 μ)) → ↥(lpMeas E 𝕜 m 2 μ)) f : ↥(lpMeas E 𝕜 m 2 μ)) ≤
    ‖f‖
⊢ eLpNorm.{u_1, u_2} (ε := E)
      (↑(↑(↑((condExpL2 E 𝕜 hm : (a : ↥(Lp E 2 μ)) → ↥(lpMeas E 𝕜 m 2 μ)) f) : ↥(Lp E 2 μ)) : α →ₘ[μ] E) : α → E) 2 μ ≤
    eLpNorm (↑(↑f : α →ₘ[μ] E) : α → E) 2 μ

Tactic:
rw [← ENNReal.toReal_le_toReal (Lp.eLpNorm_ne_top _) (Lp.eLpNorm_ne_top _), ←
    Lp.norm_def, ← Lp.norm_def, Submodule.norm_coe]

Premises used: Submodule.norm_coe, ENNReal.toReal_le_toReal, MeasureTheory.Lp.eLpNorm_ne_top, MeasureTheory.Lp.norm_def
-- 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 μ)
⊢ norm (E := ↥(lpMeas E 𝕜 m 2 μ))
      ((condExpL2 E 𝕜 hm : (a : ↥(Lp E 2 μ)) → ↥(lpMeas E 𝕜 m 2 μ)) f : ↥(lpMeas E 𝕜 m 2 μ)) ≤
    ‖f‖

Tactic:
norm_condExpL2_le hm f

Premises used: MeasureTheory.norm_condExpL2_le
-- 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 μ)
⊢ norm (E := ↥(lpMeas E 𝕜 m 2 μ))
      ((condExpL2 E 𝕜 hm : (a : ↥(Lp E 2 μ)) → ↥(lpMeas E 𝕜 m 2 μ)) f : ↥(lpMeas E 𝕜 m 2 μ)) ≤
    ‖f‖

Tactic:
exact norm_condExpL2_le hm f

Premises used: MeasureTheory.norm_condExpL2_le
-- 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 μ)
⊢ (eLpNorm.{u_1, u_2} (ε := E)
        (↑(↑(↑((condExpL2 E 𝕜 hm : (a : ↥(Lp E 2 μ)) → ↥(lpMeas E 𝕜 m 2 μ)) f) : ↥(Lp E 2 μ)) : α →ₘ[μ] E) : α → E) 2
        μ).toReal ≤
    (eLpNorm (↑(↑f : α →ₘ[μ] E) : α → E) 2 μ).toReal

Tactic:
ENNReal.toReal_mono (Lp.eLpNorm_ne_top _) (eLpNorm_condExpL2_le hm f)

Premises used: MeasureTheory.eLpNorm_condExpL2_le, ENNReal.toReal_mono, MeasureTheory.Lp.eLpNorm_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 μ)
⊢ (eLpNorm.{u_1, u_2} (ε := E)
        (↑(↑(↑((condExpL2 E 𝕜 hm : (a : ↥(Lp E 2 μ)) → ↥(lpMeas E 𝕜 m 2 μ)) f) : ↥(Lp E 2 μ)) : α →ₘ[μ] E) : α → E) 2
        μ).toReal ≤
    (eLpNorm (↑(↑f : α →ₘ[μ] E) : α → E) 2 μ).toReal

Tactic:
exact ENNReal.toReal_mono (Lp.eLpNorm_ne_top _) (eLpNorm_condExpL2_le hm f)

Premises used: MeasureTheory.eLpNorm_condExpL2_le, ENNReal.toReal_mono, MeasureTheory.Lp.eLpNorm_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 g : ↥(Lp E 2 μ)
⊢ ⟪(↑((condExpL2 E 𝕜 hm : (a : ↥(Lp E 2 μ)) → ↥(lpMeas E 𝕜 m 2 μ)) f) : ↥(Lp E 2 μ)), g⟫ =
    ⟪f, (↑((condExpL2 E 𝕜 hm : (a : ↥(Lp E 2 μ)) → ↥(lpMeas E 𝕜 m 2 μ)) g) : ↥(Lp E 2 μ))⟫

Tactic:
haveI : Fact (m ≤ m0) := ⟨hm⟩
  Submodule.inner_starProjection_left_eq_right _ f g

Premises used: Set.Mem, setOf, MeasureTheory.lpMeas, Submodule.inner_starProjection_left_eq_right, OfNat.ofNat
-- 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 α
s : Set α
hm : m ≤ m0
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : E
⊢ Fact (m ≤ m0)

Tactic:
haveI : Fact (m ≤ m0) := ⟨hm⟩
-- 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 α
s : Set α
hm : m ≤ m0
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : E
this : Fact (m ≤ m0)
⊢ Membership.mem (γ := Submodule 𝕜 ↥(Lp E 2 μ)) (lpMeas E 𝕜 m 2 μ) (indicatorConstLp (s := s) 2 ⋯ hμs c)

Tactic:
have h_mem : indicatorConstLp 2 (hm s hs) hμs c ∈ lpMeas E 𝕜 m 2 μ :=
    mem_lpMeas_indicatorConstLp hm hs hμs
-- 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 α
s : Set α
hm : m ≤ m0
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : E
this : Fact (m ≤ m0)
h_mem : Membership.mem (γ := Submodule 𝕜 ↥(Lp E 2 μ)) (lpMeas E 𝕜 m 2 μ) (indicatorConstLp (s := s) 2 ⋯ hμs c)
ind : ↥(lpMeas E 𝕜 m 2 μ) :=
  Subtype.mk (p := fun (x : ↥(Lp E 2 μ)) ↦ Membership.mem (γ := Submodule 𝕜 ↥(Lp E 2 μ)) (lpMeas E 𝕜 m 2 μ) x)
    (indicatorConstLp (s := s) 2 ⋯ hμs c) h_mem
⊢ (↑ind : ↥(Lp E 2 μ)) = indicatorConstLp (s := s) 2 ⋯ hμs c

Tactic:
have h_coe_ind : (ind : α →₂[μ] E) = indicatorConstLp 2 (hm s hs) hμs c := rfl
-- 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 α
s : Set α
hm : m ≤ m0
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : E
this : Fact (m ≤ m0)
h_mem : Membership.mem (γ := Submodule 𝕜 ↥(Lp E 2 μ)) (lpMeas E 𝕜 m 2 μ) (indicatorConstLp (s := s) 2 ⋯ hμs c)
ind : ↥(lpMeas E 𝕜 m 2 μ) :=
  Subtype.mk (p := fun (x : ↥(Lp E 2 μ)) ↦ Membership.mem (γ := Submodule 𝕜 ↥(Lp E 2 μ)) (lpMeas E 𝕜 m 2 μ) x)
    (indicatorConstLp (s := s) 2 ⋯ hμs c) h_mem
h_coe_ind : (↑ind : ↥(Lp E 2 μ)) = indicatorConstLp (s := s) 2 ⋯ hμs c
⊢ ((Submodule.orthogonalProjection (𝕜 := 𝕜) (E := ↥(Lp E 2 μ)) (lpMeas E 𝕜 m 2 μ) :
          ↥(Lp E 2 μ) →L[𝕜] ↥(lpMeas E 𝕜 m 2 μ)) :
        (a : ↥(Lp E 2 μ)) → ↥(lpMeas E 𝕜 m 2 μ))
      (↑ind : ↥(Lp E 2 μ)) =
    ind

Tactic:
have h_orth_mem := Submodule.orthogonalProjection_mem_subspace_eq_self ind
-- 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 α
s : Set α
hm : m ≤ m0
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : E
this : Fact (m ≤ m0)
h_mem : Membership.mem (γ := Submodule 𝕜 ↥(Lp E 2 μ)) (lpMeas E 𝕜 m 2 μ) (indicatorConstLp (s := s) 2 ⋯ hμs c)
ind : ↥(lpMeas E 𝕜 m 2 μ) :=
  Subtype.mk (p := fun (x : ↥(Lp E 2 μ)) ↦ Membership.mem (γ := Submodule 𝕜 ↥(Lp E 2 μ)) (lpMeas E 𝕜 m 2 μ) x)
    (indicatorConstLp (s := s) 2 ⋯ hμs c) h_mem
h_coe_ind : (↑ind : ↥(Lp E 2 μ)) = indicatorConstLp (s := s) 2 ⋯ hμs c
h_orth_mem :
  ((Submodule.orthogonalProjection (𝕜 := 𝕜) (E := ↥(Lp E 2 μ)) (lpMeas E 𝕜 m 2 μ) :
          ↥(Lp E 2 μ) →L[𝕜] ↥(lpMeas E 𝕜 m 2 μ)) :
        (a : ↥(Lp E 2 μ)) → ↥(lpMeas E 𝕜 m 2 μ))
      (↑ind : ↥(Lp E 2 μ)) =
    ind
rw :
  (↑(((Submodule.orthogonalProjection (𝕜 := 𝕜) (E := ↥(Lp E 2 μ)) (lpMeas E 𝕜 m 2 μ) :
              ↥(Lp E 2 μ) →L[𝕜] ↥(lpMeas E 𝕜 m 2 μ)) :
            (a : ↥(Lp E 2 μ)) → ↥(lpMeas E 𝕜 m 2 μ))
          (↑ind : ↥(Lp E 2 μ))) :
      ↥(Lp E 2 μ)) =
    (↑ind : ↥(Lp E 2 μ))
rw₁ rw₂ : (↑ind : ↥(Lp E 2 μ)) = (↑ind : ↥(Lp E 2 μ))
⊢ Eq (α := ↥(Lp E 2 μ))
    (↑(((Submodule.orthogonalProjection (𝕜 := 𝕜) (E := ↥(Lp E 2 μ)) (lpMeas E 𝕜 m 2 μ) :
              ↥(Lp E 2 μ) →L[𝕜] ↥(lpMeas E 𝕜 m 2 μ)) :
            (a : ↥(Lp E 2 μ)) → ↥(lpMeas E 𝕜 m 2 μ))
          (indicatorConstLp (s := s) 2 ⋯ hμs c)) :
      ↥(Lp E 2 μ))
    (indicatorConstLp (s := s) 2 ⋯ hμs c)

Tactic:
rw [← h_coe_ind, h_orth_mem]
-- 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 g : ↥(Lp E 2 μ)
hg : AEStronglyMeasurable (↑(↑g : α →ₘ[μ] E) : α → E) μ
symm : ⟪f, g⟫ = ⟪(↑((condExpL2 E 𝕜 hm : (a : ↥(Lp E 2 μ)) → ↥(lpMeas E 𝕜 m 2 μ)) f) : ↥(Lp E 2 μ)), g⟫
⊢ ⟪(↑((condExpL2 E 𝕜 hm : (a : ↥(Lp E 2 μ)) → ↥(lpMeas E 𝕜 m 2 μ)) f) : ↥(Lp E 2 μ)), g⟫ = ⟪f, g⟫

Tactic:
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 g : ↥(Lp E 2 μ)
hg : AEStronglyMeasurable (↑(↑g : α →ₘ[μ] E) : α → E) μ
rw :
  ⟪f -
        (↑(((Submodule.orthogonalProjection (𝕜 := 𝕜) (E := ↥(Lp E 2 μ)) (lpMeas E 𝕜 m 2 μ) :
                  ↥(Lp E 2 μ) →L[𝕜] ↥(lpMeas E 𝕜 m 2 μ)) :
                (a : ↥(Lp E 2 μ)) → ↥(lpMeas E 𝕜 m 2 μ))
              f) :
          ↥(Lp E 2 μ)),
      g⟫ =
    0
⊢ ⟪f, g⟫ = ⟪(↑((condExpL2 E 𝕜 hm : (a : ↥(Lp E 2 μ)) → ↥(lpMeas E 𝕜 m 2 μ)) f) : ↥(Lp E 2 μ)), g⟫

Tactic:
rw [← sub_eq_zero, ← inner_sub_left, condExpL2]

Premises used: sub_eq_zero, MeasureTheory.condExpL2, inner_sub_left
-- 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 g : ↥(Lp E 2 μ)
hg : AEStronglyMeasurable (↑(↑g : α →ₘ[μ] E) : α → E) μ
⊢ ⟪f -
        (↑(((Submodule.orthogonalProjection (𝕜 := 𝕜) (E := ↥(Lp E 2 μ)) (lpMeas E 𝕜 m 2 μ) :
                  ↥(Lp E 2 μ) →L[𝕜] ↥(lpMeas E 𝕜 m 2 μ)) :
                (a : ↥(Lp E 2 μ)) → ↥(lpMeas E 𝕜 m 2 μ))
              f) :
          ↥(Lp E 2 μ)),
      g⟫ =
    0

Tactic:
simp only [← Submodule.starProjection_apply,
    mem_lpMeas_iff_aestronglyMeasurable.mpr hg,
    Submodule.starProjection_inner_eq_zero f g]

Premises used: Iff.mpr, Submodule.starProjection_inner_eq_zero, MeasureTheory.mem_lpMeas_iff_aestronglyMeasurable, Submodule.starProjection_apply
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2
Goal:
α : Type u_1
𝕜 : Type u_7
inst : RCLike 𝕜
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
f : ↥(Lp 𝕜 2 μ)
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
rw :
  ∫ (x : α) in s,
      (↑(↑(↑((condExpL2 𝕜 𝕜 hm : (a : ↥(Lp 𝕜 2 μ)) → ↥(lpMeas 𝕜 𝕜 m 2 μ)) f) : ↥(Lp 𝕜 2 μ)) : α →ₘ[μ] 𝕜) : α → 𝕜) x ∂μ =
    ⟪indicatorConstLp (s := s) 2 ⋯ hμs 1, f⟫
⊢ Eq.{u_7 + 1} (α := 𝕜)
    (∫ (x : α) in s,
      (↑(↑(↑((condExpL2 𝕜 𝕜 hm : (a : ↥(Lp 𝕜 2 μ)) → ↥(lpMeas 𝕜 𝕜 m 2 μ)) f) : ↥(Lp 𝕜 2 μ)) : α →ₘ[μ] 𝕜) : α → 𝕜) x ∂μ)
    (∫ (x : α) in s, (↑(↑f : α →ₘ[μ] 𝕜) : α → 𝕜) x ∂μ)

Tactic:
rw [← L2.inner_indicatorConstLp_one (𝕜 := 𝕜) (hm s hs) hμs f]

Premises used: MeasureTheory.L2.inner_indicatorConstLp_one
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2
Goal:
α : Type u_1
𝕜 : Type u_7
inst : RCLike 𝕜
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
f : ↥(Lp 𝕜 2 μ)
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
rw rw₁ :
  Eq.{u_7 + 1} (α := 𝕜)
    (∫ (x : α) in s,
      (↑(↑(↑((condExpL2 𝕜 𝕜 hm : (a : ↥(Lp 𝕜 2 μ)) → ↥(lpMeas 𝕜 𝕜 m 2 μ)) f) : ↥(Lp 𝕜 2 μ)) : α →ₘ[μ] 𝕜) : α → 𝕜) x ∂μ)
    (∫ (x : α) in s,
      (↑(↑(↑((condExpL2 𝕜 𝕜 hm : (a : ↥(Lp 𝕜 2 μ)) → ↥(lpMeas 𝕜 𝕜 m 2 μ)) f) : ↥(Lp 𝕜 2 μ)) : α →ₘ[μ] 𝕜) : α → 𝕜) x ∂μ)
⊢ ∫ (x : α) in s,
      (↑(↑(↑((condExpL2 𝕜 𝕜 hm : (a : ↥(Lp 𝕜 2 μ)) → ↥(lpMeas 𝕜 𝕜 m 2 μ)) f) : ↥(Lp 𝕜 2 μ)) : α →ₘ[μ] 𝕜) : α → 𝕜) x ∂μ =
    inner 𝕜 (E := ↥(Lp 𝕜 2 μ)) (indicatorConstLp (s := s) 2 ⋯ hμs 1)
      (↑((condExpL2 𝕜 𝕜 hm : (a : ↥(Lp 𝕜 2 μ)) → ↥(lpMeas 𝕜 𝕜 m 2 μ)) f) : ↥(Lp 𝕜 2 μ))

Tactic:
rw [L2.inner_indicatorConstLp_one (hm s hs) hμs]

Premises used: MeasureTheory.L2.inner_indicatorConstLp_one
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2
Goal:
α : Type u_1
𝕜 : Type u_7
inst : RCLike 𝕜
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
f : ↥(Lp 𝕜 2 μ)
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ∫ (x : α) in s,
      (↑(↑(↑((condExpL2 𝕜 𝕜 hm : (a : ↥(Lp 𝕜 2 μ)) → ↥(lpMeas 𝕜 𝕜 m 2 μ)) f) : ↥(Lp 𝕜 2 μ)) : α →ₘ[μ] 𝕜) : α → 𝕜) x ∂μ =
    inner 𝕜 (E := ↥(Lp 𝕜 2 μ)) (indicatorConstLp (s := s) 2 ⋯ hμs 1)
      (↑((condExpL2 𝕜 𝕜 hm : (a : ↥(Lp 𝕜 2 μ)) → ↥(lpMeas 𝕜 𝕜 m 2 μ)) f) : ↥(Lp 𝕜 2 μ))

Tactic:
have h_eq_inner : ∫ x in s, (condExpL2 𝕜 𝕜 hm f : α → 𝕜) x ∂μ =
      ⟪indicatorConstLp 2 (hm s hs) hμs (1 : 𝕜), condExpL2 𝕜 𝕜 hm f⟫ := by
    rw [L2.inner_indicatorConstLp_one (hm s hs) hμs]
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2
Goal:
α : Type u_1
𝕜 : Type u_7
inst : RCLike 𝕜
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
f : ↥(Lp 𝕜 2 μ)
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
h_eq_inner :
  ∫ (x : α) in s,
      (↑(↑(↑((condExpL2 𝕜 𝕜 hm : (a : ↥(Lp 𝕜 2 μ)) → ↥(lpMeas 𝕜 𝕜 m 2 μ)) f) : ↥(Lp 𝕜 2 μ)) : α →ₘ[μ] 𝕜) : α → 𝕜) x ∂μ =
    inner 𝕜 (E := ↥(Lp 𝕜 2 μ)) (indicatorConstLp (s := s) 2 ⋯ hμs 1)
      (↑((condExpL2 𝕜 𝕜 hm : (a : ↥(Lp 𝕜 2 μ)) → ↥(lpMeas 𝕜 𝕜 m 2 μ)) f) : ↥(Lp 𝕜 2 μ))
rw :
  inner 𝕜 (E := ↥(Lp 𝕜 2 μ)) (indicatorConstLp (s := s) 2 ⋯ hμs 1)
      (↑((condExpL2 𝕜 𝕜 hm : (a : ↥(Lp 𝕜 2 μ)) → ↥(lpMeas 𝕜 𝕜 m 2 μ)) f) : ↥(Lp 𝕜 2 μ)) =
    ⟪indicatorConstLp (s := s) 2 ⋯ hμs 1, f⟫
rw₁ :
  ⟪(↑((condExpL2 𝕜 𝕜 hm : (a : ↥(Lp 𝕜 2 μ)) → ↥(lpMeas 𝕜 𝕜 m 2 μ)) (indicatorConstLp (s := s) 2 ⋯ hμs 1)) :
        ↥(Lp 𝕜 2 μ)),
      f⟫ =
    ⟪indicatorConstLp (s := s) 2 ⋯ hμs 1, f⟫
rw₂ rw₃ : ⟪indicatorConstLp (s := s) 2 ⋯ hμs 1, f⟫ = ⟪indicatorConstLp (s := s) 2 ⋯ hμs 1, f⟫
⊢ ∫ (x : α) in s,
      (↑(↑(↑((condExpL2 𝕜 𝕜 hm : (a : ↥(Lp 𝕜 2 μ)) → ↥(lpMeas 𝕜 𝕜 m 2 μ)) f) : ↥(Lp 𝕜 2 μ)) : α →ₘ[μ] 𝕜) : α → 𝕜) x ∂μ =
    ⟪indicatorConstLp (s := s) 2 ⋯ hμs 1, f⟫

Tactic:
rw [h_eq_inner, ← inner_condExpL2_left_eq_right, condExpL2_indicator_of_measurable hm hs hμs]

Premises used: MeasureTheory.inner_condExpL2_left_eq_right, MeasureTheory.condExpL2_indicator_of_measurable
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
f : ↥(Lp ℝ 2 μ)
h_meas : AEStronglyMeasurable (β := ℝ)
  (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ) μ :=
  ⋯
g : α → ℝ :=
  Exists.choose (p := fun (g : α → ℝ) ↦
    StronglyMeasurable g ∧
      (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) :
          α → ℝ) =ᶠ[ae μ]
        g)
    h_meas
⊢ StronglyMeasurable g

Tactic:
have hg_meas : StronglyMeasurable[m] g := h_meas.choose_spec.1
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
f : ↥(Lp ℝ 2 μ)
h_meas : AEStronglyMeasurable (β := ℝ)
  (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ) μ :=
  ⋯
g : α → ℝ :=
  Exists.choose (p := fun (g : α → ℝ) ↦
    StronglyMeasurable g ∧
      (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) :
          α → ℝ) =ᶠ[ae μ]
        g)
    h_meas
hg_meas : StronglyMeasurable g
⊢ g =ᶠ[ae μ] (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ)

Tactic:
have hg_eq : g =ᵐ[μ] condExpL2 ℝ ℝ hm f := h_meas.choose_spec.2.symm
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
f : ↥(Lp ℝ 2 μ)
h_meas : AEStronglyMeasurable (β := ℝ)
  (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ) μ :=
  ⋯
g : α → ℝ :=
  Exists.choose (p := fun (g : α → ℝ) ↦
    StronglyMeasurable g ∧
      (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) :
          α → ℝ) =ᶠ[ae μ]
        g)
    h_meas
hg_meas : StronglyMeasurable g
hg_eq :
  g =ᶠ[ae μ] (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ)
⊢ g =ᶠ[ae (μ.restrict s)]
    (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ)

Tactic:
have hg_eq_restrict : g =ᵐ[μ.restrict s] condExpL2 ℝ ℝ hm f := ae_restrict_of_ae hg_eq
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
f : ↥(Lp ℝ 2 μ)
h_meas : AEStronglyMeasurable (β := ℝ)
  (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ) μ :=
  ⋯
g : α → ℝ :=
  Exists.choose (p := fun (g : α → ℝ) ↦
    StronglyMeasurable g ∧
      (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) :
          α → ℝ) =ᶠ[ae μ]
        g)
    h_meas
hg_meas : StronglyMeasurable g
hg_eq :
  g =ᶠ[ae μ] (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ)
hg_eq_restrict :
  g =ᶠ[ae (μ.restrict s)]
    (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ)
⊢ (ae (μ.restrict s)).EventuallyEq (β := ℝ≥0∞) (fun (x : α) ↦ (↑‖g x‖₊ : ℝ≥0∞)) fun (x : α) ↦
    (↑(nnnorm (E := ℝ)
          ((↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ)
            x)) :
      ℝ≥0∞)

Tactic:
hg_eq_restrict.mono fun x hx => ?_

Premises used: Filter.EventuallyEq, Filter.Eventually.mono
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
f : ↥(Lp ℝ 2 μ)
h_meas : AEStronglyMeasurable (β := ℝ)
  (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ) μ :=
  ⋯
g : α → ℝ :=
  Exists.choose (p := fun (g : α → ℝ) ↦
    StronglyMeasurable g ∧
      (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) :
          α → ℝ) =ᶠ[ae μ]
        g)
    h_meas
hg_meas : StronglyMeasurable g
hg_eq :
  g =ᶠ[ae μ] (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ)
hg_eq_restrict :
  g =ᶠ[ae (μ.restrict s)]
    (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ)
refine :
  ∀ (x : α)
    (hx :
      g x =
        (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ) x),
    Eq (α := ℝ≥0∞) ((fun (x : α) ↦ (↑‖g x‖₊ : ℝ≥0∞)) x)
      ((fun (x : α) ↦
          (↑(nnnorm (E := ℝ)
                ((↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) :
                    α → ℝ)
                  x)) :
            ℝ≥0∞))
        x)
⊢ (ae (μ.restrict s)).EventuallyEq (β := ℝ≥0∞) (fun (x : α) ↦ (↑‖g x‖₊ : ℝ≥0∞)) fun (x : α) ↦
    (↑(nnnorm (E := ℝ)
          ((↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ)
            x)) :
      ℝ≥0∞)

Tactic:
refine hg_eq_restrict.mono fun x hx => ?_

Premises used: Filter.Eventually.mono
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
f : ↥(Lp ℝ 2 μ)
h_meas : AEStronglyMeasurable (β := ℝ)
  (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ) μ :=
  ⋯
g : α → ℝ :=
  Exists.choose (p := fun (g : α → ℝ) ↦
    StronglyMeasurable g ∧
      (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) :
          α → ℝ) =ᶠ[ae μ]
        g)
    h_meas
hg_meas : StronglyMeasurable g
hg_eq :
  g =ᶠ[ae μ] (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ)
hg_eq_restrict :
  g =ᶠ[ae (μ.restrict s)]
    (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ)
x : α
hx : g x = (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ) x
⊢ (↑‖g x‖₊ : ℝ≥0∞) =
    (↑(nnnorm (E := ℝ)
          ((↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ)
            x)) :
      ℝ≥0∞)

Tactic:
simp_rw [hx]