awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2 (goal)
Goal:
α : Type u_1
E' : Type u_3
𝕜 : Type u_7
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E'
inst_2 : InnerProductSpace 𝕜 E'
inst_3 : CompleteSpace E'
inst_4 : NormedSpace ℝ E'
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
x : E'
t : Set α
ht : MeasurableSet t
hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ∫⁻ (a : α) in t,
      (↑(nnnorm (E := ℝ)
              ((↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ))
                              (indicatorConstLp (s := s) 2 hs hμs 1)) :
                          ↥(Lp ℝ 2 μ)) :
                      α →ₘ[μ] ℝ) :
                  α → ℝ)
                a)) :
          ℝ≥0∞) *
        (↑‖x‖₊ : ℝ≥0∞) ∂μ =
    (∫⁻ (a : α) in t,
        (↑(nnnorm (E := ℝ)
              ((↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ))
                              (indicatorConstLp (s := s) 2 hs hμs 1)) :
                          ↥(Lp ℝ 2 μ)) :
                      α →ₘ[μ] ℝ) :
                  α → ℝ)
                a)) :
          ℝ≥0∞) ∂μ) *
      (↑‖x‖₊ : ℝ≥0∞)
have hf : Measurable (β := ℝ≥0∞) fun (a : α) ↦
  (↑(nnnorm (E := ℝ)
        ((↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) (indicatorConstLp (s := s) 2 hs hμs 1)) :
                    ↥(Lp ℝ 2 μ)) :
                α →ₘ[μ] ℝ) :
            α → ℝ)
          a)) :
    ℝ≥0∞)
Tactic: rw [lintegral_mul_const]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2 (goal)
Goal:
α : Type u_1
E' : Type u_3
𝕜 : Type u_7
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E'
inst_2 : InnerProductSpace 𝕜 E'
inst_3 : CompleteSpace E'
inst_4 : NormedSpace ℝ E'
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
x : E'
t : Set α
ht : MeasurableSet t
hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ (∫⁻ (a : α) in t,
        (↑(nnnorm (E := ℝ)
              ((↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ))
                              (indicatorConstLp (s := s) 2 hs hμs 1)) :
                          ↥(Lp ℝ 2 μ)) :
                      α →ₘ[μ] ℝ) :
                  α → ℝ)
                a)) :
          ℝ≥0∞) ∂μ) *
      (↑‖x‖₊ : ℝ≥0∞) ≤
    HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) (↑‖x‖₊ : ℝ≥0∞)
have grw : HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) (↑‖x‖₊ : ℝ≥0∞) ≤
  HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) (↑‖x‖₊ : ℝ≥0∞)
Tactic: grw [lintegral_nnnorm_condExpL2_indicator_le_real hs hμs ht hμt]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2 (goal)
Goal:
α : Type u_1
E' : Type u_3
𝕜 : Type u_7
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E'
inst_2 : InnerProductSpace 𝕜 E'
inst_3 : CompleteSpace E'
inst_4 : NormedSpace ℝ E'
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
x : E'
inst_5 : SigmaFinite (μ.trim hm)
⊢ ∫⁻ (a : α),
      (↑(nnnorm.{u_3} (E := E')
            ((↑(↑(↑((condExpL2 E' 𝕜 hm : (a : ↥(Lp E' 2 μ)) → ↥(lpMeas E' 𝕜 m 2 μ))
                            (indicatorConstLp (s := s) 2 hs hμs x)) :
                        ↥(Lp E' 2 μ)) :
                    α →ₘ[μ] E') :
                α → E')
              a)) :
        ℝ≥0∞) ∂μ ≤
    HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (↑‖x‖₊ : ℝ≥0∞)
have refine : ∀ (t : Set α) (ht : MeasurableSet t) (hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)),
  ∫⁻ (x_1 : α) in t,
      (↑(nnnorm.{u_3} (E := E')
            ((↑(↑(↑((condExpL2 E' 𝕜 hm : (a : ↥(Lp E' 2 μ)) → ↥(lpMeas E' 𝕜 m 2 μ))
                            (indicatorConstLp (s := s) 2 hs hμs x)) :
                        ↥(Lp E' 2 μ)) :
                    α →ₘ[μ] E') :
                α → E')
              x_1)) :
        ℝ≥0∞) ∂μ ≤
    HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (↑‖x‖₊ : ℝ≥0∞)
Tactic: refine lintegral_le_of_forall_fin_meas_trim_le hm (μ s * ‖x‖₊) fun t ht hμt => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2 (goal)
Goal:
α : Type u_1
E' : Type u_3
𝕜 : Type u_7
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E'
inst_2 : InnerProductSpace 𝕜 E'
inst_3 : CompleteSpace E'
inst_4 : NormedSpace ℝ E'
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
x : E'
inst_5 : SigmaFinite (μ.trim hm)
t : Set α
ht : MeasurableSet t
hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ∫⁻ (x_1 : α) in t,
      (↑(nnnorm.{u_3} (E := E')
            ((↑(↑(↑((condExpL2 E' 𝕜 hm : (a : ↥(Lp E' 2 μ)) → ↥(lpMeas E' 𝕜 m 2 μ))
                            (indicatorConstLp (s := s) 2 hs hμs x)) :
                        ↥(Lp E' 2 μ)) :
                    α →ₘ[μ] E') :
                α → E')
              x_1)) :
        ℝ≥0∞) ∂μ ≤
    HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (↑‖x‖₊ : ℝ≥0∞)
have refine : HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) (↑‖x‖₊ : ℝ≥0∞) ≤
  HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (↑‖x‖₊ : ℝ≥0∞)
Tactic: refine (setLIntegral_nnnorm_condExpL2_indicator_le hm hs hμs x ht hμt).trans ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2 (goal)
Goal:
α : Type u_1
E' : Type u_3
𝕜 : Type u_7
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E'
inst_2 : InnerProductSpace 𝕜 E'
inst_3 : CompleteSpace E'
inst_4 : NormedSpace ℝ E'
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
x : E'
inst_5 : SigmaFinite (μ.trim hm)
t : Set α
ht : MeasurableSet t
hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) (↑‖x‖₊ : ℝ≥0∞) ≤
    HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (↑‖x‖₊ : ℝ≥0∞)
have bc : s ∩ t ⊆ s
Tactic: gcongr
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2 (goal)
Goal:
α : Type u_1
E' : Type u_3
𝕜 : Type u_7
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E'
inst_2 : InnerProductSpace 𝕜 E'
inst_3 : CompleteSpace E'
inst_4 : NormedSpace ℝ E'
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
inst_5 : SigmaFinite (μ.trim hm)
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
x : E'
⊢ Integrable.{u_3, u_1} (ε := E')
    (↑(↑(↑((condExpL2 E' 𝕜 hm : (a : ↥(Lp E' 2 μ)) → ↥(lpMeas E' 𝕜 m 2 μ)) (indicatorConstLp (s := s) 2 hs hμs x)) :
              ↥(Lp E' 2 μ)) :
          α →ₘ[μ] E') :
      α → E')
    μ
have refine_1 : AEStronglyMeasurable.{u_1, u_3} (β := E')
  (↑(↑(↑((condExpL2 E' 𝕜 hm : (a : ↥(Lp E' 2 μ)) → ↥(lpMeas E' 𝕜 m 2 μ)) (indicatorConstLp (s := s) 2 hs hμs x)) :
            ↥(Lp E' 2 μ)) :
        α →ₘ[μ] E') :
    α → E')
  μ
Tactic: refine integrable_of_forall_fin_meas_le' hm (μ s * ‖x‖₊)
    (ENNReal.mul_lt_top hμs.lt_top ENNReal.coe_lt_top) ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2 (goal)
Goal:
α : Type u_1
E' : Type u_3
𝕜 : Type u_7
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E'
inst_2 : InnerProductSpace 𝕜 E'
inst_3 : CompleteSpace E'
inst_4 : NormedSpace ℝ E'
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
inst_5 : SigmaFinite (μ.trim hm)
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
x : E'
refine_1 :
  AEStronglyMeasurable.{u_1, u_3} (β := E')
    (↑(↑(↑((condExpL2 E' 𝕜 hm : (a : ↥(Lp E' 2 μ)) → ↥(lpMeas E' 𝕜 m 2 μ)) (indicatorConstLp (s := s) 2 hs hμs x)) :
              ↥(Lp E' 2 μ)) :
          α →ₘ[μ] E') :
      α → E')
    μ
⊢ Integrable.{u_3, u_1} (ε := E')
    (↑(↑(↑((condExpL2 E' 𝕜 hm : (a : ↥(Lp E' 2 μ)) → ↥(lpMeas E' 𝕜 m 2 μ)) (indicatorConstLp (s := s) 2 hs hμs x)) :
              ↥(Lp E' 2 μ)) :
          α →ₘ[μ] E') :
      α → E')
    μ
have refine_2 : ∀ (s_1 : Set α),
  MeasurableSet s_1 →
    Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s_1 : ℝ≥0∞) (∞ : ℝ≥0∞) →
      ∫⁻ (x_1 : α) in s_1,
          enorm.{u_3} (E := E')
            ((↑(↑(↑((condExpL2 E' 𝕜 hm : (a : ↥(Lp E' 2 μ)) → ↥(lpMeas E' 𝕜 m 2 μ))
                            (indicatorConstLp (s := s) 2 hs hμs x)) :
                        ↥(Lp E' 2 μ)) :
                    α →ₘ[μ] E') :
                α → E')
              x_1) ∂μ ≤
        HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (↑‖x‖₊ : ℝ≥0∞)
Tactic: refine integrable_of_forall_fin_meas_le' hm (μ s * ‖x‖₊)
    (ENNReal.mul_lt_top hμs.lt_top ENNReal.coe_lt_top) ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2 (goal)
Goal:
α : Type u_1
E' : Type u_3
𝕜 : Type u_7
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E'
inst_2 : InnerProductSpace 𝕜 E'
inst_3 : CompleteSpace E'
inst_4 : NormedSpace ℝ E'
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
inst_5 : SigmaFinite (μ.trim hm)
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
x : E'
⊢ ∀ (s_1 : Set α),
    MeasurableSet s_1 →
      Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s_1 : ℝ≥0∞) (∞ : ℝ≥0∞) →
        ∫⁻ (x_1 : α) in s_1,
            enorm.{u_3} (E := E')
              ((↑(↑(↑((condExpL2 E' 𝕜 hm : (a : ↥(Lp E' 2 μ)) → ↥(lpMeas E' 𝕜 m 2 μ))
                              (indicatorConstLp (s := s) 2 hs hμs x)) :
                          ↥(Lp E' 2 μ)) :
                      α →ₘ[μ] E') :
                  α → E')
                x_1) ∂μ ≤
          HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (↑‖x‖₊ : ℝ≥0∞)
have refine_2 : ∀ (t : Set α) (ht : MeasurableSet t) (hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)),
  HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) (↑‖x‖₊ : ℝ≥0∞) ≤
    HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (↑‖x‖₊ : ℝ≥0∞)
Tactic: refine fun t ht hμt =>
      (setLIntegral_nnnorm_condExpL2_indicator_le hm hs hμs x ht hμt).trans ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2 (goal)
Goal:
α : Type u_1
E' : Type u_3
𝕜 : Type u_7
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E'
inst_2 : InnerProductSpace 𝕜 E'
inst_3 : CompleteSpace E'
inst_4 : NormedSpace ℝ E'
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
inst_5 : SigmaFinite (μ.trim hm)
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
x : E'
t : Set α
ht : MeasurableSet t
hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) (↑‖x‖₊ : ℝ≥0∞) ≤
    HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (↑‖x‖₊ : ℝ≥0∞)
have refine_2 : s ∩ t ⊆ s
Tactic: gcongr
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2 (hypothesis)
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst_1 : NormedSpace ℝ G
hm : m ≤ m0
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
x : G
⊢ AEStronglyMeasurable (↑(↑(condExpIndSMul (s := s) hm hs hμs x) : α →ₘ[μ] G) : α → G) μ
have h : AEStronglyMeasurable (β := ℝ)
  (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) (indicatorConstLp (s := s) 2 hs hμs 1)) :
            ↥(Lp ℝ 2 μ)) :
        α →ₘ[μ] ℝ) :
    α → ℝ)
  μ
Tactic: have h : AEStronglyMeasurable[m] (condExpL2 ℝ ℝ hm (indicatorConstLp 2 hs hμs 1) : α → ℝ) μ :=
    aestronglyMeasurable_condExpL2 _ _
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2 (goal)
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst_1 : NormedSpace ℝ G
hm : m ≤ m0
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
x : G
h :
  AEStronglyMeasurable (β := ℝ)
    (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) (indicatorConstLp (s := s) 2 hs hμs 1)) :
              ↥(Lp ℝ 2 μ)) :
          α →ₘ[μ] ℝ) :
      α → ℝ)
    μ
⊢ AEStronglyMeasurable (↑(↑(condExpIndSMul (s := s) hm hs hμs x) : α →ₘ[μ] G) : α → G) μ
have rw : AEStronglyMeasurable.{u_1, u_5} (β := G)
  (↑(↑((compLpL 2 μ (toSpanSingleton ℝ x) : (a : ↥(Lp ℝ 2 μ)) → ↥(Lp G 2 μ))
            (↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) (indicatorConstLp (s := s) 2 hs hμs 1)) :
              ↥(Lp ℝ 2 μ))) :
        α →ₘ[μ] G) :
    α → G)
  μ
Tactic: rw [condExpIndSMul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2 (goal)
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst_1 : NormedSpace ℝ G
hm : m ≤ m0
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
x y : G
⊢ (compLpL 2 μ (toSpanSingleton ℝ (x + y)) : (a : ↥(Lp ℝ 2 μ)) → ↥(Lp G 2 μ))
      (↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) (indicatorConstLp (s := s) 2 hs hμs 1)) :
        ↥(Lp ℝ 2 μ)) =
    HAdd.hAdd (α := ↥(Lp G 2 μ))
      ((compLpL 2 μ (toSpanSingleton ℝ x) : (a : ↥(Lp ℝ 2 μ)) → ↥(Lp G 2 μ))
        (↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) (indicatorConstLp (s := s) 2 hs hμs 1)) :
          ↥(Lp ℝ 2 μ)))
      ((compLpL 2 μ (toSpanSingleton ℝ y) : (a : ↥(Lp ℝ 2 μ)) → ↥(Lp G 2 μ))
        (↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) (indicatorConstLp (s := s) 2 hs hμs 1)) :
          ↥(Lp ℝ 2 μ)))
have rw : (compLpL 2 μ (HAdd.hAdd (α := ℝ →L[ℝ] G) (toSpanSingleton ℝ x) (toSpanSingleton ℝ y)) : (a : ↥(Lp ℝ 2 μ)) → ↥(Lp G 2 μ))
    (↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) (indicatorConstLp (s := s) 2 hs hμs 1)) :
      ↥(Lp ℝ 2 μ)) =
  HAdd.hAdd (α := ↥(Lp G 2 μ))
    ((compLpL 2 μ (toSpanSingleton ℝ x) : (a : ↥(Lp ℝ 2 μ)) → ↥(Lp G 2 μ))
      (↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) (indicatorConstLp (s := s) 2 hs hμs 1)) :
        ↥(Lp ℝ 2 μ)))
    ((compLpL 2 μ (toSpanSingleton ℝ y) : (a : ↥(Lp ℝ 2 μ)) → ↥(Lp G 2 μ))
      (↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) (indicatorConstLp (s := s) 2 hs hμs 1)) :
        ↥(Lp ℝ 2 μ)))
Tactic: rw [toSpanSingleton_add, add_compLpL, add_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2 (goal)
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst_1 : NormedSpace ℝ G
hm : m ≤ m0
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
x y : G
rw :
  (compLpL 2 μ (HAdd.hAdd (α := ℝ →L[ℝ] G) (toSpanSingleton ℝ x) (toSpanSingleton ℝ y)) :
        (a : ↥(Lp ℝ 2 μ)) → ↥(Lp G 2 μ))
      (↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) (indicatorConstLp (s := s) 2 hs hμs 1)) :
        ↥(Lp ℝ 2 μ)) =
    HAdd.hAdd (α := ↥(Lp G 2 μ))
      ((compLpL 2 μ (toSpanSingleton ℝ x) : (a : ↥(Lp ℝ 2 μ)) → ↥(Lp G 2 μ))
        (↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) (indicatorConstLp (s := s) 2 hs hμs 1)) :
          ↥(Lp ℝ 2 μ)))
      ((compLpL 2 μ (toSpanSingleton ℝ y) : (a : ↥(Lp ℝ 2 μ)) → ↥(Lp G 2 μ))
        (↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) (indicatorConstLp (s := s) 2 hs hμs 1)) :
          ↥(Lp ℝ 2 μ)))
⊢ (compLpL 2 μ (toSpanSingleton ℝ (x + y)) : (a : ↥(Lp ℝ 2 μ)) → ↥(Lp G 2 μ))
      (↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) (indicatorConstLp (s := s) 2 hs hμs 1)) :
        ↥(Lp ℝ 2 μ)) =
    HAdd.hAdd (α := ↥(Lp G 2 μ))
      ((compLpL 2 μ (toSpanSingleton ℝ x) : (a : ↥(Lp ℝ 2 μ)) → ↥(Lp G 2 μ))
        (↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) (indicatorConstLp (s := s) 2 hs hμs 1)) :
          ↥(Lp ℝ 2 μ)))
      ((compLpL 2 μ (toSpanSingleton ℝ y) : (a : ↥(Lp ℝ 2 μ)) → ↥(Lp G 2 μ))
        (↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) (indicatorConstLp (s := s) 2 hs hμs 1)) :
          ↥(Lp ℝ 2 μ)))
have rw₁ : (HAdd.hAdd (α := ↥(Lp ℝ 2 μ) →L[ℝ] ↥(Lp G 2 μ)) (compLpL 2 μ (toSpanSingleton ℝ x))
        (compLpL 2 μ (toSpanSingleton ℝ y)) :
      (a : ↥(Lp ℝ 2 μ)) → ↥(Lp G 2 μ))
    (↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) (indicatorConstLp (s := s) 2 hs hμs 1)) :
      ↥(Lp ℝ 2 μ)) =
  HAdd.hAdd (α := ↥(Lp G 2 μ))
    ((compLpL 2 μ (toSpanSingleton ℝ x) : (a : ↥(Lp ℝ 2 μ)) → ↥(Lp G 2 μ))
      (↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) (indicatorConstLp (s := s) 2 hs hμs 1)) :
        ↥(Lp ℝ 2 μ)))
    ((compLpL 2 μ (toSpanSingleton ℝ y) : (a : ↥(Lp ℝ 2 μ)) → ↥(Lp G 2 μ))
      (↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) (indicatorConstLp (s := s) 2 hs hμs 1)) :
        ↥(Lp ℝ 2 μ)))
Tactic: rw [toSpanSingleton_add, add_compLpL, add_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2 (goal)
Goal:
α : Type u_1
F : Type u_4
𝕜 : Type u_7
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
inst_3 : NormedSpace ℝ F
inst_4 : SMulCommClass ℝ 𝕜 F
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : 𝕜
x : F
⊢ condExpIndSMul (s := s) hm hs hμs (c • x) = HSMul.hSMul (β := ↥(Lp F 2 μ)) c (condExpIndSMul (s := s) hm hs hμs x)
have simp_rw : (compLpL 2 μ (toSpanSingleton ℝ (c • x)) : (a : ↥(Lp ℝ 2 μ)) → ↥(Lp F 2 μ))
    (↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) (indicatorConstLp (s := s) 2 hs hμs 1)) :
      ↥(Lp ℝ 2 μ)) =
  HSMul.hSMul (β := ↥(Lp F 2 μ)) c
    ((compLpL 2 μ (toSpanSingleton ℝ x) : (a : ↥(Lp ℝ 2 μ)) → ↥(Lp F 2 μ))
      (↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) (indicatorConstLp (s := s) 2 hs hμs 1)) :
        ↥(Lp ℝ 2 μ)))
Tactic: simp_rw [condExpIndSMul, toSpanSingleton_smul, smul_compLpL, smul_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2 (goal)
Goal:
α : Type u_1
F : Type u_4
𝕜 : Type u_7
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
inst_3 : NormedSpace ℝ F
inst_4 : SMulCommClass ℝ 𝕜 F
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : 𝕜
x : F
simp_rw :
  (compLpL 2 μ (toSpanSingleton ℝ (c • x)) : (a : ↥(Lp ℝ 2 μ)) → ↥(Lp F 2 μ))
      (↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) (indicatorConstLp (s := s) 2 hs hμs 1)) :
        ↥(Lp ℝ 2 μ)) =
    HSMul.hSMul (β := ↥(Lp F 2 μ)) c
      ((compLpL 2 μ (toSpanSingleton ℝ x) : (a : ↥(Lp ℝ 2 μ)) → ↥(Lp F 2 μ))
        (↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) (indicatorConstLp (s := s) 2 hs hμs 1)) :
          ↥(Lp ℝ 2 μ)))
⊢ condExpIndSMul (s := s) hm hs hμs (c • x) = HSMul.hSMul (β := ↥(Lp F 2 μ)) c (condExpIndSMul (s := s) hm hs hμs x)
have simp_rw₁ : (compLpL 2 μ (HSMul.hSMul (β := ℝ →L[ℝ] F) c (toSpanSingleton ℝ x)) : (a : ↥(Lp ℝ 2 μ)) → ↥(Lp F 2 μ))
    (↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) (indicatorConstLp (s := s) 2 hs hμs 1)) :
      ↥(Lp ℝ 2 μ)) =
  HSMul.hSMul (β := ↥(Lp F 2 μ)) c
    ((compLpL 2 μ (toSpanSingleton ℝ x) : (a : ↥(Lp ℝ 2 μ)) → ↥(Lp F 2 μ))
      (↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) (indicatorConstLp (s := s) 2 hs hμs 1)) :
        ↥(Lp ℝ 2 μ)))
Tactic: simp_rw [condExpIndSMul, toSpanSingleton_smul, smul_compLpL, smul_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2 (goal)
Goal:
α : Type u_1
F : Type u_4
𝕜 : Type u_7
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
inst_3 : NormedSpace ℝ F
inst_4 : SMulCommClass ℝ 𝕜 F
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : 𝕜
x : F
simp_rw :
  (compLpL 2 μ (toSpanSingleton ℝ (c • x)) : (a : ↥(Lp ℝ 2 μ)) → ↥(Lp F 2 μ))
      (↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) (indicatorConstLp (s := s) 2 hs hμs 1)) :
        ↥(Lp ℝ 2 μ)) =
    HSMul.hSMul (β := ↥(Lp F 2 μ)) c
      ((compLpL 2 μ (toSpanSingleton ℝ x) : (a : ↥(Lp ℝ 2 μ)) → ↥(Lp F 2 μ))
        (↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) (indicatorConstLp (s := s) 2 hs hμs 1)) :
          ↥(Lp ℝ 2 μ)))
simp_rw₁ :
  (compLpL 2 μ (HSMul.hSMul (β := ℝ →L[ℝ] F) c (toSpanSingleton ℝ x)) : (a : ↥(Lp ℝ 2 μ)) → ↥(Lp F 2 μ))
      (↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) (indicatorConstLp (s := s) 2 hs hμs 1)) :
        ↥(Lp ℝ 2 μ)) =
    HSMul.hSMul (β := ↥(Lp F 2 μ)) c
      ((compLpL 2 μ (toSpanSingleton ℝ x) : (a : ↥(Lp ℝ 2 μ)) → ↥(Lp F 2 μ))
        (↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) (indicatorConstLp (s := s) 2 hs hμs 1)) :
          ↥(Lp ℝ 2 μ)))
⊢ condExpIndSMul (s := s) hm hs hμs (c • x) = HSMul.hSMul (β := ↥(Lp F 2 μ)) c (condExpIndSMul (s := s) hm hs hμs x)
have simp_rw₂ : (HSMul.hSMul (β := ↥(Lp ℝ 2 μ) →L[ℝ] ↥(Lp F 2 μ)) c (compLpL 2 μ (toSpanSingleton ℝ x)) :
      (a : ↥(Lp ℝ 2 μ)) → ↥(Lp F 2 μ))
    (↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) (indicatorConstLp (s := s) 2 hs hμs 1)) :
      ↥(Lp ℝ 2 μ)) =
  HSMul.hSMul (β := ↥(Lp F 2 μ)) c
    ((compLpL 2 μ (toSpanSingleton ℝ x) : (a : ↥(Lp ℝ 2 μ)) → ↥(Lp F 2 μ))
      (↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) (indicatorConstLp (s := s) 2 hs hμs 1)) :
        ↥(Lp ℝ 2 μ)))
Tactic: simp_rw [condExpIndSMul, toSpanSingleton_smul, smul_compLpL, smul_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2 (goal)
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst_1 : NormedSpace ℝ G
hm : m ≤ m0
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
x : G
t : Set α
ht : MeasurableSet t
hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
a : α
ha :
  (↑(↑(condExpIndSMul (s := s) hm hs hμs x) : α →ₘ[μ] G) : α → G) a =
    (fun (a : α) ↦
        HSMul.hSMul (α := ℝ)
          ((↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) (indicatorConstLp (s := s) 2 hs hμs 1)) :
                      ↥(Lp ℝ 2 μ)) :
                  α →ₘ[μ] ℝ) :
              α → ℝ)
            a)
          x)
      a
h : a ∈ t
⊢ (↑‖(↑(↑(condExpIndSMul (s := s) hm hs hμs x) : α →ₘ[μ] G) : α → G) a‖₊ : ℝ≥0∞) =
    (↑‖HSMul.hSMul (α := ℝ)
            ((↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ))
                            (indicatorConstLp (s := s) 2 hs hμs 1)) :
                        ↥(Lp ℝ 2 μ)) :
                    α →ₘ[μ] ℝ) :
                α → ℝ)
              a)
            x‖₊ :
      ℝ≥0∞)
have rw : (↑(nnnorm.{u_5} (E := G)
        ((fun (a : α) ↦
            HSMul.hSMul (α := ℝ)
              ((↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ))
                              (indicatorConstLp (s := s) 2 hs hμs 1)) :
                          ↥(Lp ℝ 2 μ)) :
                      α →ₘ[μ] ℝ) :
                  α → ℝ)
                a)
              x)
          a)) :
    ℝ≥0∞) =
  (↑‖HSMul.hSMul (α := ℝ)
          ((↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) (indicatorConstLp (s := s) 2 hs hμs 1)) :
                      ↥(Lp ℝ 2 μ)) :
                  α →ₘ[μ] ℝ) :
              α → ℝ)
            a)
          x‖₊ :
    ℝ≥0∞)
Tactic: rw [ha]