awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic (goal)
Goal:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : CompleteSpace E
hm : m ≤ m₀
hfμ : SigmaFinite (μ.trim hm)
pos : ∀ (hfi : Integrable f μ), eLpNorm μ[f | m] 2 μ ≤ eLpNorm f 2 μ
⊢ eLpNorm μ[f | m] 2 μ ≤ eLpNorm f 2 μ
have neg : ∀ (hfi : ¬Integrable f μ), eLpNorm μ[f | m] 2 μ ≤ eLpNorm f 2 μ
Tactic: by_cases hfi : Integrable f μ
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic (goal)
Goal:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : CompleteSpace E
hm : m ≤ m₀
hfμ : SigmaFinite (μ.trim hm)
hfi : ¬Integrable f μ
⊢ eLpNorm μ[f | m] 2 μ ≤ eLpNorm f 2 μ
have neg : eLpNorm.{u_1, u_3} (ε := E) 0 2 μ ≤ eLpNorm f 2 μ
Tactic: rw [condExp_of_not_integrable hfi]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic (goal)
Goal:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : CompleteSpace E
hm : m ≤ m₀
hfμ : SigmaFinite (μ.trim hm)
hfi : Integrable f μ
⊢ eLpNorm μ[f | m] 2 μ ≤ eLpNorm f 2 μ
have pos : ∀ (hf : eLpNorm f 2 μ = ∞), eLpNorm μ[f | m] 2 μ ≤ eLpNorm f 2 μ
Tactic: obtain hf | hf := eq_or_ne (eLpNorm f 2 μ) ∞
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic (goal)
Goal:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : CompleteSpace E
hm : m ≤ m₀
hfμ : SigmaFinite (μ.trim hm)
hfi : Integrable f μ
pos : ∀ (hf : eLpNorm f 2 μ = ∞), eLpNorm μ[f | m] 2 μ ≤ eLpNorm f 2 μ
⊢ eLpNorm μ[f | m] 2 μ ≤ eLpNorm f 2 μ
have pos₁ : ∀ (hf : eLpNorm f 2 μ ≠ ∞), eLpNorm μ[f | m] 2 μ ≤ eLpNorm f 2 μ
Tactic: obtain hf | hf := eq_or_ne (eLpNorm f 2 μ) ∞
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic (hypothesis)
Goal:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : CompleteSpace E
hm : m ≤ m₀
hfμ : SigmaFinite (μ.trim hm)
hfi : Integrable f μ
hf : eLpNorm f 2 μ ≠ ∞
⊢ eLpNorm μ[f | m] 2 μ ≤ eLpNorm f 2 μ
have hf₁ : MemLp f 2 μ
Tactic: replace hf : MemLp f 2 μ := ⟨hfi.1, Ne.lt_top' fun a ↦ hf a.symm⟩
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic (goal)
Goal:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : CompleteSpace E
hm : m ≤ m₀
hfμ : SigmaFinite (μ.trim hm)
hfi : Integrable f μ
hf : MemLp f 2 μ
⊢ eLpNorm μ[f | m] 2 μ ≤ eLpNorm f 2 μ
have pos : eLpNorm.{u_1, u_3} (ε := E)
    (↑(↑(↑((condExpL2 E ℝ hm : (a : ↥(Lp E 2 μ)) → ↥(lpMeas E ℝ m 2 μ)) (MemLp.toLp f hf)) : ↥(Lp E 2 μ)) : α →ₘ[μ] E) :
      α → E)
    2 μ ≤
  eLpNorm f 2 μ
Tactic: rw [← eLpNorm_congr_ae (hf.condExpL2_ae_eq_condExp' (𝕜 := ℝ) hm hfi)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic (goal)
Goal:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : CompleteSpace E
hm : m ≤ m₀
hfμ : SigmaFinite (μ.trim hm)
hfi : Integrable f μ
hf : MemLp f 2 μ
⊢ eLpNorm.{u_1, u_3} (ε := E)
      (↑(↑(↑((condExpL2 E ℝ hm : (a : ↥(Lp E 2 μ)) → ↥(lpMeas E ℝ m 2 μ)) (MemLp.toLp f hf)) : ↥(Lp E 2 μ)) :
            α →ₘ[μ] E) :
        α → E)
      2 μ ≤
    eLpNorm f 2 μ
have pos : eLpNorm (↑(↑(MemLp.toLp f hf) : α →ₘ[μ] E) : α → E) 2 μ ≤ eLpNorm f 2 μ
Tactic: refine le_trans (eLpNorm_condExpL2_le hm _) ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic (goal)
Goal:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : CompleteSpace E
hm : m ≤ m₀
hfμ : SigmaFinite (μ.trim hm)
hfi : Integrable f μ
hf : MemLp f 2 μ
⊢ eLpNorm (↑(↑(MemLp.toLp f hf) : α →ₘ[μ] E) : α → E) 2 μ ≤ eLpNorm f 2 μ
have pos : eLpNorm f 2 μ ≤ eLpNorm f 2 μ
Tactic: rw [eLpNorm_congr_ae hf.coeFn_toLp]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic (goal)
Goal:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : CompleteSpace E
hf : MemLp f 2 μ
⊢ MemLp μ[f | m] 2 μ
have pos : ∀ (hm : m ≤ m₀), MemLp μ[f | m] 2 μ
Tactic: by_cases hm : m ≤ m₀
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic (goal)
Goal:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : CompleteSpace E
hf : MemLp f 2 μ
pos : ∀ (hm : m ≤ m₀), MemLp μ[f | m] 2 μ
⊢ MemLp μ[f | m] 2 μ
have neg : ∀ (hm : ¬m ≤ m₀), MemLp μ[f | m] 2 μ
Tactic: by_cases hm : m ≤ m₀
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic (goal)
Goal:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
fs gs : ℕ → α → E
f g : α → E
hfs_int : ∀ (n : ℕ), Integrable (fs n) μ
hgs_int : ∀ (n : ℕ), Integrable (gs n) μ
hfs : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ fs n x) atTop (𝓝 (f x))
hgs : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ gs n x) atTop (𝓝 (g x))
bound_fs : α → ℝ
h_int_bound_fs : Integrable bound_fs μ
bound_gs : α → ℝ
h_int_bound_gs : Integrable bound_gs μ
hfs_bound : ∀ (n : ℕ), ∀ᵐ (x : α) ∂μ, ‖fs n x‖ ≤ bound_fs x
hgs_bound : ∀ (n : ℕ), ∀ᵐ (x : α) ∂μ, ‖gs n x‖ ≤ bound_gs x
hfg : ∀ (n : ℕ), μ[fs n | m] =ᶠ[ae μ] μ[gs n | m]
⊢ μ[f | m] =ᶠ[ae μ] μ[g | m]
have pos : ∀ (hm : m ≤ m₀), μ[f | m] =ᶠ[ae μ] μ[g | m]
Tactic: by_cases hm : m ≤ m₀
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic (goal)
Goal:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
fs gs : ℕ → α → E
f g : α → E
hfs_int : ∀ (n : ℕ), Integrable (fs n) μ
hgs_int : ∀ (n : ℕ), Integrable (gs n) μ
hfs : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ fs n x) atTop (𝓝 (f x))
hgs : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ gs n x) atTop (𝓝 (g x))
bound_fs : α → ℝ
h_int_bound_fs : Integrable bound_fs μ
bound_gs : α → ℝ
h_int_bound_gs : Integrable bound_gs μ
hfs_bound : ∀ (n : ℕ), ∀ᵐ (x : α) ∂μ, ‖fs n x‖ ≤ bound_fs x
hgs_bound : ∀ (n : ℕ), ∀ᵐ (x : α) ∂μ, ‖gs n x‖ ≤ bound_gs x
hfg : ∀ (n : ℕ), μ[fs n | m] =ᶠ[ae μ] μ[gs n | m]
pos : ∀ (hm : m ≤ m₀), μ[f | m] =ᶠ[ae μ] μ[g | m]
⊢ μ[f | m] =ᶠ[ae μ] μ[g | m]
have neg : ∀ (hm : ¬m ≤ m₀), μ[f | m] =ᶠ[ae μ] μ[g | m]
Tactic: by_cases hm : m ≤ m₀
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic (goal)
Goal:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
fs gs : ℕ → α → E
f g : α → E
hfs_int : ∀ (n : ℕ), Integrable (fs n) μ
hgs_int : ∀ (n : ℕ), Integrable (gs n) μ
hfs : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ fs n x) atTop (𝓝 (f x))
hgs : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ gs n x) atTop (𝓝 (g x))
bound_fs : α → ℝ
h_int_bound_fs : Integrable bound_fs μ
bound_gs : α → ℝ
h_int_bound_gs : Integrable bound_gs μ
hfs_bound : ∀ (n : ℕ), ∀ᵐ (x : α) ∂μ, ‖fs n x‖ ≤ bound_fs x
hgs_bound : ∀ (n : ℕ), ∀ᵐ (x : α) ∂μ, ‖gs n x‖ ≤ bound_gs x
hfg : ∀ (n : ℕ), μ[fs n | m] =ᶠ[ae μ] μ[gs n | m]
hm : ¬m ≤ m₀
⊢ μ[f | m] =ᶠ[ae μ] μ[g | m]
have neg : EventuallyEq.{u_1, u_3} (β := E) (ae μ) 0 0
Tactic: simp_rw [condExp_of_not_le hm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic (goal)
Goal:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
fs gs : ℕ → α → E
f g : α → E
hfs_int : ∀ (n : ℕ), Integrable (fs n) μ
hgs_int : ∀ (n : ℕ), Integrable (gs n) μ
hfs : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ fs n x) atTop (𝓝 (f x))
hgs : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ gs n x) atTop (𝓝 (g x))
bound_fs : α → ℝ
h_int_bound_fs : Integrable bound_fs μ
bound_gs : α → ℝ
h_int_bound_gs : Integrable bound_gs μ
hfs_bound : ∀ (n : ℕ), ∀ᵐ (x : α) ∂μ, ‖fs n x‖ ≤ bound_fs x
hgs_bound : ∀ (n : ℕ), ∀ᵐ (x : α) ∂μ, ‖gs n x‖ ≤ bound_gs x
hfg : ∀ (n : ℕ), μ[fs n | m] =ᶠ[ae μ] μ[gs n | m]
hm : m ≤ m₀
⊢ μ[f | m] =ᶠ[ae μ] μ[g | m]
have pos : ∀ (hμm : SigmaFinite (μ.trim hm)), μ[f | m] =ᶠ[ae μ] μ[g | m]
Tactic: by_cases hμm : SigmaFinite (μ.trim hm)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic (goal)
Goal:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
fs gs : ℕ → α → E
f g : α → E
hfs_int : ∀ (n : ℕ), Integrable (fs n) μ
hgs_int : ∀ (n : ℕ), Integrable (gs n) μ
hfs : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ fs n x) atTop (𝓝 (f x))
hgs : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ gs n x) atTop (𝓝 (g x))
bound_fs : α → ℝ
h_int_bound_fs : Integrable bound_fs μ
bound_gs : α → ℝ
h_int_bound_gs : Integrable bound_gs μ
hfs_bound : ∀ (n : ℕ), ∀ᵐ (x : α) ∂μ, ‖fs n x‖ ≤ bound_fs x
hgs_bound : ∀ (n : ℕ), ∀ᵐ (x : α) ∂μ, ‖gs n x‖ ≤ bound_gs x
hfg : ∀ (n : ℕ), μ[fs n | m] =ᶠ[ae μ] μ[gs n | m]
hm : m ≤ m₀
pos : ∀ (hμm : SigmaFinite (μ.trim hm)), μ[f | m] =ᶠ[ae μ] μ[g | m]
⊢ μ[f | m] =ᶠ[ae μ] μ[g | m]
have neg : ∀ (hμm : ¬SigmaFinite (μ.trim hm)), μ[f | m] =ᶠ[ae μ] μ[g | m]
Tactic: by_cases hμm : SigmaFinite (μ.trim hm)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic (goal)
Goal:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
fs gs : ℕ → α → E
f g : α → E
hfs_int : ∀ (n : ℕ), Integrable (fs n) μ
hgs_int : ∀ (n : ℕ), Integrable (gs n) μ
hfs : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ fs n x) atTop (𝓝 (f x))
hgs : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ gs n x) atTop (𝓝 (g x))
bound_fs : α → ℝ
h_int_bound_fs : Integrable bound_fs μ
bound_gs : α → ℝ
h_int_bound_gs : Integrable bound_gs μ
hfs_bound : ∀ (n : ℕ), ∀ᵐ (x : α) ∂μ, ‖fs n x‖ ≤ bound_fs x
hgs_bound : ∀ (n : ℕ), ∀ᵐ (x : α) ∂μ, ‖gs n x‖ ≤ bound_gs x
hfg : ∀ (n : ℕ), μ[fs n | m] =ᶠ[ae μ] μ[gs n | m]
hm : m ≤ m₀
hμm : ¬SigmaFinite (μ.trim hm)
⊢ μ[f | m] =ᶠ[ae μ] μ[g | m]
have neg : EventuallyEq.{u_1, u_3} (β := E) (ae μ) 0 0
Tactic: simp_rw [condExp_of_not_sigmaFinite hm hμm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic (goal)
Goal:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
fs gs : ℕ → α → E
f g : α → E
hfs_int : ∀ (n : ℕ), Integrable (fs n) μ
hgs_int : ∀ (n : ℕ), Integrable (gs n) μ
hfs : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ fs n x) atTop (𝓝 (f x))
hgs : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ gs n x) atTop (𝓝 (g x))
bound_fs : α → ℝ
h_int_bound_fs : Integrable bound_fs μ
bound_gs : α → ℝ
h_int_bound_gs : Integrable bound_gs μ
hfs_bound : ∀ (n : ℕ), ∀ᵐ (x : α) ∂μ, ‖fs n x‖ ≤ bound_fs x
hgs_bound : ∀ (n : ℕ), ∀ᵐ (x : α) ∂μ, ‖gs n x‖ ≤ bound_gs x
hfg : ∀ (n : ℕ), μ[fs n | m] =ᶠ[ae μ] μ[gs n | m]
hm : m ≤ m₀
hμm : SigmaFinite (μ.trim hm)
⊢ μ[f | m] =ᶠ[ae μ] μ[g | m]
have pos : (↑(↑(condExpL1 hm μ g) : α →ₘ[μ] E) : α → E) =ᶠ[ae μ] (↑(↑(condExpL1 hm μ f) : α →ₘ[μ] E) : α → E)
Tactic: refine (condExp_ae_eq_condExpL1 hm f).trans ((condExp_ae_eq_condExpL1 hm g).trans ?_).symm
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic (goal)
Goal:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
fs gs : ℕ → α → E
f g : α → E
hfs_int : ∀ (n : ℕ), Integrable (fs n) μ
hgs_int : ∀ (n : ℕ), Integrable (gs n) μ
hfs : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ fs n x) atTop (𝓝 (f x))
hgs : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ gs n x) atTop (𝓝 (g x))
bound_fs : α → ℝ
h_int_bound_fs : Integrable bound_fs μ
bound_gs : α → ℝ
h_int_bound_gs : Integrable bound_gs μ
hfs_bound : ∀ (n : ℕ), ∀ᵐ (x : α) ∂μ, ‖fs n x‖ ≤ bound_fs x
hgs_bound : ∀ (n : ℕ), ∀ᵐ (x : α) ∂μ, ‖gs n x‖ ≤ bound_gs x
hfg : ∀ (n : ℕ), μ[fs n | m] =ᶠ[ae μ] μ[gs n | m]
hm : m ≤ m₀
hμm : SigmaFinite (μ.trim hm)
⊢ (↑(↑(condExpL1 hm μ g) : α →ₘ[μ] E) : α → E) =ᶠ[ae μ] (↑(↑(condExpL1 hm μ f) : α →ₘ[μ] E) : α → E)
have pos : Eq (α := ↥(Lp E 1 μ)) (condExpL1 hm μ g) (condExpL1 hm μ f)
Tactic: rw [← Lp.ext_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic (goal)
Goal:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
fs gs : ℕ → α → E
f g : α → E
hfs_int : ∀ (n : ℕ), Integrable (fs n) μ
hgs_int : ∀ (n : ℕ), Integrable (gs n) μ
hfs : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ fs n x) atTop (𝓝 (f x))
hgs : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ gs n x) atTop (𝓝 (g x))
bound_fs : α → ℝ
h_int_bound_fs : Integrable bound_fs μ
bound_gs : α → ℝ
h_int_bound_gs : Integrable bound_gs μ
hfs_bound : ∀ (n : ℕ), ∀ᵐ (x : α) ∂μ, ‖fs n x‖ ≤ bound_fs x
hgs_bound : ∀ (n : ℕ), ∀ᵐ (x : α) ∂μ, ‖gs n x‖ ≤ bound_gs x
hfg : ∀ (n : ℕ), μ[fs n | m] =ᶠ[ae μ] μ[gs n | m]
hm : m ≤ m₀
hμm : SigmaFinite (μ.trim hm)
n : ℕ
⊢ Eq (α := ↥(Lp E 1 μ)) (condExpL1 hm μ (gs n)) (condExpL1 hm μ (fs n))
have h : (↑(↑(condExpL1 hm μ (gs n)) : α →ₘ[μ] E) : α → E) =ᶠ[ae μ] (↑(↑(condExpL1 hm μ (fs n)) : α →ₘ[μ] E) : α → E)
Tactic: ext1
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic (goal)
Goal:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
fs gs : ℕ → α → E
f g : α → E
hfs_int : ∀ (n : ℕ), Integrable (fs n) μ
hgs_int : ∀ (n : ℕ), Integrable (gs n) μ
hfs : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ fs n x) atTop (𝓝 (f x))
hgs : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ gs n x) atTop (𝓝 (g x))
bound_fs : α → ℝ
h_int_bound_fs : Integrable bound_fs μ
bound_gs : α → ℝ
h_int_bound_gs : Integrable bound_gs μ
hfs_bound : ∀ (n : ℕ), ∀ᵐ (x : α) ∂μ, ‖fs n x‖ ≤ bound_fs x
hgs_bound : ∀ (n : ℕ), ∀ᵐ (x : α) ∂μ, ‖gs n x‖ ≤ bound_gs x
hfg : ∀ (n : ℕ), μ[fs n | m] =ᶠ[ae μ] μ[gs n | m]
hm : m ≤ m₀
hμm : SigmaFinite (μ.trim hm)
n : ℕ
⊢ (↑(↑(condExpL1 hm μ (gs n)) : α →ₘ[μ] E) : α → E) =ᶠ[ae μ] (↑(↑(condExpL1 hm μ (fs n)) : α →ₘ[μ] E) : α → E)
have h : μ[fs n | m] =ᶠ[ae μ] (↑(↑(condExpL1 hm μ (fs n)) : α →ₘ[μ] E) : α → E)
Tactic: refine (condExp_ae_eq_condExpL1 hm (gs n)).symm.trans ((hfg n).symm.trans ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic (hypothesis)
Goal:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
fs gs : ℕ → α → E
f g : α → E
hfs_int : ∀ (n : ℕ), Integrable (fs n) μ
hgs_int : ∀ (n : ℕ), Integrable (gs n) μ
hfs : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ fs n x) atTop (𝓝 (f x))
hgs : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ gs n x) atTop (𝓝 (g x))
bound_fs : α → ℝ
h_int_bound_fs : Integrable bound_fs μ
bound_gs : α → ℝ
h_int_bound_gs : Integrable bound_gs μ
hfs_bound : ∀ (n : ℕ), ∀ᵐ (x : α) ∂μ, ‖fs n x‖ ≤ bound_fs x
hgs_bound : ∀ (n : ℕ), ∀ᵐ (x : α) ∂μ, ‖gs n x‖ ≤ bound_gs x
hfg : ∀ (n : ℕ), μ[fs n | m] =ᶠ[ae μ] μ[gs n | m]
hm : m ≤ m₀
hμm : SigmaFinite (μ.trim hm)
⊢ Eq (α := ↥(Lp E 1 μ)) (condExpL1 hm μ g) (condExpL1 hm μ f)
have hn_eq : ∀ (n : ℕ), Eq (α := ↥(Lp E 1 μ)) (condExpL1 hm μ (gs n)) (condExpL1 hm μ (fs n))
Tactic: have hn_eq : ∀ n, condExpL1 hm μ (gs n) = condExpL1 hm μ (fs n) := by
    intro n
    ext1
    refine (condExp_ae_eq_condExpL1 hm (gs n)).symm.trans ((hfg n).symm.trans ?_)
    exact condExp_ae_eq_condExpL1 hm (fs n)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic (hypothesis)
Goal:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
fs gs : ℕ → α → E
f g : α → E
hfs_int : ∀ (n : ℕ), Integrable (fs n) μ
hgs_int : ∀ (n : ℕ), Integrable (gs n) μ
hfs : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ fs n x) atTop (𝓝 (f x))
hgs : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ gs n x) atTop (𝓝 (g x))
bound_fs : α → ℝ
h_int_bound_fs : Integrable bound_fs μ
bound_gs : α → ℝ
h_int_bound_gs : Integrable bound_gs μ
hfs_bound : ∀ (n : ℕ), ∀ᵐ (x : α) ∂μ, ‖fs n x‖ ≤ bound_fs x
hgs_bound : ∀ (n : ℕ), ∀ᵐ (x : α) ∂μ, ‖gs n x‖ ≤ bound_gs x
hfg : ∀ (n : ℕ), μ[fs n | m] =ᶠ[ae μ] μ[gs n | m]
hm : m ≤ m₀
hμm : SigmaFinite (μ.trim hm)
hn_eq : ∀ (n : ℕ), Eq (α := ↥(Lp E 1 μ)) (condExpL1 hm μ (gs n)) (condExpL1 hm μ (fs n))
⊢ Eq (α := ↥(Lp E 1 μ)) (condExpL1 hm μ g) (condExpL1 hm μ f)
have hcond_fs : Tendsto (β := ↥(Lp E 1 μ)) (fun (n : ℕ) ↦ condExpL1 hm μ (fs n)) atTop (𝓝 (condExpL1 hm μ f))
Tactic: have hcond_fs : Tendsto (fun n => condExpL1 hm μ (fs n)) atTop (𝓝 (condExpL1 hm μ f)) :=
    tendsto_condExpL1_of_dominated_convergence hm _ (fun n => (hfs_int n).1) h_int_bound_fs
      hfs_bound hfs
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic (hypothesis)
Goal:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
fs gs : ℕ → α → E
f g : α → E
hfs_int : ∀ (n : ℕ), Integrable (fs n) μ
hgs_int : ∀ (n : ℕ), Integrable (gs n) μ
hfs : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ fs n x) atTop (𝓝 (f x))
hgs : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ gs n x) atTop (𝓝 (g x))
bound_fs : α → ℝ
h_int_bound_fs : Integrable bound_fs μ
bound_gs : α → ℝ
h_int_bound_gs : Integrable bound_gs μ
hfs_bound : ∀ (n : ℕ), ∀ᵐ (x : α) ∂μ, ‖fs n x‖ ≤ bound_fs x
hgs_bound : ∀ (n : ℕ), ∀ᵐ (x : α) ∂μ, ‖gs n x‖ ≤ bound_gs x
hfg : ∀ (n : ℕ), μ[fs n | m] =ᶠ[ae μ] μ[gs n | m]
hm : m ≤ m₀
hμm : SigmaFinite (μ.trim hm)
hn_eq : ∀ (n : ℕ), Eq (α := ↥(Lp E 1 μ)) (condExpL1 hm μ (gs n)) (condExpL1 hm μ (fs n))
hcond_fs : Tendsto (β := ↥(Lp E 1 μ)) (fun (n : ℕ) ↦ condExpL1 hm μ (fs n)) atTop (𝓝 (condExpL1 hm μ f))
⊢ Eq (α := ↥(Lp E 1 μ)) (condExpL1 hm μ g) (condExpL1 hm μ f)
have hcond_gs : Tendsto (β := ↥(Lp E 1 μ)) (fun (n : ℕ) ↦ condExpL1 hm μ (gs n)) atTop (𝓝 (condExpL1 hm μ g))
Tactic: have hcond_gs : Tendsto (fun n => condExpL1 hm μ (gs n)) atTop (𝓝 (condExpL1 hm μ g)) :=
    tendsto_condExpL1_of_dominated_convergence hm _ (fun n => (hgs_int n).1) h_int_bound_gs
      hgs_bound hgs
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic (goal)
Goal:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f g : α → E
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
inst_3 : PartialOrder E
inst_4 : ClosedIciTopology E
inst_5 : IsOrderedAddMonoid E
inst_6 : IsOrderedModule ℝ E
hf : Integrable f μ
hg : Integrable g μ
hfg : f ≤ᶠ[ae μ] g
⊢ μ[f | m] ≤ᶠ[ae μ] μ[g | m]
have pos : ∀ (hm : m ≤ m₀), μ[f | m] ≤ᶠ[ae μ] μ[g | m]
Tactic: by_cases hm : m ≤ m₀
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic (goal)
Goal:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f g : α → E
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
inst_3 : PartialOrder E
inst_4 : ClosedIciTopology E
inst_5 : IsOrderedAddMonoid E
inst_6 : IsOrderedModule ℝ E
hf : Integrable f μ
hg : Integrable g μ
hfg : f ≤ᶠ[ae μ] g
pos : ∀ (hm : m ≤ m₀), μ[f | m] ≤ᶠ[ae μ] μ[g | m]
⊢ μ[f | m] ≤ᶠ[ae μ] μ[g | m]
have neg : ∀ (hm : ¬m ≤ m₀), μ[f | m] ≤ᶠ[ae μ] μ[g | m]
Tactic: by_cases hm : m ≤ m₀
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic (goal)
Goal:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f g : α → E
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
inst_3 : PartialOrder E
inst_4 : ClosedIciTopology E
inst_5 : IsOrderedAddMonoid E
inst_6 : IsOrderedModule ℝ E
hf : Integrable f μ
hg : Integrable g μ
hfg : f ≤ᶠ[ae μ] g
hm : ¬m ≤ m₀
⊢ μ[f | m] ≤ᶠ[ae μ] μ[g | m]
have neg : EventuallyLE.{u_1, u_3} (β := E) (ae μ) 0 0
Tactic: simp_rw [condExp_of_not_le hm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic (goal)
Goal:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f g : α → E
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
inst_3 : PartialOrder E
inst_4 : ClosedIciTopology E
inst_5 : IsOrderedAddMonoid E
inst_6 : IsOrderedModule ℝ E
hf : Integrable f μ
hg : Integrable g μ
hfg : f ≤ᶠ[ae μ] g
hm : m ≤ m₀
⊢ μ[f | m] ≤ᶠ[ae μ] μ[g | m]
have pos : ∀ (hμm : SigmaFinite (μ.trim hm)), μ[f | m] ≤ᶠ[ae μ] μ[g | m]
Tactic: by_cases hμm : SigmaFinite (μ.trim hm)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic (goal)
Goal:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f g : α → E
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
inst_3 : PartialOrder E
inst_4 : ClosedIciTopology E
inst_5 : IsOrderedAddMonoid E
inst_6 : IsOrderedModule ℝ E
hf : Integrable f μ
hg : Integrable g μ
hfg : f ≤ᶠ[ae μ] g
hm : m ≤ m₀
pos : ∀ (hμm : SigmaFinite (μ.trim hm)), μ[f | m] ≤ᶠ[ae μ] μ[g | m]
⊢ μ[f | m] ≤ᶠ[ae μ] μ[g | m]
have neg : ∀ (hμm : ¬SigmaFinite (μ.trim hm)), μ[f | m] ≤ᶠ[ae μ] μ[g | m]
Tactic: by_cases hμm : SigmaFinite (μ.trim hm)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic (goal)
Goal:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f g : α → E
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
inst_3 : PartialOrder E
inst_4 : ClosedIciTopology E
inst_5 : IsOrderedAddMonoid E
inst_6 : IsOrderedModule ℝ E
hf : Integrable f μ
hg : Integrable g μ
hfg : f ≤ᶠ[ae μ] g
hm : m ≤ m₀
hμm : ¬SigmaFinite (μ.trim hm)
⊢ μ[f | m] ≤ᶠ[ae μ] μ[g | m]
have neg : EventuallyLE.{u_1, u_3} (β := E) (ae μ) 0 0
Tactic: simp_rw [condExp_of_not_sigmaFinite hm hμm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic (goal)
Goal:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
inst_3 : PartialOrder E
inst_4 : ClosedIciTopology E
inst_5 : IsOrderedAddMonoid E
inst_6 : IsOrderedModule ℝ E
hf : 0 ≤ᶠ[ae μ] f
⊢ 0 ≤ᶠ[ae μ] μ[f | m]
have pos : ∀ (hfint : Integrable f μ), 0 ≤ᶠ[ae μ] μ[f | m]
Tactic: by_cases hfint : Integrable f μ
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic (goal)
Goal:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
inst_3 : PartialOrder E
inst_4 : ClosedIciTopology E
inst_5 : IsOrderedAddMonoid E
inst_6 : IsOrderedModule ℝ E
hf : 0 ≤ᶠ[ae μ] f
pos : ∀ (hfint : Integrable f μ), 0 ≤ᶠ[ae μ] μ[f | m]
⊢ 0 ≤ᶠ[ae μ] μ[f | m]
have neg : ∀ (hfint : ¬Integrable f μ), 0 ≤ᶠ[ae μ] μ[f | m]
Tactic: by_cases hfint : Integrable f μ
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic (goal)
Goal:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
inst_3 : PartialOrder E
inst_4 : ClosedIciTopology E
inst_5 : IsOrderedAddMonoid E
inst_6 : IsOrderedModule ℝ E
hf : 0 ≤ᶠ[ae μ] f
hfint : Integrable f μ
⊢ 0 ≤ᶠ[ae μ] μ[f | m]
have pos : μ[0 | m] ≤ᶠ[ae μ] μ[f | m]
Tactic: rw [(condExp_zero.symm : (0 : α → E) = μ[0 | m])]