awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
f : Ω → F
g : Ω → E
hf : StronglyMeasurable f
hfg :
  Integrable.{u_4, u_1} (ε := G) (fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) (f ω) : E →L[ℝ] G) : (a : E) → G) (g ω)) μ
hg : Integrable g μ
hm : m ≤ mΩ
hμm : SigmaFinite (μ.trim hm)
sets : ℕ → Set Ω
h_univ : Eq.{u_1 + 1} (α := Set Ω) (⋃ (i : ℕ), sets i) Set.univ
h_meas : ∀ (x : ℕ), MeasurableSet (sets x)
h_finite : ∀ (x : ℕ), LT.lt (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (sets x) : ℝ≥0∞) (∞ : ℝ≥0∞)
h_norm : ∀ (x : ℕ), ∀ x_1 ∈ sets x, ‖f x_1‖ ≤ (↑x : ℝ)
n : ℕ
this :
  EventuallyEq.{u_1, u_4} (β := G) (ae (μ.restrict (sets n)))
    (μ.restrict (sets n))[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) ((μ.restrict (sets n))[g | m] ω)
ω : Ω
hω1 :
  Eq.{u_4 + 1} (α := G)
    ((μ.restrict (sets n))[fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) (f ω) : E →L[ℝ] G) : (a : E) → G) (g ω) | m] ω : G)
    ((((B : (a : F) → E →L[ℝ] G) (f ω) : E →L[ℝ] G) : (a : E) → G) ((μ.restrict (sets n))[g | m] ω) : G)
hω2 : (μ.restrict (sets n))[g | m] ω = μ[g | m] ω
⊢ Eq.{u_4 + 1} (α := G)
    ((μ.restrict (sets n))[fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) (f ω) : E →L[ℝ] G) : (a : E) → G) (g ω) | m] ω : G)
    ((((B : (a : F) → E →L[ℝ] G) (f ω) : E →L[ℝ] G) : (a : E) → G) (μ[g | m] ω) : G)
have h : Eq.{u_4 + 1} (α := G)
  ((((B : (a : F) → E →L[ℝ] G) (f ω) : E →L[ℝ] G) : (a : E) → G) ((μ.restrict (sets n))[g | m] ω) : G)
  ((((B : (a : F) → E →L[ℝ] G) (f ω) : E →L[ℝ] G) : (a : E) → G) (μ[g | m] ω) : G)
Tactic: rw [hω1, hω2]
-- 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
f : Ω → F
g : Ω → E
hf : StronglyMeasurable f
hfg :
  Integrable.{u_4, u_1} (ε := G) (fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) (f ω) : E →L[ℝ] G) : (a : E) → G) (g ω)) μ
hg : Integrable g μ
hm : m ≤ mΩ
hμm : SigmaFinite (μ.trim hm)
sets : ℕ → Set Ω
h_univ : Eq.{u_1 + 1} (α := Set Ω) (⋃ (i : ℕ), sets i) Set.univ
h_meas : ∀ (x : ℕ), MeasurableSet (sets x)
h_finite : ∀ (x : ℕ), LT.lt (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (sets x) : ℝ≥0∞) (∞ : ℝ≥0∞)
h_norm : ∀ (x : ℕ), ∀ x_1 ∈ sets x, ‖f x_1‖ ≤ (↑x : ℝ)
n : ℕ
this :
  EventuallyEq.{u_1, u_4} (β := G) (ae (μ.restrict (sets n)))
    (μ.restrict (sets n))[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) ((μ.restrict (sets n))[g | m] ω)
ω : Ω
hω1 :
  Eq.{u_4 + 1} (α := G)
    ((μ.restrict (sets n))[fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) (f ω) : E →L[ℝ] G) : (a : E) → G) (g ω) | m] ω : G)
    ((((B : (a : F) → E →L[ℝ] G) (f ω) : E →L[ℝ] G) : (a : E) → G) ((μ.restrict (sets n))[g | m] ω) : G)
hω2 : (μ.restrict (sets n))[g | m] ω = μ[g | m] ω
h :
  Eq.{u_4 + 1} (α := G)
    ((((B : (a : F) → E →L[ℝ] G) (f ω) : E →L[ℝ] G) : (a : E) → G) ((μ.restrict (sets n))[g | m] ω) : G)
    ((((B : (a : F) → E →L[ℝ] G) (f ω) : E →L[ℝ] G) : (a : E) → G) (μ[g | m] ω) : G)
⊢ Eq.{u_4 + 1} (α := G)
    ((μ.restrict (sets n))[fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) (f ω) : E →L[ℝ] G) : (a : E) → G) (g ω) | m] ω : G)
    ((((B : (a : F) → E →L[ℝ] G) (f ω) : E →L[ℝ] G) : (a : E) → G) (μ[g | m] ω) : G)
have h₁ : Eq.{u_4 + 1} (α := G) ((((B : (a : F) → E →L[ℝ] G) (f ω) : E →L[ℝ] G) : (a : E) → G) (μ[g | m] ω) : G)
  ((((B : (a : F) → E →L[ℝ] G) (f ω) : E →L[ℝ] G) : (a : E) → G) (μ[g | m] ω) : G)
Tactic: rw [hω1, hω2]
-- 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
f : Ω → F
g : Ω → E
hf : StronglyMeasurable f
hfg :
  Integrable.{u_4, u_1} (ε := G) (fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) (f ω) : E →L[ℝ] G) : (a : E) → G) (g ω)) μ
hg : Integrable g μ
hm : m ≤ mΩ
hμm : SigmaFinite (μ.trim hm)
sets : ℕ → Set Ω
h_univ : Eq.{u_1 + 1} (α := Set Ω) (⋃ (i : ℕ), sets i) Set.univ
h_meas : ∀ (x : ℕ), MeasurableSet (sets x)
h_finite : ∀ (x : ℕ), LT.lt (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (sets x) : ℝ≥0∞) (∞ : ℝ≥0∞)
h_norm : ∀ (x : ℕ), ∀ x_1 ∈ sets x, ‖f x_1‖ ≤ (↑x : ℝ)
n : ℕ
⊢ ∀ᵐ (x : Ω) ∂μ.restrict (sets n),
    Eq.{u_4 + 1} (α := G)
      (μ[fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) (f ω) : E →L[ℝ] G) : (a : E) → G) (g ω) | m] x : G)
      ((((B : (a : F) → E →L[ℝ] G) (f x) : E →L[ℝ] G) : (a : E) → G) (μ[g | m] x) : G)
have pos : EventuallyEq.{u_1, u_4} (β := G) (ae (μ.restrict (sets n)))
  (μ.restrict (sets n))[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) ((μ.restrict (sets n))[g | m] ω)
Tactic: suffices (μ.restrict (sets n))[fun ω ↦ B (f ω) (g ω) | m] =ᵐ[μ.restrict (sets n)]
      fun ω ↦ B (f ω) ((μ.restrict (sets n))[g | m] ω) by
    refine (condExp_restrict_ae_eq_restrict hm (h_meas n) hfg).symm.trans ?_
    filter_upwards [this, (condExp_restrict_ae_eq_restrict hm (h_meas n) hg)] with ω hω1 hω2
    rw [hω1, hω2]
-- 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
f : Ω → F
g : Ω → E
hf : StronglyMeasurable f
hfg :
  Integrable.{u_4, u_1} (ε := G) (fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) (f ω) : E →L[ℝ] G) : (a : E) → G) (g ω)) μ
hg : Integrable g μ
hm : m ≤ mΩ
hμm : SigmaFinite (μ.trim hm)
sets : ℕ → Set Ω
h_univ : Eq.{u_1 + 1} (α := Set Ω) (⋃ (i : ℕ), sets i) Set.univ
h_meas : ∀ (x : ℕ), MeasurableSet (sets x)
h_finite : ∀ (x : ℕ), LT.lt (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (sets x) : ℝ≥0∞) (∞ : ℝ≥0∞)
h_norm : ∀ (x : ℕ), ∀ x_1 ∈ sets x, ‖f x_1‖ ≤ (↑x : ℝ)
n : ℕ
this :
  EventuallyEq.{u_1, u_4} (β := G) (ae (μ.restrict (sets n)))
    (μ.restrict (sets n))[fun (ω : Ω) ↦
      (((B : (a : F) → E →L[ℝ] G) ((sets n).indicator f ω) : E →L[ℝ] G) : (a : E) → G) (g ω) | m]
    fun (ω : Ω) ↦
    (((B : (a : F) → E →L[ℝ] G) ((sets n).indicator f ω) : E →L[ℝ] G) : (a : E) → G) ((μ.restrict (sets n))[g | m] ω)
⊢ EventuallyEq.{u_1, u_4} (β := G) (ae (μ.restrict (sets n)))
    (μ.restrict (sets n))[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) ((μ.restrict (sets n))[g | m] ω)
have refine_1 : EventuallyEq.{u_1, u_4} (β := G) (ae (μ.restrict (sets n)))
  (fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) (f ω) : E →L[ℝ] G) : (a : E) → G) (g ω)) fun (ω : Ω) ↦
  (((B : (a : F) → E →L[ℝ] G) ((sets n).indicator f ω) : E →L[ℝ] G) : (a : E) → G) (g ω)
Tactic: refine EventuallyEq.trans (condExp_congr_ae ?_) (this.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
f : Ω → F
g : Ω → E
hf : StronglyMeasurable f
hfg :
  Integrable.{u_4, u_1} (ε := G) (fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) (f ω) : E →L[ℝ] G) : (a : E) → G) (g ω)) μ
hg : Integrable g μ
hm : m ≤ mΩ
hμm : SigmaFinite (μ.trim hm)
sets : ℕ → Set Ω
h_univ : Eq.{u_1 + 1} (α := Set Ω) (⋃ (i : ℕ), sets i) Set.univ
h_meas : ∀ (x : ℕ), MeasurableSet (sets x)
h_finite : ∀ (x : ℕ), LT.lt (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (sets x) : ℝ≥0∞) (∞ : ℝ≥0∞)
h_norm : ∀ (x : ℕ), ∀ x_1 ∈ sets x, ‖f x_1‖ ≤ (↑x : ℝ)
n : ℕ
this :
  EventuallyEq.{u_1, u_4} (β := G) (ae (μ.restrict (sets n)))
    (μ.restrict (sets n))[fun (ω : Ω) ↦
      (((B : (a : F) → E →L[ℝ] G) ((sets n).indicator f ω) : E →L[ℝ] G) : (a : E) → G) (g ω) | m]
    fun (ω : Ω) ↦
    (((B : (a : F) → E →L[ℝ] G) ((sets n).indicator f ω) : E →L[ℝ] G) : (a : E) → G) ((μ.restrict (sets n))[g | m] ω)
refine_1 :
  EventuallyEq.{u_1, u_4} (β := G) (ae (μ.restrict (sets n)))
    (fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) (f ω) : E →L[ℝ] G) : (a : E) → G) (g ω)) fun (ω : Ω) ↦
    (((B : (a : F) → E →L[ℝ] G) ((sets n).indicator f ω) : E →L[ℝ] G) : (a : E) → G) (g ω)
⊢ EventuallyEq.{u_1, u_4} (β := G) (ae (μ.restrict (sets n)))
    (μ.restrict (sets n))[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) ((μ.restrict (sets n))[g | m] ω)
have refine_2 : EventuallyEq.{u_1, u_4} (β := G) (ae (μ.restrict (sets n)))
  (fun (ω : Ω) ↦
    (((B : (a : F) → E →L[ℝ] G) ((sets n).indicator f ω) : E →L[ℝ] G) : (a : E) → G) ((μ.restrict (sets n))[g | m] ω))
  fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) (f ω) : E →L[ℝ] G) : (a : E) → G) ((μ.restrict (sets n))[g | m] ω)
Tactic: refine EventuallyEq.trans (condExp_congr_ae ?_) (this.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
f : Ω → F
g : Ω → E
hf : StronglyMeasurable f
hfg :
  Integrable.{u_4, u_1} (ε := G) (fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) (f ω) : E →L[ℝ] G) : (a : E) → G) (g ω)) μ
hg : Integrable g μ
hm : m ≤ mΩ
hμm : SigmaFinite (μ.trim hm)
sets : ℕ → Set Ω
h_univ : Eq.{u_1 + 1} (α := Set Ω) (⋃ (i : ℕ), sets i) Set.univ
h_meas : ∀ (x : ℕ), MeasurableSet (sets x)
h_finite : ∀ (x : ℕ), LT.lt (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (sets x) : ℝ≥0∞) (∞ : ℝ≥0∞)
h_norm : ∀ (x : ℕ), ∀ x_1 ∈ sets x, ‖f x_1‖ ≤ (↑x : ℝ)
n : ℕ
this :
  EventuallyEq.{u_1, u_4} (β := G) (ae (μ.restrict (sets n)))
    (μ.restrict (sets n))[fun (ω : Ω) ↦
      (((B : (a : F) → E →L[ℝ] G) ((sets n).indicator f ω) : E →L[ℝ] G) : (a : E) → G) (g ω) | m]
    fun (ω : Ω) ↦
    (((B : (a : F) → E →L[ℝ] G) ((sets n).indicator f ω) : E →L[ℝ] G) : (a : E) → G) ((μ.restrict (sets n))[g | m] ω)
⊢ EventuallyEq.{u_1, u_4} (β := G) (ae (μ.restrict (sets n)))
    (fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) (f ω) : E →L[ℝ] G) : (a : E) → G) (g ω)) fun (ω : Ω) ↦
    (((B : (a : F) → E →L[ℝ] G) ((sets n).indicator f ω) : E →L[ℝ] G) : (a : E) → G) (g ω)
have h : ∀ (ω : Ω) (hω : (sets n).indicator f ω = f ω),
  Eq.{u_4 + 1} (α := G) ((((B : (a : F) → E →L[ℝ] G) (f ω) : E →L[ℝ] G) : (a : E) → G) (g ω) : G)
    ((((B : (a : F) → E →L[ℝ] G) ((sets n).indicator f ω) : E →L[ℝ] G) : (a : E) → G) (g ω) : G)
Tactic: filter_upwards [indicator_ae_eq_restrict (f := f) <| hm _ <| h_meas n] with ω 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
f : Ω → F
g : Ω → E
hf : StronglyMeasurable f
hfg :
  Integrable.{u_4, u_1} (ε := G) (fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) (f ω) : E →L[ℝ] G) : (a : E) → G) (g ω)) μ
hg : Integrable g μ
hm : m ≤ mΩ
hμm : SigmaFinite (μ.trim hm)
sets : ℕ → Set Ω
h_univ : Eq.{u_1 + 1} (α := Set Ω) (⋃ (i : ℕ), sets i) Set.univ
h_meas : ∀ (x : ℕ), MeasurableSet (sets x)
h_finite : ∀ (x : ℕ), LT.lt (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (sets x) : ℝ≥0∞) (∞ : ℝ≥0∞)
h_norm : ∀ (x : ℕ), ∀ x_1 ∈ sets x, ‖f x_1‖ ≤ (↑x : ℝ)
n : ℕ
this :
  EventuallyEq.{u_1, u_4} (β := G) (ae (μ.restrict (sets n)))
    (μ.restrict (sets n))[fun (ω : Ω) ↦
      (((B : (a : F) → E →L[ℝ] G) ((sets n).indicator f ω) : E →L[ℝ] G) : (a : E) → G) (g ω) | m]
    fun (ω : Ω) ↦
    (((B : (a : F) → E →L[ℝ] G) ((sets n).indicator f ω) : E →L[ℝ] G) : (a : E) → G) ((μ.restrict (sets n))[g | m] ω)
ω : Ω
hω : (sets n).indicator f ω = f ω
⊢ Eq.{u_4 + 1} (α := G) ((((B : (a : F) → E →L[ℝ] G) (f ω) : E →L[ℝ] G) : (a : E) → G) (g ω) : G)
    ((((B : (a : F) → E →L[ℝ] G) ((sets n).indicator f ω) : E →L[ℝ] G) : (a : E) → G) (g ω) : G)
have h : Eq.{u_4 + 1} (α := G) ((((B : (a : F) → E →L[ℝ] G) (f ω) : E →L[ℝ] G) : (a : E) → G) (g ω) : G)
  ((((B : (a : F) → E →L[ℝ] G) (f ω) : E →L[ℝ] G) : (a : E) → G) (g ω) : G)
Tactic: rw [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
f : Ω → F
g : Ω → E
hf : StronglyMeasurable f
hfg :
  Integrable.{u_4, u_1} (ε := G) (fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) (f ω) : E →L[ℝ] G) : (a : E) → G) (g ω)) μ
hg : Integrable g μ
hm : m ≤ mΩ
hμm : SigmaFinite (μ.trim hm)
sets : ℕ → Set Ω
h_univ : Eq.{u_1 + 1} (α := Set Ω) (⋃ (i : ℕ), sets i) Set.univ
h_meas : ∀ (x : ℕ), MeasurableSet (sets x)
h_finite : ∀ (x : ℕ), LT.lt (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (sets x) : ℝ≥0∞) (∞ : ℝ≥0∞)
h_norm : ∀ (x : ℕ), ∀ x_1 ∈ sets x, ‖f x_1‖ ≤ (↑x : ℝ)
n : ℕ
this :
  EventuallyEq.{u_1, u_4} (β := G) (ae (μ.restrict (sets n)))
    (μ.restrict (sets n))[fun (ω : Ω) ↦
      (((B : (a : F) → E →L[ℝ] G) ((sets n).indicator f ω) : E →L[ℝ] G) : (a : E) → G) (g ω) | m]
    fun (ω : Ω) ↦
    (((B : (a : F) → E →L[ℝ] G) ((sets n).indicator f ω) : E →L[ℝ] G) : (a : E) → G) ((μ.restrict (sets n))[g | m] ω)
⊢ EventuallyEq.{u_1, u_4} (β := G) (ae (μ.restrict (sets n)))
    (fun (ω : Ω) ↦
      (((B : (a : F) → E →L[ℝ] G) ((sets n).indicator f ω) : E →L[ℝ] G) : (a : E) → G) ((μ.restrict (sets n))[g | m] ω))
    fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) (f ω) : E →L[ℝ] G) : (a : E) → G) ((μ.restrict (sets n))[g | m] ω)
have h : ∀ (ω : Ω) (hω : (sets n).indicator f ω = f ω),
  Eq.{u_4 + 1} (α := G)
    ((((B : (a : F) → E →L[ℝ] G) ((sets n).indicator f ω) : E →L[ℝ] G) : (a : E) → G) ((μ.restrict (sets n))[g | m] ω) :
      G)
    ((((B : (a : F) → E →L[ℝ] G) (f ω) : E →L[ℝ] G) : (a : E) → G) ((μ.restrict (sets n))[g | m] ω) : G)
Tactic: filter_upwards [indicator_ae_eq_restrict (f := f) <| hm _ <| h_meas n] with ω 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
f : Ω → F
g : Ω → E
hf : StronglyMeasurable f
hfg :
  Integrable.{u_4, u_1} (ε := G) (fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) (f ω) : E →L[ℝ] G) : (a : E) → G) (g ω)) μ
hg : Integrable g μ
hm : m ≤ mΩ
hμm : SigmaFinite (μ.trim hm)
sets : ℕ → Set Ω
h_univ : Eq.{u_1 + 1} (α := Set Ω) (⋃ (i : ℕ), sets i) Set.univ
h_meas : ∀ (x : ℕ), MeasurableSet (sets x)
h_finite : ∀ (x : ℕ), LT.lt (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (sets x) : ℝ≥0∞) (∞ : ℝ≥0∞)
h_norm : ∀ (x : ℕ), ∀ x_1 ∈ sets x, ‖f x_1‖ ≤ (↑x : ℝ)
n : ℕ
this :
  EventuallyEq.{u_1, u_4} (β := G) (ae (μ.restrict (sets n)))
    (μ.restrict (sets n))[fun (ω : Ω) ↦
      (((B : (a : F) → E →L[ℝ] G) ((sets n).indicator f ω) : E →L[ℝ] G) : (a : E) → G) (g ω) | m]
    fun (ω : Ω) ↦
    (((B : (a : F) → E →L[ℝ] G) ((sets n).indicator f ω) : E →L[ℝ] G) : (a : E) → G) ((μ.restrict (sets n))[g | m] ω)
ω : Ω
hω : (sets n).indicator f ω = f ω
⊢ Eq.{u_4 + 1} (α := G)
    ((((B : (a : F) → E →L[ℝ] G) ((sets n).indicator f ω) : E →L[ℝ] G) : (a : E) → G) ((μ.restrict (sets n))[g | m] ω) :
      G)
    ((((B : (a : F) → E →L[ℝ] G) (f ω) : E →L[ℝ] G) : (a : E) → G) ((μ.restrict (sets n))[g | m] ω) : G)
have h : Eq.{u_4 + 1} (α := G)
  ((((B : (a : F) → E →L[ℝ] G) (f ω) : E →L[ℝ] G) : (a : E) → G) ((μ.restrict (sets n))[g | m] ω) : G)
  ((((B : (a : F) → E →L[ℝ] G) (f ω) : E →L[ℝ] G) : (a : E) → G) ((μ.restrict (sets n))[g | m] ω) : G)
Tactic: rw [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
f : Ω → F
g : Ω → E
hf : StronglyMeasurable f
hfg :
  Integrable.{u_4, u_1} (ε := G) (fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) (f ω) : E →L[ℝ] G) : (a : E) → G) (g ω)) μ
hg : Integrable g μ
hm : m ≤ mΩ
hμm : SigmaFinite (μ.trim hm)
sets : ℕ → Set Ω
h_univ : Eq.{u_1 + 1} (α := Set Ω) (⋃ (i : ℕ), sets i) Set.univ
h_meas : ∀ (x : ℕ), MeasurableSet (sets x)
h_finite : ∀ (x : ℕ), LT.lt (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (sets x) : ℝ≥0∞) (∞ : ℝ≥0∞)
h_norm : ∀ (x : ℕ), ∀ x_1 ∈ sets x, ‖f x_1‖ ≤ (↑x : ℝ)
n : ℕ
⊢ EventuallyEq.{u_1, u_4} (β := G) (ae (μ.restrict (sets n)))
    (μ.restrict (sets n))[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) ((μ.restrict (sets n))[g | m] ω)
have pos : EventuallyEq.{u_1, u_4} (β := G) (ae (μ.restrict (sets n)))
  (μ.restrict (sets n))[fun (ω : Ω) ↦
    (((B : (a : F) → E →L[ℝ] G) ((sets n).indicator f ω) : E →L[ℝ] G) : (a : E) → G) (g ω) | m]
  fun (ω : Ω) ↦
  (((B : (a : F) → E →L[ℝ] G) ((sets n).indicator f ω) : E →L[ℝ] G) : (a : E) → G) ((μ.restrict (sets n))[g | m] ω)
Tactic: suffices (μ.restrict (sets n))[fun ω ↦ B ((sets n).indicator f ω) (g ω) | m]
      =ᵐ[μ.restrict (sets n)] fun ω ↦ B ((sets n).indicator f ω) ((μ.restrict (sets n))[g | m] ω) by
    refine EventuallyEq.trans (condExp_congr_ae ?_) (this.trans ?_)
    · filter_upwards [indicator_ae_eq_restrict (f := f) <| hm _ <| h_meas n] with ω hω
      rw [hω]
    · filter_upwards [indicator_ae_eq_restrict (f := f) <| hm _ <| h_meas n] with ω hω
      rw [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
f : Ω → F
g : Ω → E
hf : StronglyMeasurable f
hfg :
  Integrable.{u_4, u_1} (ε := G) (fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) (f ω) : E →L[ℝ] G) : (a : E) → G) (g ω)) μ
hg : Integrable g μ
hm : m ≤ mΩ
hμm : SigmaFinite (μ.trim hm)
sets : ℕ → Set Ω
h_univ : Eq.{u_1 + 1} (α := Set Ω) (⋃ (i : ℕ), sets i) Set.univ
h_meas : ∀ (x : ℕ), MeasurableSet (sets x)
h_finite : ∀ (x : ℕ), LT.lt (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (sets x) : ℝ≥0∞) (∞ : ℝ≥0∞)
h_norm : ∀ (x : ℕ), ∀ x_1 ∈ sets x, ‖f x_1‖ ≤ (↑x : ℝ)
n : ℕ
⊢ IsFiniteMeasure (μ.restrict (sets n))
have measure_univ_lt_top : LT.lt (α := ℝ≥0∞) ((μ.restrict (sets n) : (a : Set Ω) → ℝ≥0∞) Set.univ : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: constructor
-- 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
f : Ω → F
g : Ω → E
hf : StronglyMeasurable f
hfg :
  Integrable.{u_4, u_1} (ε := G) (fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) (f ω) : E →L[ℝ] G) : (a : E) → G) (g ω)) μ
hg : Integrable g μ
hm : m ≤ mΩ
hμm : SigmaFinite (μ.trim hm)
sets : ℕ → Set Ω
h_univ : Eq.{u_1 + 1} (α := Set Ω) (⋃ (i : ℕ), sets i) Set.univ
h_meas : ∀ (x : ℕ), MeasurableSet (sets x)
h_finite : ∀ (x : ℕ), LT.lt (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (sets x) : ℝ≥0∞) (∞ : ℝ≥0∞)
h_norm : ∀ (x : ℕ), ∀ x_1 ∈ sets x, ‖f x_1‖ ≤ (↑x : ℝ)
n : ℕ
⊢ LT.lt (α := ℝ≥0∞) ((μ.restrict (sets n) : (a : Set Ω) → ℝ≥0∞) Set.univ : ℝ≥0∞) (∞ : ℝ≥0∞)
have measure_univ_lt_top : LT.lt (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (sets n) : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: rw [Measure.restrict_apply_univ]
-- 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
f : Ω → F
g : Ω → E
hf : StronglyMeasurable f
hfg :
  Integrable.{u_4, u_1} (ε := G) (fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) (f ω) : E →L[ℝ] G) : (a : E) → G) (g ω)) μ
hg : Integrable g μ
hm : m ≤ mΩ
hμm : SigmaFinite (μ.trim hm)
sets : ℕ → Set Ω
h_univ : Eq.{u_1 + 1} (α := Set Ω) (⋃ (i : ℕ), sets i) Set.univ
h_meas : ∀ (x : ℕ), MeasurableSet (sets x)
h_finite : ∀ (x : ℕ), LT.lt (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (sets x) : ℝ≥0∞) (∞ : ℝ≥0∞)
h_norm : ∀ (x : ℕ), ∀ x_1 ∈ sets x, ‖f x_1‖ ≤ (↑x : ℝ)
n : ℕ
⊢ EventuallyEq.{u_1, u_4} (β := G) (ae (μ.restrict (sets n)))
    (μ.restrict (sets n))[fun (ω : Ω) ↦
      (((B : (a : F) → E →L[ℝ] G) ((sets n).indicator f ω) : E →L[ℝ] G) : (a : E) → G) (g ω) | m]
    fun (ω : Ω) ↦
    (((B : (a : F) → E →L[ℝ] G) ((sets n).indicator f ω) : E →L[ℝ] G) : (a : E) → G) ((μ.restrict (sets n))[g | m] ω)
have this : IsFiniteMeasure (μ.restrict (sets n))
Tactic: have : IsFiniteMeasure (μ.restrict (sets n)) := by
    constructor
    rw [Measure.restrict_apply_univ]
    exact h_finite n