awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
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)
⊢ EventuallyEq.{u_1, u_3} (β := E) (ae μ) 0 0

Tactic:
rfl
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
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]

Tactic:
(condExp_ae_eq_condExpL1 hm f).trans ((condExp_ae_eq_condExpL1 hm g).trans ?_).symm

Premises used: Filter.EventuallyEq.trans, MeasureTheory.condExp_ae_eq_condExpL1, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
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)
pos : (↑(↑(condExpL1 hm μ g) : α →ₘ[μ] E) : α → E) =ᶠ[ae μ] (↑(↑(condExpL1 hm μ f) : α →ₘ[μ] E) : α → E)
⊢ μ[f | m] =ᶠ[ae μ] μ[g | m]

Tactic:
refine (condExp_ae_eq_condExpL1 hm f).trans ((condExp_ae_eq_condExpL1 hm g).trans ?_).symm

Premises used: Filter.EventuallyEq.trans, MeasureTheory.condExp_ae_eq_condExpL1, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
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)
pos : Eq (α := ↥(Lp E 1 μ)) (condExpL1 hm μ g) (condExpL1 hm μ f)
⊢ (↑(↑(condExpL1 hm μ g) : α →ₘ[μ] E) : α → E) =ᶠ[ae μ] (↑(↑(condExpL1 hm μ f) : α →ₘ[μ] E) : α → E)

Tactic:
rw [← Lp.ext_iff]

Premises used: MeasureTheory.Lp.ext_iff
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
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 : ℕ
h : (↑(↑(condExpL1 hm μ (gs n)) : α →ₘ[μ] E) : α → E) =ᶠ[ae μ] (↑(↑(condExpL1 hm μ (fs n)) : α →ₘ[μ] E) : α → E)
⊢ Eq (α := ↥(Lp E 1 μ)) (condExpL1 hm μ (gs n)) (condExpL1 hm μ (fs n))

Tactic:
ext1
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
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)

Tactic:
(condExp_ae_eq_condExpL1 hm (gs n)).symm.trans ((hfg n).symm.trans ?_)

Premises used: Filter.EventuallyEq.trans, MeasureTheory.condExp_ae_eq_condExpL1, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
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 : ℕ
h : μ[fs n | m] =ᶠ[ae μ] (↑(↑(condExpL1 hm μ (fs n)) : α →ₘ[μ] E) : α → E)
⊢ (↑(↑(condExpL1 hm μ (gs n)) : α →ₘ[μ] E) : α → E) =ᶠ[ae μ] (↑(↑(condExpL1 hm μ (fs n)) : α →ₘ[μ] E) : α → E)

Tactic:
refine (condExp_ae_eq_condExpL1 hm (gs n)).symm.trans ((hfg n).symm.trans ?_)

Premises used: Filter.EventuallyEq.trans, MeasureTheory.condExp_ae_eq_condExpL1, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
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 : ℕ
⊢ μ[fs n | m] =ᶠ[ae μ] (↑(↑(condExpL1 hm μ (fs n)) : α →ₘ[μ] E) : α → E)

Tactic:
condExp_ae_eq_condExpL1 hm (fs n)

Premises used: MeasureTheory.condExp_ae_eq_condExpL1
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
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 : ℕ
⊢ μ[fs n | m] =ᶠ[ae μ] (↑(↑(condExpL1 hm μ (fs n)) : α →ₘ[μ] E) : α → E)

Tactic:
exact condExp_ae_eq_condExpL1 hm (fs n)

Premises used: MeasureTheory.condExp_ae_eq_condExpL1
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
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))

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)
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
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))
⊢ 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
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
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))
⊢ 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
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
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))
hcond_gs : Tendsto (β := ↥(Lp E 1 μ)) (fun (n : ℕ) ↦ condExpL1 hm μ (gs n)) atTop (𝓝 (condExpL1 hm μ g))
⊢ Eq (α := ↥(Lp E 1 μ)) (condExpL1 hm μ g) (condExpL1 hm μ f)

Tactic:
tendsto_nhds_unique_of_eventuallyEq hcond_gs hcond_fs (Eventually.of_forall hn_eq)

Premises used: Filter.Eventually.of_forall, tendsto_nhds_unique_of_eventuallyEq
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
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))
hcond_gs : Tendsto (β := ↥(Lp E 1 μ)) (fun (n : ℕ) ↦ condExpL1 hm μ (gs n)) atTop (𝓝 (condExpL1 hm μ g))
⊢ Eq (α := ↥(Lp E 1 μ)) (condExpL1 hm μ g) (condExpL1 hm μ f)

Tactic:
exact tendsto_nhds_unique_of_eventuallyEq hcond_gs hcond_fs (Eventually.of_forall hn_eq)

Premises used: Filter.Eventually.of_forall, tendsto_nhds_unique_of_eventuallyEq
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
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]
neg : ∀ (hm : ¬m ≤ m₀), μ[f | m] ≤ᶠ[ae μ] μ[g | m]
⊢ μ[f | m] ≤ᶠ[ae μ] μ[g | m]

Tactic:
by_cases hm : m ≤ m₀
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
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₀
neg : EventuallyLE.{u_1, u_3} (β := E) (ae μ) 0 0
⊢ μ[f | m] ≤ᶠ[ae μ] μ[g | m]

Tactic:
simp_rw [condExp_of_not_le hm]

Premises used: MeasureTheory.condExp_of_not_le
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
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₀
⊢ EventuallyLE.{u_1, u_3} (β := E) (ae μ) 0 0

Tactic:
rfl
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
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]
neg : ∀ (hμm : ¬SigmaFinite (μ.trim hm)), μ[f | m] ≤ᶠ[ae μ] μ[g | m]
⊢ μ[f | m] ≤ᶠ[ae μ] μ[g | m]

Tactic:
by_cases hμm : SigmaFinite (μ.trim hm)

Premises used: MeasureTheory.SigmaFinite, MeasureTheory.Measure.trim
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
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)
neg : EventuallyLE.{u_1, u_3} (β := E) (ae μ) 0 0
⊢ μ[f | m] ≤ᶠ[ae μ] μ[g | m]

Tactic:
simp_rw [condExp_of_not_sigmaFinite hm hμm]

Premises used: MeasureTheory.condExp_of_not_sigmaFinite
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
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)
⊢ EventuallyLE.{u_1, u_3} (β := E) (ae μ) 0 0

Tactic:
rfl
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
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]

Tactic:
(condExp_ae_eq_condExpL1 hm _).trans_le
    ((condExpL1_mono hf hg hfg).trans_eq (condExp_ae_eq_condExpL1 hm _).symm)

Premises used: Filter.EventuallyLE.trans_eq, Filter.EventuallyEq.trans_le, MeasureTheory.condExp_ae_eq_condExpL1, MeasureTheory.condExpL1_mono, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
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]

Tactic:
exact (condExp_ae_eq_condExpL1 hm _).trans_le
    ((condExpL1_mono hf hg hfg).trans_eq (condExp_ae_eq_condExpL1 hm _).symm)

Premises used: Filter.EventuallyLE.trans_eq, Filter.EventuallyEq.trans_le, MeasureTheory.condExp_ae_eq_condExpL1, MeasureTheory.condExpL1_mono, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
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]
neg : ∀ (hfint : ¬Integrable f μ), 0 ≤ᶠ[ae μ] μ[f | m]
⊢ 0 ≤ᶠ[ae μ] μ[f | m]

Tactic:
by_cases hfint : Integrable f μ

Premises used: MeasureTheory.Integrable
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
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 μ
pos : μ[0 | m] ≤ᶠ[ae μ] μ[f | m]
⊢ 0 ≤ᶠ[ae μ] μ[f | m]

Tactic:
rw [(condExp_zero.symm : (0 : α → E) = μ[0 | m])]

Premises used: MeasureTheory.condExp_zero, Eq.symm
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
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 | m] ≤ᶠ[ae μ] μ[f | m]

Tactic:
condExp_mono (integrable_zero _ _ _) hfint hf

Premises used: MeasureTheory.condExp_mono, MeasureTheory.integrable_zero
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
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 | m] ≤ᶠ[ae μ] μ[f | m]

Tactic:
exact condExp_mono (integrable_zero _ _ _) hfint hf

Premises used: MeasureTheory.condExp_mono
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
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 μ
neg neg₁ : EventuallyLE.{u_1, u_3} (β := E) (ae μ) 0 0
⊢ 0 ≤ᶠ[ae μ] μ[f | m]

Tactic:
rw [condExp_of_not_integrable hfint]

Premises used: MeasureTheory.condExp_of_not_integrable
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
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 : f ≤ᶠ[ae μ] 0
pos : ∀ (hfint : Integrable f μ), μ[f | m] ≤ᶠ[ae μ] 0
neg : ∀ (hfint : ¬Integrable f μ), μ[f | m] ≤ᶠ[ae μ] 0
⊢ μ[f | m] ≤ᶠ[ae μ] 0

Tactic:
by_cases hfint : Integrable f μ

Premises used: MeasureTheory.Integrable
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
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 : f ≤ᶠ[ae μ] 0
hfint : Integrable f μ
pos : μ[f | m] ≤ᶠ[ae μ] μ[0 | m]
⊢ μ[f | m] ≤ᶠ[ae μ] 0

Tactic:
rw [(condExp_zero.symm : (0 : α → E) = μ[0 | m])]

Premises used: MeasureTheory.condExp_zero, Eq.symm