awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2
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'
⊢ 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:
exact Lp.aestronglyMeasurable _

Premises used: MeasureTheory.Lp.aestronglyMeasurable
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2
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∞)

Tactic:
fun t ht hμt =>
      (setLIntegral_nnnorm_condExpL2_indicator_le hm hs hμs x ht hμt).trans ?_

Premises used: MeasureTheory.setLIntegral_nnnorm_condExpL2_indicator_le, LE.le.trans
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2
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_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∞)
⊢ ∀ (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 fun t ht hμt =>
      (setLIntegral_nnnorm_condExpL2_indicator_le hm hs hμs x ht hμt).trans ?_

Premises used: MeasureTheory.setLIntegral_nnnorm_condExpL2_indicator_le, LE.le.trans
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2
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∞)
refine_2 : s ∩ t ⊆ s
⊢ HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) (↑‖x‖₊ : ℝ≥0∞) ≤
    HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (↑‖x‖₊ : ℝ≥0∞)

Tactic:
gcongr
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2
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∞)
⊢ s ∩ t ⊆ s

Tactic:
apply Set.inter_subset_left

Premises used: Set.inter_subset_left
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2
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 (β := ℝ)
    (↑(↑(↑((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 _ _
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2
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 μ)) :
          α →ₘ[μ] ℝ) :
      α → ℝ)
    μ
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)
    μ
⊢ AEStronglyMeasurable (↑(↑(condExpIndSMul (s := s) hm hs hμs x) : α →ₘ[μ] G) : α → G) μ

Tactic:
rw [condExpIndSMul]

Premises used: MeasureTheory.condExpIndSMul
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2
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.{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:
((toSpanSingleton ℝ x).continuous.comp_aestronglyMeasurable h).congr
    (coeFn_compLpL _ _).symm

Premises used: MeasureTheory.AEStronglyMeasurable.congr, Continuous.comp_aestronglyMeasurable, Real, ContinuousLinearMap.continuous, ContinuousLinearMap.coeFn_compLpL, ContinuousLinearMap.toSpanSingleton, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2
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.{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:
exact ((toSpanSingleton ℝ x).continuous.comp_aestronglyMeasurable h).congr
    (coeFn_compLpL _ _).symm

Premises used: MeasureTheory.AEStronglyMeasurable.congr, Continuous.comp_aestronglyMeasurable, Real, ContinuousLinearMap.continuous, ContinuousLinearMap.coeFn_compLpL, ContinuousLinearMap.toSpanSingleton, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2
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 μ)))
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 μ)))
⊢ condExpIndSMul (s := s) hm hs hμs (c • x) = HSMul.hSMul (β := ↥(Lp F 2 μ)) c (condExpIndSMul (s := s) hm hs hμs x)

Tactic:
simp_rw [condExpIndSMul, toSpanSingleton_smul, smul_compLpL, smul_apply]

Premises used: ContinuousLinearMap.smul_apply, ContinuousLinearMap.toSpanSingleton_smul, MeasureTheory.condExpIndSMul, ContinuousLinearMap.smul_compLpL
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2
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
⊢ (↑(↑(condExpIndSMul (s := s) hm hs hμs x) : α →ₘ[μ] G) : α → G) =ᶠ[ae μ] fun (a : α) ↦
    HSMul.hSMul (α := ℝ)
      ((↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) (indicatorConstLp (s := s) 2 hs hμs 1)) :
                  ↥(Lp ℝ 2 μ)) :
              α →ₘ[μ] ℝ) :
          α → ℝ)
        a)
      x

Tactic:
(toSpanSingleton ℝ x).coeFn_compLpL _

Premises used: Real, MeasureTheory.AEEqFun.cast, dite, ContinuousLinearMap.coeFn_compLpL, ContinuousLinearMap.toSpanSingleton
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2
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
rw 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∞)
⊢ (↑‖(↑(↑(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∞)

Tactic:
rw [ha]
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2
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∞)
simp_rw :
  ∫⁻ (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∞)
⊢ ∫⁻ (a : α) in t,
      (↑‖HSMul.hSMul (α := ℝ)
              ((↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ))
                              (indicatorConstLp (s := s) 2 hs hμs 1)) :
                          ↥(Lp ℝ 2 μ)) :
                      α →ₘ[μ] ℝ) :
                  α → ℝ)
                a)
              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∞)

Tactic:
simp_rw [nnnorm_smul, ENNReal.coe_mul]

Premises used: nnnorm_smul, ENNReal.coe_mul
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2
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∞)
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∞)
⊢ ∫⁻ (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∞)

Tactic:
rw [lintegral_mul_const]

Premises used: MeasureTheory.lintegral_mul_const
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2
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∞)
⊢ 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:
(Lp.stronglyMeasurable _).enorm (ε := ℝ)

Premises used: MeasureTheory.Lp.stronglyMeasurable, MeasureTheory.StronglyMeasurable.enorm
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2
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∞)
⊢ 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:
exact (Lp.stronglyMeasurable _).enorm (ε := ℝ)

Premises used: MeasureTheory.Lp.stronglyMeasurable, MeasureTheory.StronglyMeasurable.enorm
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2
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∞)
grw grw₁ :
  HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) (↑‖x‖₊ : ℝ≥0∞) ≤
    HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥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∞) ≤
    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]

Premises used: MeasureTheory.lintegral_nnnorm_condExpL2_indicator_le_real
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2
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
inst_2 : SigmaFinite (μ.trim hm)
⊢ ∫⁻ (a : α), (↑‖(↑(↑(condExpIndSMul (s := s) hm hs hμs x) : α →ₘ[μ] G) : α → G) a‖₊ : ℝ≥0∞) ∂μ ≤
    HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (↑‖x‖₊ : ℝ≥0∞)

Tactic:
lintegral_le_of_forall_fin_meas_trim_le hm (μ s * ‖x‖₊) fun t ht hμt => ?_

Premises used: ENNReal.ofNNReal, HMul.hMul, NNNorm.nnnorm, MeasureTheory.lintegral_le_of_forall_fin_meas_trim_le, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2
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
inst_2 : SigmaFinite (μ.trim hm)
refine :
  ∀ (t : Set α) (ht : MeasurableSet t) (hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)),
    ∫⁻ (x_1 : α) in t, (↑‖(↑(↑(condExpIndSMul (s := s) hm hs hμs x) : α →ₘ[μ] G) : α → G) x_1‖₊ : ℝ≥0∞) ∂μ ≤
      HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (↑‖x‖₊ : ℝ≥0∞)
⊢ ∫⁻ (a : α), (↑‖(↑(↑(condExpIndSMul (s := s) hm hs hμs x) : α →ₘ[μ] G) : α → G) a‖₊ : ℝ≥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 => ?_

Premises used: ENNReal.ofNNReal, HMul.hMul, NNNorm.nnnorm, MeasureTheory.lintegral_le_of_forall_fin_meas_trim_le, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2
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
inst_2 : SigmaFinite (μ.trim hm)
t : Set α
ht : MeasurableSet t
hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ∫⁻ (x_1 : α) in t, (↑‖(↑(↑(condExpIndSMul (s := s) hm hs hμs x) : α →ₘ[μ] G) : α → G) x_1‖₊ : ℝ≥0∞) ∂μ ≤
    HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (↑‖x‖₊ : ℝ≥0∞)

Tactic:
(setLIntegral_nnnorm_condExpIndSMul_le hm hs hμs x ht hμt).trans ?_

Premises used: MeasureTheory.setLIntegral_nnnorm_condExpIndSMul_le, LE.le.trans
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2
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
inst_2 : SigmaFinite (μ.trim hm)
t : Set α
ht : MeasurableSet t
hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
refine :
  HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) (↑‖x‖₊ : ℝ≥0∞) ≤
    HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (↑‖x‖₊ : ℝ≥0∞)
⊢ ∫⁻ (x_1 : α) in t, (↑‖(↑(↑(condExpIndSMul (s := s) hm hs hμs x) : α →ₘ[μ] G) : α → G) x_1‖₊ : ℝ≥0∞) ∂μ ≤
    HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (↑‖x‖₊ : ℝ≥0∞)

Tactic:
refine (setLIntegral_nnnorm_condExpIndSMul_le hm hs hμs x ht hμt).trans ?_

Premises used: MeasureTheory.setLIntegral_nnnorm_condExpIndSMul_le, LE.le.trans