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
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
x : E'
h_comp :
  (↑(↑(compLp (toSpanSingleton ℝ x)
              (↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) (indicatorConstLp (s := s) 2 hs hμs 1)) :
                ↥(Lp ℝ 2 μ))) :
          α →ₘ[μ] E') :
      α → E') =ᶠ[ae μ]
    fun (a : α) ↦
    (toSpanSingleton ℝ x : (a : ℝ) → E')
      ((↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) (indicatorConstLp (s := s) 2 hs hμs 1)) :
                  ↥(Lp ℝ 2 μ)) :
              α →ₘ[μ] ℝ) :
          α → ℝ)
        a)
y : α
⊢ HSMul.hSMul (α := ℝ)
      ((↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) (indicatorConstLp (s := s) 2 hs hμs 1)) :
                  ↥(Lp ℝ 2 μ)) :
              α →ₘ[μ] ℝ) :
          α → ℝ)
        y)
      x =
    (toSpanSingleton ℝ x : (a : ℝ) → E')
      ((↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) (indicatorConstLp (s := s) 2 hs hμs 1)) :
                  ↥(Lp ℝ 2 μ)) :
              α →ₘ[μ] ℝ) :
          α → ℝ)
        y)

Tactic:
rfl

Premises used: MeasureTheory.AEEqFun.cast, dite, rfl
-- 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
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
x : E'
h_comp :
  (↑(↑(compLp (toSpanSingleton ℝ x)
              (↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) (indicatorConstLp (s := s) 2 hs hμs 1)) :
                ↥(Lp ℝ 2 μ))) :
          α →ₘ[μ] E') :
      α → E') =ᶠ[ae μ]
    fun (a : α) ↦
    (toSpanSingleton ℝ x : (a : ℝ) → E')
      ((↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) (indicatorConstLp (s := s) 2 hs hμs 1)) :
                  ↥(Lp ℝ 2 μ)) :
              α →ₘ[μ] ℝ) :
          α → ℝ)
        a)
h :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x_1 : α |
        (fun (x_2 : α) ↦
            Eq.{u_3 + 1} (α := E')
              ((fun (a : α) ↦
                  HSMul.hSMul (α := ℝ)
                    ((↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ))
                                    (indicatorConstLp (s := s) 2 hs hμs 1)) :
                                ↥(Lp ℝ 2 μ)) :
                            α →ₘ[μ] ℝ) :
                        α → ℝ)
                      a)
                    x)
                x_2)
              ((fun (a : α) ↦
                  ((toSpanSingleton ℝ x : (a : ℝ) → E')
                      ((↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ))
                                      (indicatorConstLp (s := s) 2 hs hμs 1)) :
                                  ↥(Lp ℝ 2 μ)) :
                              α →ₘ[μ] ℝ) :
                          α → ℝ)
                        a) :
                    E'))
                x_2))
          x_1}
      a
h₁ h₂ :
  ∀ (y : α),
    HSMul.hSMul (α := ℝ)
        ((↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) (indicatorConstLp (s := s) 2 hs hμs 1)) :
                    ↥(Lp ℝ 2 μ)) :
                α →ₘ[μ] ℝ) :
            α → ℝ)
          y)
        x =
      (toSpanSingleton ℝ x : (a : ℝ) → E')
        ((↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) (indicatorConstLp (s := s) 2 hs hμs 1)) :
                    ↥(Lp ℝ 2 μ)) :
                α →ₘ[μ] ℝ) :
            α → ℝ)
          y)
⊢ EventuallyEq.{u_1, u_3} (β := E') (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)
    fun (a : α) ↦
    (toSpanSingleton ℝ x : (a : ℝ) → E')
      ((↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) (indicatorConstLp (s := s) 2 hs hμs 1)) :
                  ↥(Lp ℝ 2 μ)) :
              α →ₘ[μ] ℝ) :
          α → ℝ)
        a)

Tactic:
filter_upwards with y using rfl

Premises used: rfl
-- 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
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 : α
ha :
  Eq.{u_3 + 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')
      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_3} (E := E')
          ((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∞)
⊢ (↑(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∞) =
    (↑‖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
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∞)
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
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∞)
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
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∞)
⊢ 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
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∞)
⊢ 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
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∞)
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
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∞)

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
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)
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∞)
⊢ ∫⁻ (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∞)

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
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∞)

Tactic:
(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
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∞)
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,
      (↑(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 (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
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∞)
bc : 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
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∞)
⊢ 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
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')
    μ

Tactic:
integrable_of_forall_fin_meas_le' hm (μ s * ‖x‖₊)
    (ENNReal.mul_lt_top hμs.lt_top ENNReal.coe_lt_top) ?_ ?_

Premises used: ENNReal.ofNNReal, HMul.hMul, MeasureTheory.integrable_of_forall_fin_meas_le', NNNorm.nnnorm, ENNReal.mul_lt_top, Ne.lt_top, DFunLike.coe, ENNReal.coe_lt_top
-- 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_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')
    μ
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∞)
⊢ 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')
    μ

Tactic:
refine integrable_of_forall_fin_meas_le' hm (μ s * ‖x‖₊)
    (ENNReal.mul_lt_top hμs.lt_top ENNReal.coe_lt_top) ?_ ?_

Premises used: ENNReal.ofNNReal, HMul.hMul, MeasureTheory.integrable_of_forall_fin_meas_le', NNNorm.nnnorm, ENNReal.mul_lt_top, Ne.lt_top, DFunLike.coe, ENNReal.coe_lt_top
-- 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:
Lp.aestronglyMeasurable _

Premises used: MeasureTheory.Lp.aestronglyMeasurable