awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.PullOut
Goal:
Ω : Type u_1
m mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_2
F : Type u_3
G : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace ℝ G
inst_6 : CompleteSpace G
B : F →L[ℝ] E →L[ℝ] G
inst_7 : CompleteSpace E
hm : m ≤ mΩ
f : SimpleFunc Ω F
g : Ω → E
hg : Integrable g μ
this :
  ∀ (s : Set Ω) (c : F) (f : Ω → E),
    Eq (α := (ω : Ω) → G)
      (fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) (s.indicator (Function.const Ω c) ω) : E →L[ℝ] G) : (a : E) → G) (f ω))
      (s.indicator fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) c : E →L[ℝ] G) : (a : E) → G) (f ω))
g₁ g₂ : SimpleFunc Ω F
h :
  Disjoint.{u_1} (α := Set Ω) (Function.support.{u_1, u_3} (M := F) (⇑g₁ : (a : Ω) → F))
    (Function.support.{u_1, u_3} (M := F) (⇑g₂ : (a : Ω) → F))
h_eq₁ :
  (fun (f : SimpleFunc Ω F) ↦
      EventuallyEq.{u_1, u_4} (β := G) (ae μ)
        μ[fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) ((f : (a : Ω) → F) ω) : E →L[ℝ] G) : (a : E) → G) (g ω) | m]
        fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) ((f : (a : Ω) → F) ω) : E →L[ℝ] G) : (a : E) → G) (μ[g | m] ω))
    g₁
h_eq₂ :
  (fun (f : SimpleFunc Ω F) ↦
      EventuallyEq.{u_1, u_4} (β := G) (ae μ)
        μ[fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) ((f : (a : Ω) → F) ω) : E →L[ℝ] G) : (a : E) → G) (g ω) | m]
        fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) ((f : (a : Ω) → F) ω) : E →L[ℝ] G) : (a : E) → G) (μ[g | m] ω))
    g₂
⊢ (⇑(g₁ + g₂) : (a : Ω) → F) = HAdd.hAdd (α := (a : Ω) → F) (⇑g₁ : (a : Ω) → F) (⇑g₂ : (a : Ω) → F)

Tactic:
have h_add := @SimpleFunc.coe_add _ _ m _ g₁ g₂
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.PullOut
Goal:
Ω : Type u_1
m mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_2
F : Type u_3
G : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace ℝ G
inst_6 : CompleteSpace G
B : F →L[ℝ] E →L[ℝ] G
inst_7 : CompleteSpace E
hm : m ≤ mΩ
f : SimpleFunc Ω F
g : Ω → E
hg : Integrable g μ
this :
  ∀ (s : Set Ω) (c : F) (f : Ω → E),
    Eq (α := (ω : Ω) → G)
      (fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) (s.indicator (Function.const Ω c) ω) : E →L[ℝ] G) : (a : E) → G) (f ω))
      (s.indicator fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) c : E →L[ℝ] G) : (a : E) → G) (f ω))
g₁ g₂ : SimpleFunc Ω F
h :
  Disjoint.{u_1} (α := Set Ω) (Function.support.{u_1, u_3} (M := F) (⇑g₁ : (a : Ω) → F))
    (Function.support.{u_1, u_3} (M := F) (⇑g₂ : (a : Ω) → F))
h_eq₁ :
  (fun (f : SimpleFunc Ω F) ↦
      EventuallyEq.{u_1, u_4} (β := G) (ae μ)
        μ[fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) ((f : (a : Ω) → F) ω) : E →L[ℝ] G) : (a : E) → G) (g ω) | m]
        fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) ((f : (a : Ω) → F) ω) : E →L[ℝ] G) : (a : E) → G) (μ[g | m] ω))
    g₁
h_eq₂ :
  (fun (f : SimpleFunc Ω F) ↦
      EventuallyEq.{u_1, u_4} (β := G) (ae μ)
        μ[fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) ((f : (a : Ω) → F) ω) : E →L[ℝ] G) : (a : E) → G) (g ω) | m]
        fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) ((f : (a : Ω) → F) ω) : E →L[ℝ] G) : (a : E) → G) (μ[g | m] ω))
    g₂
h_add : (⇑(g₁ + g₂) : (a : Ω) → F) = HAdd.hAdd (α := (a : Ω) → F) (⇑g₁ : (a : Ω) → F) (⇑g₂ : (a : Ω) → F)
simp_rw :
  μ[fun (ω : Ω) ↦
      (HAdd.hAdd (α := E →L[ℝ] G) (β := E →L[ℝ] G) ((B : (a : F) → E →L[ℝ] G) ((g₁ : (a : Ω) → F) ω) : E →L[ℝ] G)
            ((B : (a : F) → E →L[ℝ] G) ((g₂ : (a : Ω) → F) ω) : E →L[ℝ] G) :
          (a : E) → G)
        (g ω) |
      m] =ᶠ[ae μ]
    HAdd.hAdd (α := Ω → G)
      μ[fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) ((g₁ : (a : Ω) → F) ω) : E →L[ℝ] G) : (a : E) → G) (g ω) | m]
      μ[fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) ((g₂ : (a : Ω) → F) ω) : E →L[ℝ] G) : (a : E) → G) (g ω) | m]
⊢ μ[fun (ω : Ω) ↦
      (((B : (a : F) → E →L[ℝ] G) (HAdd.hAdd (α := F) (β := F) ((g₁ : (a : Ω) → F) ω : F) ((g₂ : (a : Ω) → F) ω : F)) :
            E →L[ℝ] G) :
          (a : E) → G)
        (g ω) |
      m] =ᶠ[ae μ]
    HAdd.hAdd (α := Ω → G)
      μ[fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) ((g₁ : (a : Ω) → F) ω) : E →L[ℝ] G) : (a : E) → G) (g ω) | m]
      μ[fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) ((g₂ : (a : Ω) → F) ω) : E →L[ℝ] G) : (a : E) → G) (g ω) | m]

Tactic:
simp_rw [B.map_add]

Premises used: ContinuousLinearMap.map_add
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.PullOut
Goal:
Ω : Type u_1
m mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_2
F : Type u_3
G : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace ℝ G
inst_6 : CompleteSpace G
B : F →L[ℝ] E →L[ℝ] G
inst_7 : CompleteSpace E
hm : m ≤ mΩ
f : SimpleFunc Ω F
g : Ω → E
hg : Integrable g μ
this :
  ∀ (s : Set Ω) (c : F) (f : Ω → E),
    Eq (α := (ω : Ω) → G)
      (fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) (s.indicator (Function.const Ω c) ω) : E →L[ℝ] G) : (a : E) → G) (f ω))
      (s.indicator fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) c : E →L[ℝ] G) : (a : E) → G) (f ω))
g₁ g₂ : SimpleFunc Ω F
h :
  Disjoint.{u_1} (α := Set Ω) (Function.support.{u_1, u_3} (M := F) (⇑g₁ : (a : Ω) → F))
    (Function.support.{u_1, u_3} (M := F) (⇑g₂ : (a : Ω) → F))
h_eq₁ :
  (fun (f : SimpleFunc Ω F) ↦
      EventuallyEq.{u_1, u_4} (β := G) (ae μ)
        μ[fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) ((f : (a : Ω) → F) ω) : E →L[ℝ] G) : (a : E) → G) (g ω) | m]
        fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) ((f : (a : Ω) → F) ω) : E →L[ℝ] G) : (a : E) → G) (μ[g | m] ω))
    g₁
h_eq₂ :
  (fun (f : SimpleFunc Ω F) ↦
      EventuallyEq.{u_1, u_4} (β := G) (ae μ)
        μ[fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) ((f : (a : Ω) → F) ω) : E →L[ℝ] G) : (a : E) → G) (g ω) | m]
        fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) ((f : (a : Ω) → F) ω) : E →L[ℝ] G) : (a : E) → G) (μ[g | m] ω))
    g₂
h_add : (⇑(g₁ + g₂) : (a : Ω) → F) = HAdd.hAdd (α := (a : Ω) → F) (⇑g₁ : (a : Ω) → F) (⇑g₂ : (a : Ω) → F)
obtain :
  ∀ (C₁ : ℝ) (hC₁ : ∀ (x : Ω), norm.{u_3} (E := F) ((g₁ : (a : Ω) → F) x : F) ≤ C₁),
    μ[fun (ω : Ω) ↦
        (HAdd.hAdd (α := E →L[ℝ] G) (β := E →L[ℝ] G) ((B : (a : F) → E →L[ℝ] G) ((g₁ : (a : Ω) → F) ω) : E →L[ℝ] G)
              ((B : (a : F) → E →L[ℝ] G) ((g₂ : (a : Ω) → F) ω) : E →L[ℝ] G) :
            (a : E) → G)
          (g ω) |
        m] =ᶠ[ae μ]
      HAdd.hAdd (α := Ω → G)
        μ[fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) ((g₁ : (a : Ω) → F) ω) : E →L[ℝ] G) : (a : E) → G) (g ω) | m]
        μ[fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) ((g₂ : (a : Ω) → F) ω) : E →L[ℝ] G) : (a : E) → G) (g ω) | m]
⊢ μ[fun (ω : Ω) ↦
      (HAdd.hAdd (α := E →L[ℝ] G) (β := E →L[ℝ] G) ((B : (a : F) → E →L[ℝ] G) ((g₁ : (a : Ω) → F) ω) : E →L[ℝ] G)
            ((B : (a : F) → E →L[ℝ] G) ((g₂ : (a : Ω) → F) ω) : E →L[ℝ] G) :
          (a : E) → G)
        (g ω) |
      m] =ᶠ[ae μ]
    HAdd.hAdd (α := Ω → G)
      μ[fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) ((g₁ : (a : Ω) → F) ω) : E →L[ℝ] G) : (a : E) → G) (g ω) | m]
      μ[fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) ((g₂ : (a : Ω) → F) ω) : E →L[ℝ] G) : (a : E) → G) (g ω) | m]

Tactic:
obtain ⟨C₁, hC₁⟩ := @SimpleFunc.exists_forall_norm_le _ _ m _ g₁

Premises used: MeasureTheory.SimpleFunc.exists_forall_norm_le
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.PullOut
Goal:
Ω : Type u_1
m mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_2
F : Type u_3
G : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace ℝ G
inst_6 : CompleteSpace G
B : F →L[ℝ] E →L[ℝ] G
inst_7 : CompleteSpace E
hm : m ≤ mΩ
f : SimpleFunc Ω F
g : Ω → E
hg : Integrable g μ
this :
  ∀ (s : Set Ω) (c : F) (f : Ω → E),
    Eq (α := (ω : Ω) → G)
      (fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) (s.indicator (Function.const Ω c) ω) : E →L[ℝ] G) : (a : E) → G) (f ω))
      (s.indicator fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) c : E →L[ℝ] G) : (a : E) → G) (f ω))
g₁ g₂ : SimpleFunc Ω F
h :
  Disjoint.{u_1} (α := Set Ω) (Function.support.{u_1, u_3} (M := F) (⇑g₁ : (a : Ω) → F))
    (Function.support.{u_1, u_3} (M := F) (⇑g₂ : (a : Ω) → F))
h_eq₁ :
  (fun (f : SimpleFunc Ω F) ↦
      EventuallyEq.{u_1, u_4} (β := G) (ae μ)
        μ[fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) ((f : (a : Ω) → F) ω) : E →L[ℝ] G) : (a : E) → G) (g ω) | m]
        fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) ((f : (a : Ω) → F) ω) : E →L[ℝ] G) : (a : E) → G) (μ[g | m] ω))
    g₁
h_eq₂ :
  (fun (f : SimpleFunc Ω F) ↦
      EventuallyEq.{u_1, u_4} (β := G) (ae μ)
        μ[fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) ((f : (a : Ω) → F) ω) : E →L[ℝ] G) : (a : E) → G) (g ω) | m]
        fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) ((f : (a : Ω) → F) ω) : E →L[ℝ] G) : (a : E) → G) (μ[g | m] ω))
    g₂
h_add : (⇑(g₁ + g₂) : (a : Ω) → F) = HAdd.hAdd (α := (a : Ω) → F) (⇑g₁ : (a : Ω) → F) (⇑g₂ : (a : Ω) → F)
C₁ : ℝ
hC₁ : ∀ (x : Ω), norm.{u_3} (E := F) ((g₁ : (a : Ω) → F) x : F) ≤ C₁
obtain :
  ∀ (C₂ : ℝ) (hC₂ : ∀ (x : Ω), norm.{u_3} (E := F) ((g₂ : (a : Ω) → F) x : F) ≤ C₂),
    μ[fun (ω : Ω) ↦
        (HAdd.hAdd (α := E →L[ℝ] G) (β := E →L[ℝ] G) ((B : (a : F) → E →L[ℝ] G) ((g₁ : (a : Ω) → F) ω) : E →L[ℝ] G)
              ((B : (a : F) → E →L[ℝ] G) ((g₂ : (a : Ω) → F) ω) : E →L[ℝ] G) :
            (a : E) → G)
          (g ω) |
        m] =ᶠ[ae μ]
      HAdd.hAdd (α := Ω → G)
        μ[fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) ((g₁ : (a : Ω) → F) ω) : E →L[ℝ] G) : (a : E) → G) (g ω) | m]
        μ[fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) ((g₂ : (a : Ω) → F) ω) : E →L[ℝ] G) : (a : E) → G) (g ω) | m]
⊢ μ[fun (ω : Ω) ↦
      (HAdd.hAdd (α := E →L[ℝ] G) (β := E →L[ℝ] G) ((B : (a : F) → E →L[ℝ] G) ((g₁ : (a : Ω) → F) ω) : E →L[ℝ] G)
            ((B : (a : F) → E →L[ℝ] G) ((g₂ : (a : Ω) → F) ω) : E →L[ℝ] G) :
          (a : E) → G)
        (g ω) |
      m] =ᶠ[ae μ]
    HAdd.hAdd (α := Ω → G)
      μ[fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) ((g₁ : (a : Ω) → F) ω) : E →L[ℝ] G) : (a : E) → G) (g ω) | m]
      μ[fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) ((g₂ : (a : Ω) → F) ω) : E →L[ℝ] G) : (a : E) → G) (g ω) | m]

Tactic:
obtain ⟨C₂, hC₂⟩ := @SimpleFunc.exists_forall_norm_le _ _ m _ g₂

Premises used: MeasureTheory.SimpleFunc.exists_forall_norm_le
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.PullOut
Goal:
Ω : Type u_1
m mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_2
F : Type u_3
G : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace ℝ G
inst_6 : CompleteSpace G
B : F →L[ℝ] E →L[ℝ] G
inst_7 : CompleteSpace E
hm : m ≤ mΩ
f : SimpleFunc Ω F
g : Ω → E
hg : Integrable g μ
this :
  ∀ (s : Set Ω) (c : F) (f : Ω → E),
    Eq (α := (ω : Ω) → G)
      (fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) (s.indicator (Function.const Ω c) ω) : E →L[ℝ] G) : (a : E) → G) (f ω))
      (s.indicator fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) c : E →L[ℝ] G) : (a : E) → G) (f ω))
g₁ g₂ : SimpleFunc Ω F
h :
  Disjoint.{u_1} (α := Set Ω) (Function.support.{u_1, u_3} (M := F) (⇑g₁ : (a : Ω) → F))
    (Function.support.{u_1, u_3} (M := F) (⇑g₂ : (a : Ω) → F))
h_eq₁ :
  (fun (f : SimpleFunc Ω F) ↦
      EventuallyEq.{u_1, u_4} (β := G) (ae μ)
        μ[fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) ((f : (a : Ω) → F) ω) : E →L[ℝ] G) : (a : E) → G) (g ω) | m]
        fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) ((f : (a : Ω) → F) ω) : E →L[ℝ] G) : (a : E) → G) (μ[g | m] ω))
    g₁
h_eq₂ :
  (fun (f : SimpleFunc Ω F) ↦
      EventuallyEq.{u_1, u_4} (β := G) (ae μ)
        μ[fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) ((f : (a : Ω) → F) ω) : E →L[ℝ] G) : (a : E) → G) (g ω) | m]
        fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) ((f : (a : Ω) → F) ω) : E →L[ℝ] G) : (a : E) → G) (μ[g | m] ω))
    g₂
h_add : (⇑(g₁ + g₂) : (a : Ω) → F) = HAdd.hAdd (α := (a : Ω) → F) (⇑g₁ : (a : Ω) → F) (⇑g₂ : (a : Ω) → F)
C₁ : ℝ
hC₁ : ∀ (x : Ω), norm.{u_3} (E := F) ((g₁ : (a : Ω) → F) x : F) ≤ C₁
C₂ : ℝ
hC₂ : ∀ (x : Ω), norm.{u_3} (E := F) ((g₂ : (a : Ω) → F) x : F) ≤ C₂
⊢ μ[fun (ω : Ω) ↦
      (HAdd.hAdd (α := E →L[ℝ] G) (β := E →L[ℝ] G) ((B : (a : F) → E →L[ℝ] G) ((g₁ : (a : Ω) → F) ω) : E →L[ℝ] G)
            ((B : (a : F) → E →L[ℝ] G) ((g₂ : (a : Ω) → F) ω) : E →L[ℝ] G) :
          (a : E) → G)
        (g ω) |
      m] =ᶠ[ae μ]
    HAdd.hAdd (α := Ω → G)
      μ[fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) ((g₁ : (a : Ω) → F) ω) : E →L[ℝ] G) : (a : E) → G) (g ω) | m]
      μ[fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) ((g₂ : (a : Ω) → F) ω) : E →L[ℝ] G) : (a : E) → G) (g ω) | m]

Tactic:
condExp_add
          (B.integrable_of_bilin_of_bdd_left C₁ (g₁.stronglyMeasurable.mono hm).aestronglyMeasurable
            (ae_of_all _ hC₁) hg)
          (B.integrable_of_bilin_of_bdd_left C₂ (g₂.stronglyMeasurable.mono hm).aestronglyMeasurable
            (ae_of_all _ hC₂) hg) m

Premises used: ContinuousLinearMap.integrable_of_bilin_of_bdd_left, MeasureTheory.StronglyMeasurable.aestronglyMeasurable, MeasureTheory.condExp_add, MeasureTheory.ae_of_all, MeasureTheory.StronglyMeasurable.mono, MeasureTheory.SimpleFunc.stronglyMeasurable
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.PullOut
Goal:
Ω : Type u_1
m mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_2
F : Type u_3
G : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace ℝ G
inst_6 : CompleteSpace G
B : F →L[ℝ] E →L[ℝ] G
inst_7 : CompleteSpace E
hm : m ≤ mΩ
f : SimpleFunc Ω F
g : Ω → E
hg : Integrable g μ
this :
  ∀ (s : Set Ω) (c : F) (f : Ω → E),
    Eq (α := (ω : Ω) → G)
      (fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) (s.indicator (Function.const Ω c) ω) : E →L[ℝ] G) : (a : E) → G) (f ω))
      (s.indicator fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) c : E →L[ℝ] G) : (a : E) → G) (f ω))
g₁ g₂ : SimpleFunc Ω F
h :
  Disjoint.{u_1} (α := Set Ω) (Function.support.{u_1, u_3} (M := F) (⇑g₁ : (a : Ω) → F))
    (Function.support.{u_1, u_3} (M := F) (⇑g₂ : (a : Ω) → F))
h_eq₁ :
  (fun (f : SimpleFunc Ω F) ↦
      EventuallyEq.{u_1, u_4} (β := G) (ae μ)
        μ[fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) ((f : (a : Ω) → F) ω) : E →L[ℝ] G) : (a : E) → G) (g ω) | m]
        fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) ((f : (a : Ω) → F) ω) : E →L[ℝ] G) : (a : E) → G) (μ[g | m] ω))
    g₁
h_eq₂ :
  (fun (f : SimpleFunc Ω F) ↦
      EventuallyEq.{u_1, u_4} (β := G) (ae μ)
        μ[fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) ((f : (a : Ω) → F) ω) : E →L[ℝ] G) : (a : E) → G) (g ω) | m]
        fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) ((f : (a : Ω) → F) ω) : E →L[ℝ] G) : (a : E) → G) (μ[g | m] ω))
    g₂
h_add : (⇑(g₁ + g₂) : (a : Ω) → F) = HAdd.hAdd (α := (a : Ω) → F) (⇑g₁ : (a : Ω) → F) (⇑g₂ : (a : Ω) → F)
C₁ : ℝ
hC₁ : ∀ (x : Ω), norm.{u_3} (E := F) ((g₁ : (a : Ω) → F) x : F) ≤ C₁
C₂ : ℝ
hC₂ : ∀ (x : Ω), norm.{u_3} (E := F) ((g₂ : (a : Ω) → F) x : F) ≤ C₂
⊢ μ[fun (ω : Ω) ↦
      (HAdd.hAdd (α := E →L[ℝ] G) (β := E →L[ℝ] G) ((B : (a : F) → E →L[ℝ] G) ((g₁ : (a : Ω) → F) ω) : E →L[ℝ] G)
            ((B : (a : F) → E →L[ℝ] G) ((g₂ : (a : Ω) → F) ω) : E →L[ℝ] G) :
          (a : E) → G)
        (g ω) |
      m] =ᶠ[ae μ]
    HAdd.hAdd (α := Ω → G)
      μ[fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) ((g₁ : (a : Ω) → F) ω) : E →L[ℝ] G) : (a : E) → G) (g ω) | m]
      μ[fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) ((g₂ : (a : Ω) → F) ω) : E →L[ℝ] G) : (a : E) → G) (g ω) | m]

Tactic:
exact condExp_add
          (B.integrable_of_bilin_of_bdd_left C₁ (g₁.stronglyMeasurable.mono hm).aestronglyMeasurable
            (ae_of_all _ hC₁) hg)
          (B.integrable_of_bilin_of_bdd_left C₂ (g₂.stronglyMeasurable.mono hm).aestronglyMeasurable
            (ae_of_all _ hC₂) hg) m

Premises used: ContinuousLinearMap.integrable_of_bilin_of_bdd_left, MeasureTheory.StronglyMeasurable.aestronglyMeasurable, MeasureTheory.condExp_add, MeasureTheory.ae_of_all, MeasureTheory.StronglyMeasurable.mono, MeasureTheory.SimpleFunc.stronglyMeasurable
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.PullOut
Goal:
Ω : Type u_1
m mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_2
F : Type u_3
G : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace ℝ G
inst_6 : CompleteSpace G
B : F →L[ℝ] E →L[ℝ] G
inst_7 : CompleteSpace E
hm : m ≤ mΩ
f : SimpleFunc Ω F
g : Ω → E
hg : Integrable g μ
this :
  ∀ (s : Set Ω) (c : F) (f : Ω → E),
    Eq (α := (ω : Ω) → G)
      (fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) (s.indicator (Function.const Ω c) ω) : E →L[ℝ] G) : (a : E) → G) (f ω))
      (s.indicator fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) c : E →L[ℝ] G) : (a : E) → G) (f ω))
g₁ g₂ : SimpleFunc Ω F
h :
  Disjoint.{u_1} (α := Set Ω) (Function.support.{u_1, u_3} (M := F) (⇑g₁ : (a : Ω) → F))
    (Function.support.{u_1, u_3} (M := F) (⇑g₂ : (a : Ω) → F))
h_eq₁ :
  (fun (f : SimpleFunc Ω F) ↦
      EventuallyEq.{u_1, u_4} (β := G) (ae μ)
        μ[fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) ((f : (a : Ω) → F) ω) : E →L[ℝ] G) : (a : E) → G) (g ω) | m]
        fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) ((f : (a : Ω) → F) ω) : E →L[ℝ] G) : (a : E) → G) (μ[g | m] ω))
    g₁
h_eq₂ :
  (fun (f : SimpleFunc Ω F) ↦
      EventuallyEq.{u_1, u_4} (β := G) (ae μ)
        μ[fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) ((f : (a : Ω) → F) ω) : E →L[ℝ] G) : (a : E) → G) (g ω) | m]
        fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) ((f : (a : Ω) → F) ω) : E →L[ℝ] G) : (a : E) → G) (μ[g | m] ω))
    g₂
h_add : (⇑(g₁ + g₂) : (a : Ω) → F) = HAdd.hAdd (α := (a : Ω) → F) (⇑g₁ : (a : Ω) → F) (⇑g₂ : (a : Ω) → F)
⊢ HAdd.hAdd (α := Ω → G)
      μ[fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) ((g₁ : (a : Ω) → F) ω) : E →L[ℝ] G) : (a : E) → G) (g ω) | m]
      μ[fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) ((g₂ : (a : Ω) → F) ω) : E →L[ℝ] G) : (a : E) → G) (g ω) | m] =ᶠ[ae μ]
    fun (ω : Ω) ↦
    HAdd.hAdd (α := G) (β := G)
      ((((B : (a : F) → E →L[ℝ] G) ((g₁ : (a : Ω) → F) ω) : E →L[ℝ] G) : (a : E) → G) (μ[g | m] ω) : G)
      ((((B : (a : F) → E →L[ℝ] G) ((g₂ : (a : Ω) → F) ω) : E →L[ℝ] G) : (a : E) → G) (μ[g | m] ω) : G)

Tactic:
EventuallyEq.add h_eq₁ h_eq₂

Premises used: Filter.EventuallyEq.add
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.PullOut
Goal:
Ω : Type u_1
m mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_2
F : Type u_3
G : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace ℝ G
inst_6 : CompleteSpace G
B : F →L[ℝ] E →L[ℝ] G
inst_7 : CompleteSpace E
hm : m ≤ mΩ
f : SimpleFunc Ω F
g : Ω → E
hg : Integrable g μ
this :
  ∀ (s : Set Ω) (c : F) (f : Ω → E),
    Eq (α := (ω : Ω) → G)
      (fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) (s.indicator (Function.const Ω c) ω) : E →L[ℝ] G) : (a : E) → G) (f ω))
      (s.indicator fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) c : E →L[ℝ] G) : (a : E) → G) (f ω))
g₁ g₂ : SimpleFunc Ω F
h :
  Disjoint.{u_1} (α := Set Ω) (Function.support.{u_1, u_3} (M := F) (⇑g₁ : (a : Ω) → F))
    (Function.support.{u_1, u_3} (M := F) (⇑g₂ : (a : Ω) → F))
h_eq₁ :
  (fun (f : SimpleFunc Ω F) ↦
      EventuallyEq.{u_1, u_4} (β := G) (ae μ)
        μ[fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) ((f : (a : Ω) → F) ω) : E →L[ℝ] G) : (a : E) → G) (g ω) | m]
        fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) ((f : (a : Ω) → F) ω) : E →L[ℝ] G) : (a : E) → G) (μ[g | m] ω))
    g₁
h_eq₂ :
  (fun (f : SimpleFunc Ω F) ↦
      EventuallyEq.{u_1, u_4} (β := G) (ae μ)
        μ[fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) ((f : (a : Ω) → F) ω) : E →L[ℝ] G) : (a : E) → G) (g ω) | m]
        fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) ((f : (a : Ω) → F) ω) : E →L[ℝ] G) : (a : E) → G) (μ[g | m] ω))
    g₂
h_add : (⇑(g₁ + g₂) : (a : Ω) → F) = HAdd.hAdd (α := (a : Ω) → F) (⇑g₁ : (a : Ω) → F) (⇑g₂ : (a : Ω) → F)
⊢ EventuallyEq.{u_1, u_4} (β := G) (ae μ)
    (fun (ω : Ω) ↦
      HAdd.hAdd (α := G) (β := G)
        ((((B : (a : F) → E →L[ℝ] G) ((g₁ : (a : Ω) → F) ω) : E →L[ℝ] G) : (a : E) → G) (μ[g | m] ω) : G)
        ((((B : (a : F) → E →L[ℝ] G) ((g₂ : (a : Ω) → F) ω) : E →L[ℝ] G) : (a : E) → G) (μ[g | m] ω) : G))
    fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) ((g₁ + g₂ : (a : Ω) → F) ω) : E →L[ℝ] G) : (a : E) → G) (μ[g | m] ω)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.PullOut
Goal:
Ω : Type u_1
m mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_2
F : Type u_3
G : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace ℝ G
inst_6 : CompleteSpace G
B : F →L[ℝ] E →L[ℝ] G
inst_7 : CompleteSpace E
hm : m ≤ mΩ
inst_8 : IsFiniteMeasure μ
f : Ω → F
g : Ω → E
hf : StronglyMeasurable f
hg : Integrable g μ
c : ℝ
hf_bound : ∀ᵐ (ω : Ω) ∂μ, ‖f ω‖ ≤ c
fs : ℕ → SimpleFunc Ω F := hf.approxBounded c
⊢ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun (x : ℕ) ↦ (fs x : (a : Ω) → F) ω) atTop (𝓝 (f ω))

Tactic:
have hfs_tendsto : ∀ᵐ ω ∂μ, Tendsto (fs · ω) atTop (𝓝 (f ω)) :=
    hf.tendsto_approxBounded_ae hf_bound
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.PullOut
Goal:
Ω : Type u_1
m mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_2
F : Type u_3
G : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace ℝ G
inst_6 : CompleteSpace G
B : F →L[ℝ] E →L[ℝ] G
inst_7 : CompleteSpace E
hm : m ≤ mΩ
inst_8 : IsFiniteMeasure μ
f : Ω → F
g : Ω → E
hf : StronglyMeasurable f
hg : Integrable g μ
c : ℝ
hf_bound : ∀ᵐ (ω : Ω) ∂μ, ‖f ω‖ ≤ c
fs : ℕ → SimpleFunc Ω F := hf.approxBounded c
hfs_tendsto : ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun (x : ℕ) ↦ (fs x : (a : Ω) → F) ω) atTop (𝓝 (f ω))
pos :
  ∀ (hμ : μ = 0),
    EventuallyEq.{u_1, u_4} (β := G) (ae μ)
      μ[fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) (f ω) : E →L[ℝ] G) : (a : E) → G) (g ω) | m] fun (ω : Ω) ↦
      (((B : (a : F) → E →L[ℝ] G) (f ω) : E →L[ℝ] G) : (a : E) → G) (μ[g | m] ω)
neg :
  ∀ (hμ : ¬μ = 0),
    EventuallyEq.{u_1, u_4} (β := G) (ae μ)
      μ[fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) (f ω) : E →L[ℝ] G) : (a : E) → G) (g ω) | m] fun (ω : Ω) ↦
      (((B : (a : F) → E →L[ℝ] G) (f ω) : E →L[ℝ] G) : (a : E) → G) (μ[g | m] ω)
⊢ EventuallyEq.{u_1, u_4} (β := G) (ae μ)
    μ[fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) (f ω) : E →L[ℝ] G) : (a : E) → G) (g ω) | m] fun (ω : Ω) ↦
    (((B : (a : F) → E →L[ℝ] G) (f ω) : E →L[ℝ] G) : (a : E) → G) (μ[g | m] ω)

Tactic:
by_cases hμ : μ = 0
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.PullOut
Goal:
Ω : Type u_1
m mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_2
F : Type u_3
G : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace ℝ G
inst_6 : CompleteSpace G
B : F →L[ℝ] E →L[ℝ] G
inst_7 : CompleteSpace E
hm : m ≤ mΩ
inst_8 : IsFiniteMeasure μ
f : Ω → F
g : Ω → E
hf : StronglyMeasurable f
hg : Integrable g μ
c : ℝ
hf_bound : ∀ᵐ (ω : Ω) ∂μ, ‖f ω‖ ≤ c
fs : ℕ → SimpleFunc Ω F := hf.approxBounded c
hfs_tendsto : ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun (x : ℕ) ↦ (fs x : (a : Ω) → F) ω) atTop (𝓝 (f ω))
hμ : μ = 0
pos :
  EventuallyEq.{u_1, u_4} (β := G) ⊥
    (condExp m (m₀ := mΩ) 0 fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) (f ω) : E →L[ℝ] G) : (a : E) → G) (g ω))
    fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) (f ω) : E →L[ℝ] G) : (a : E) → G) (condExp m (m₀ := mΩ) 0 g ω)
⊢ EventuallyEq.{u_1, u_4} (β := G) (ae μ)
    μ[fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) (f ω) : E →L[ℝ] G) : (a : E) → G) (g ω) | m] fun (ω : Ω) ↦
    (((B : (a : F) → E →L[ℝ] G) (f ω) : E →L[ℝ] G) : (a : E) → G) (μ[g | m] ω)

Tactic:
simp only [hμ, ae_zero]

Premises used: MeasureTheory.ae_zero