awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.LebesgueBochner (goal)
Goal:
𝓧 : Type u_1
m m𝓧 : MeasurableSpace 𝓧
μ : Measure 𝓧
f : 𝓧 → ℝ≥0∞
hf_meas : AEMeasurable f μ
hf : ∫⁻ (x : 𝓧), f x ∂μ ≠ ∞
hm : m ≤ m𝓧
hμ : SigmaFinite (μ.trim hm)
⊢ ∀ (s : Set 𝓧),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set 𝓧) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        IntegrableOn (ε := ℝ) (fun (x : 𝓧) ↦ (μ⁻[f|m] x).toReal) s μ
have pos : ∀ (s : Set 𝓧) (hs : MeasurableSet s) (hsμ : LT.lt (α := ℝ≥0∞) ((μ : (a : Set 𝓧) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
  Integrable (ε := ℝ) (fun (x : 𝓧) ↦ (μ⁻[f|m] x).toReal) μ
Tactic: refine fun s hs hsμ ↦ Integrable.integrableOn ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.LebesgueBochner (goal)
Goal:
𝓧 : Type u_1
m m𝓧 : MeasurableSpace 𝓧
μ : Measure 𝓧
f : 𝓧 → ℝ≥0∞
hf_meas : AEMeasurable f μ
hf : ∫⁻ (x : 𝓧), f x ∂μ ≠ ∞
hm : m ≤ m𝓧
hμ : SigmaFinite (μ.trim hm)
s : Set 𝓧
hs : MeasurableSet s
hsμ : LT.lt (α := ℝ≥0∞) ((μ : (a : Set 𝓧) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Integrable (ε := ℝ) (fun (x : 𝓧) ↦ (μ⁻[f|m] x).toReal) μ
have pos : ∫⁻ (x : 𝓧), μ⁻[f|m] x ∂μ ≠ ∞
Tactic: rwa [integrable_toReal_iff (by fun_prop) (condLExp_ne_top hf), lintegral_condLExp]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.LebesgueBochner (goal)
Goal:
𝓧 : Type u_1
m m𝓧 : MeasurableSpace 𝓧
μ : Measure 𝓧
f : 𝓧 → ℝ≥0∞
hf_meas : AEMeasurable f μ
hf : ∫⁻ (x : 𝓧), f x ∂μ ≠ ∞
hm : m ≤ m𝓧
hμ : SigmaFinite (μ.trim hm)
s : Set 𝓧
hs : MeasurableSet s
hsμ : LT.lt (α := ℝ≥0∞) ((μ : (a : Set 𝓧) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Eq (α := ℝ) (∫ (x : 𝓧) in s, (μ⁻[f|m] x).toReal ∂μ) (∫ (x : 𝓧) in s, (f x).toReal ∂μ)
have pos : ∀ᵐ (x : 𝓧) ∂μ.restrict s, f x < ∞
Tactic: rw [integral_toReal (by fun_prop), integral_toReal (by fun_prop),
      setLIntegral_condLExp _ _ _ hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.LebesgueBochner (goal)
Goal:
𝓧 : Type u_1
m m𝓧 : MeasurableSpace 𝓧
μ : Measure 𝓧
f : 𝓧 → ℝ≥0∞
hf_meas : AEMeasurable f μ
hf : ∫⁻ (x : 𝓧), f x ∂μ ≠ ∞
hm : m ≤ m𝓧
hμ : SigmaFinite (μ.trim hm)
s : Set 𝓧
hs : MeasurableSet s
hsμ : LT.lt (α := ℝ≥0∞) ((μ : (a : Set 𝓧) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
pos : ∀ᵐ (x : 𝓧) ∂μ.restrict s, f x < ∞
⊢ Eq (α := ℝ) (∫ (x : 𝓧) in s, (μ⁻[f|m] x).toReal ∂μ) (∫ (x : 𝓧) in s, (f x).toReal ∂μ)
have pos₁ : ∀ᵐ (x : 𝓧) ∂μ.restrict s, μ⁻[f|m] x < ∞
Tactic: rw [integral_toReal (by fun_prop), integral_toReal (by fun_prop),
      setLIntegral_condLExp _ _ _ hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.PullOut (goal)
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_1 : SimpleFunc Ω F
g : Ω → E
hg : Integrable g μ
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 ω))
have h : ∀ (ω : Ω),
  Eq.{u_4 + 1} (α := G)
    ((((B : (a : F) → E →L[ℝ] G) (s.indicator (Function.const Ω c) ω) : E →L[ℝ] G) : (a : E) → G) (f ω) : G)
    (s.indicator (fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) c : E →L[ℝ] G) : (a : E) → G) (f ω)) ω : G)
Tactic: ext ω
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.PullOut (goal)
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_1 : SimpleFunc Ω F
g : Ω → E
hg : Integrable g μ
s : Set Ω
c : F
f : Ω → E
ω : Ω
⊢ Eq.{u_4 + 1} (α := G)
    ((((B : (a : F) → E →L[ℝ] G) (s.indicator (Function.const Ω c) ω) : E →L[ℝ] G) : (a : E) → G) (f ω) : G)
    (s.indicator (fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) c : E →L[ℝ] G) : (a : E) → G) (f ω)) ω : G)
have pos : ∀ (hω : ω ∈ s),
  Eq.{u_4 + 1} (α := G)
    ((((B : (a : F) → E →L[ℝ] G) (s.indicator (Function.const Ω c) ω) : E →L[ℝ] G) : (a : E) → G) (f ω) : G)
    (s.indicator (fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) c : E →L[ℝ] G) : (a : E) → G) (f ω)) ω : G)
Tactic: by_cases hω : ω ∈ s
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.PullOut (goal)
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_1 : SimpleFunc Ω F
g : Ω → E
hg : Integrable g μ
s : Set Ω
c : F
f : Ω → E
ω : Ω
pos :
  ∀ (hω : ω ∈ s),
    Eq.{u_4 + 1} (α := G)
      ((((B : (a : F) → E →L[ℝ] G) (s.indicator (Function.const Ω c) ω) : E →L[ℝ] G) : (a : E) → G) (f ω) : G)
      (s.indicator (fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) c : E →L[ℝ] G) : (a : E) → G) (f ω)) ω : G)
⊢ Eq.{u_4 + 1} (α := G)
    ((((B : (a : F) → E →L[ℝ] G) (s.indicator (Function.const Ω c) ω) : E →L[ℝ] G) : (a : E) → G) (f ω) : G)
    (s.indicator (fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) c : E →L[ℝ] G) : (a : E) → G) (f ω)) ω : G)
have neg : ∀ (hω : ω ∉ s),
  Eq.{u_4 + 1} (α := G)
    ((((B : (a : F) → E →L[ℝ] G) (s.indicator (Function.const Ω c) ω) : E →L[ℝ] G) : (a : E) → G) (f ω) : G)
    (s.indicator (fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) c : E →L[ℝ] G) : (a : E) → G) (f ω)) ω : G)
Tactic: by_cases hω : ω ∈ s
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.PullOut (hypothesis)
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 μ
⊢ 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] ω)
have 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 ω))
Tactic: have : ∀ (s c) (f : Ω → E),
      (fun ω ↦ B (Set.indicator s (Function.const Ω c) ω) (f ω)) =
        s.indicator (fun ω ↦ B c (f ω)) := by
    intro s c f
    ext ω
    by_cases hω : ω ∈ s <;> simp [hω]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.PullOut (goal)
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 ω))
⊢ 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] ω)
have apply : ∀ (c : F) (s : Set Ω) (hs : MeasurableSet s),
  EventuallyEq.{u_1, u_4} (β := G) (ae μ)
    μ[fun (ω : Ω) ↦
      (((B : (a : F) → E →L[ℝ] G)
              ((SimpleFunc.piecewise s hs (SimpleFunc.const Ω c) (SimpleFunc.const Ω 0) : (a : Ω) → F) ω) :
            E →L[ℝ] G) :
          (a : E) → G)
        (g ω) |
      m]
    fun (ω : Ω) ↦
    (((B : (a : F) → E →L[ℝ] G)
            ((SimpleFunc.piecewise s hs (SimpleFunc.const Ω c) (SimpleFunc.const Ω 0) : (a : Ω) → F) ω) :
          E →L[ℝ] G) :
        (a : E) → G)
      (μ[g | m] ω)
Tactic: apply @SimpleFunc.induction _ _ m _ (fun f ↦ _)
    (fun c s hs ↦ ?_) (fun g₁ g₂ _ h_eq₁ h_eq₂ ↦ ?_) f
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.PullOut (goal)
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 ω))
apply :
  ∀ (c : F) (s : Set Ω) (hs : MeasurableSet s),
    EventuallyEq.{u_1, u_4} (β := G) (ae μ)
      μ[fun (ω : Ω) ↦
        (((B : (a : F) → E →L[ℝ] G)
                ((SimpleFunc.piecewise s hs (SimpleFunc.const Ω c) (SimpleFunc.const Ω 0) : (a : Ω) → F) ω) :
              E →L[ℝ] G) :
            (a : E) → G)
          (g ω) |
        m]
      fun (ω : Ω) ↦
      (((B : (a : F) → E →L[ℝ] G)
              ((SimpleFunc.piecewise s hs (SimpleFunc.const Ω c) (SimpleFunc.const Ω 0) : (a : Ω) → F) ω) :
            E →L[ℝ] G) :
          (a : E) → G)
        (μ[g | m] ω)
⊢ 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] ω)
have apply₁ : ∀ (g₁ g₂ : SimpleFunc Ω F),
  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₂),
      EventuallyEq.{u_1, u_4} (β := G) (ae μ)
        μ[fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) ((g₁ + g₂ : (a : Ω) → F) ω) : E →L[ℝ] G) : (a : E) → G) (g ω) | m]
        fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) ((g₁ + g₂ : (a : Ω) → F) ω) : E →L[ℝ] G) : (a : E) → G) (μ[g | m] ω)
Tactic: apply @SimpleFunc.induction _ _ m _ (fun f ↦ _)
    (fun c s hs ↦ ?_) (fun g₁ g₂ _ h_eq₁ h_eq₂ ↦ ?_) f
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.PullOut (goal)
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 ω))
c : F
s : Set Ω
hs : MeasurableSet s
⊢ EventuallyEq.{u_1, u_4} (β := G) (ae μ)
    μ[fun (ω : Ω) ↦
      (((B : (a : F) → E →L[ℝ] G)
              ((SimpleFunc.piecewise s hs (SimpleFunc.const Ω c) (SimpleFunc.const Ω 0) : (a : Ω) → F) ω) :
            E →L[ℝ] G) :
          (a : E) → G)
        (g ω) |
      m]
    fun (ω : Ω) ↦
    (((B : (a : F) → E →L[ℝ] G)
            ((SimpleFunc.piecewise s hs (SimpleFunc.const Ω c) (SimpleFunc.const Ω 0) : (a : Ω) → F) ω) :
          E →L[ℝ] G) :
        (a : E) → G)
      (μ[g | m] ω)
have simp : EventuallyEq.{u_1, u_4} (β := G) (ae μ)
  μ[fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) (s.indicator (Function.const Ω c) ω) : E →L[ℝ] G) : (a : E) → G) (g ω) |
    m]
  fun (ω : Ω) ↦
  (((B : (a : F) → E →L[ℝ] G) (s.indicator (Function.const Ω c) ω) : E →L[ℝ] G) : (a : E) → G) (μ[g | m] ω)
Tactic: simp only [SimpleFunc.const_zero, SimpleFunc.coe_piecewise, SimpleFunc.coe_const,
      SimpleFunc.coe_zero, Set.piecewise_eq_indicator]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.PullOut (goal)
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 ω))
c : F
s : Set Ω
hs : MeasurableSet s
⊢ EventuallyEq.{u_1, u_4} (β := G) (ae μ)
    μ[fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) (s.indicator (Function.const Ω c) ω) : E →L[ℝ] G) : (a : E) → G) (g ω) |
      m]
    fun (ω : Ω) ↦
    (((B : (a : F) → E →L[ℝ] G) (s.indicator (Function.const Ω c) ω) : E →L[ℝ] G) : (a : E) → G) (μ[g | m] ω)
have rw : EventuallyEq.{u_1, u_4} (β := G) (ae μ)
  μ[s.indicator fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) c : E →L[ℝ] G) : (a : E) → G) (g ω) | m]
  (s.indicator fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) c : E →L[ℝ] G) : (a : E) → G) (μ[g | m] ω))
Tactic: rw [this, this]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.PullOut (goal)
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 ω))
c : F
s : Set Ω
hs : MeasurableSet s
⊢ EventuallyEq.{u_1, u_4} (β := G) (ae μ)
    μ[s.indicator fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) c : E →L[ℝ] G) : (a : E) → G) (g ω) | m]
    (s.indicator fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) c : E →L[ℝ] G) : (a : E) → G) (μ[g | m] ω))
have refine : EventuallyEq.{u_1, u_4} (β := G) (ae μ)
  (s.indicator μ[fun (a : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) c : E →L[ℝ] G) : (a : E) → G) (g a) | m])
  (s.indicator fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) c : E →L[ℝ] G) : (a : E) → G) (μ[g | m] ω))
Tactic: refine (condExp_indicator ((B c).integrable_comp hg) hs).trans ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.PullOut (goal)
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 ω))
c : F
s : Set Ω
hs : MeasurableSet s
⊢ EventuallyEq.{u_1, u_4} (β := G) (ae μ)
    (s.indicator μ[fun (a : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) c : E →L[ℝ] G) : (a : E) → G) (g a) | m])
    (s.indicator fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) c : E →L[ℝ] G) : (a : E) → G) (μ[g | m] ω))
have h : ∀ (ω : Ω)
  (hω :
    Eq.{u_4 + 1} (α := G) (((⇑((B : (a : F) → E →L[ℝ] G) c : E →L[ℝ] G) : (a : E) → G) ∘ μ[g | m]) ω)
      (μ[(⇑((B : (a : F) → E →L[ℝ] G) c : E →L[ℝ] G) : (a : E) → G) ∘ g | m] ω)),
  Eq.{u_4 + 1} (α := G)
    (s.indicator μ[fun (a : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) c : E →L[ℝ] G) : (a : E) → G) (g a) | m] ω)
    (s.indicator (fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) c : E →L[ℝ] G) : (a : E) → G) (μ[g | m] ω)) ω)
Tactic: filter_upwards [(B c).comp_condExp_comm hg (m := m)] with ω hω
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.PullOut (hypothesis)
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₂
⊢ EventuallyEq.{u_1, u_4} (β := G) (ae μ)
    μ[fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) ((g₁ + g₂ : (a : Ω) → F) ω) : E →L[ℝ] G) : (a : E) → G) (g ω) | m]
    fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) ((g₁ + g₂ : (a : Ω) → F) ω) : E →L[ℝ] G) : (a : E) → G) (μ[g | m] ω)
have h_add : (⇑(g₁ + g₂) : (a : Ω) → F) = HAdd.hAdd (α := (a : Ω) → F) (⇑g₁ : (a : Ω) → F) (⇑g₂ : (a : Ω) → F)
Tactic: have h_add := @SimpleFunc.coe_add _ _ m _ g₁ g₂
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.PullOut (goal)
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)
⊢ μ[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]
have 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]
Tactic: simp_rw [B.map_add]