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 : 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 neg : EventuallyLE.{u_1, u_3} (β := E) (ae μ) 0 0
Tactic: rw [condExp_of_not_integrable hfint]
-- 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 : f ≤ᶠ[ae μ] 0
⊢ μ[f | m] ≤ᶠ[ae μ] 0
have pos : ∀ (hfint : Integrable f μ), μ[f | m] ≤ᶠ[ae μ] 0
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 : f ≤ᶠ[ae μ] 0
pos : ∀ (hfint : Integrable f μ), μ[f | m] ≤ᶠ[ae μ] 0
⊢ μ[f | m] ≤ᶠ[ae μ] 0
have neg : ∀ (hfint : ¬Integrable f μ), μ[f | m] ≤ᶠ[ae μ] 0
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 : f ≤ᶠ[ae μ] 0
hfint : Integrable f μ
⊢ μ[f | m] ≤ᶠ[ae μ] 0
have pos : μ[f | m] ≤ᶠ[ae μ] μ[0 | m]
Tactic: rw [(condExp_zero.symm : (0 : α → E) = μ[0 | 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 : f ≤ᶠ[ae μ] 0
hfint : ¬Integrable f μ
⊢ μ[f | m] ≤ᶠ[ae μ] 0
have neg : EventuallyLE.{u_1, u_3} (β := E) (ae μ) 0 0
Tactic: rw [condExp_of_not_integrable hfint]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondJensen (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
α : Type u_2
f : α → E
m mα : MeasurableSpace α
μ : Measure α
s : Set E
inst_3 : IsFiniteMeasure μ
inst_4 : HereditarilyLindelofSpace E
hm : m ≤ mα
hf_int : Integrable f μ
hs : IsClosed s
hc : Convex ℝ s
hf : ∀ᵐ (a : α) ∂μ, f a ∈ s
⊢ ∀ᵐ (a : α) ∂μ, μ[f | m] a ∈ s
have obtain : ∀ (L : ℕ → StrongDual ℝ E) (c : ℕ → ℝ)
  (hLc : ⋂ (n : ℕ), {x : E | (RCLike.re : (a : ℝ) → ℝ) ((L n : (a : E) → ℝ) x : ℝ) ≤ c n} = s),
  ∀ᵐ (a : α) ∂μ, μ[f | m] a ∈ s
Tactic: obtain ⟨L, c, hLc⟩ := RCLike.iInter_countable_halfSpaces_eq (𝕜 := ℝ) hc hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondJensen (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
α : Type u_2
f : α → E
m mα : MeasurableSpace α
μ : Measure α
s : Set E
inst_3 : IsFiniteMeasure μ
inst_4 : HereditarilyLindelofSpace E
hm : m ≤ mα
hf_int : Integrable f μ
hs : IsClosed s
hc : Convex ℝ s
hf : ∀ᵐ (a : α) ∂μ, f a ∈ s
L : ℕ → StrongDual ℝ E
c : ℕ → ℝ
hLc : ⋂ (n : ℕ), {x : E | (RCLike.re : (a : ℝ) → ℝ) ((L n : (a : E) → ℝ) x : ℝ) ≤ c n} = s
⊢ ∀ᵐ (a : α) ∂μ, μ[f | m] a ∈ s
have simp_all : ∀ (hs : IsClosed.{u_1} (X := E) (⋂ (n : ℕ), {x : E | (L n : (a : E) → ℝ) x ≤ c n}))
  (hc : Convex.{0, u_1} ℝ (E := E) (⋂ (n : ℕ), {x : E | (L n : (a : E) → ℝ) x ≤ c n}))
  (hf : ∀ (i : ℕ), ∀ᵐ (a : α) ∂μ, Membership.mem (γ := Set E) {x : E | (L i : (a : E) → ℝ) x ≤ c i} (f a)) (i : ℕ),
  ∀ᵐ (a : α) ∂μ, Membership.mem (γ := Set E) {x : E | (L i : (a : E) → ℝ) x ≤ c i} (μ[f | m] a)
Tactic: simp_all only [← hLc, RCLike.re_to_real, mem_iInter, ae_all_iff]
Cleared hypotheses: hs, hc, hf, hLc
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondJensen (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
α : Type u_2
f : α → E
m mα : MeasurableSpace α
μ : Measure α
s : Set E
inst_3 : IsFiniteMeasure μ
inst_4 : HereditarilyLindelofSpace E
hm : m ≤ mα
hf_int : Integrable f μ
L : ℕ → StrongDual ℝ E
c : ℕ → ℝ
hs : IsClosed.{u_1} (X := E) (⋂ (n : ℕ), {x : E | (L n : (a : E) → ℝ) x ≤ c n})
hc : Convex.{0, u_1} ℝ (E := E) (⋂ (n : ℕ), {x : E | (L n : (a : E) → ℝ) x ≤ c n})
hf : ∀ (i : ℕ), ∀ᵐ (a : α) ∂μ, Membership.mem (γ := Set E) {x : E | (L i : (a : E) → ℝ) x ≤ c i} (f a)
n : ℕ
⊢ ∀ᵐ (a : α) ∂μ, Membership.mem (γ := Set E) {x : E | (L n : (a : E) → ℝ) x ≤ c n} (μ[f | m] a)
have h1 : (ae μ).EventuallyEq (β := ℝ) ((⇑(L n) : (a : E) → ℝ) ∘ μ[f | m]) μ[(⇑(L n) : (a : E) → ℝ) ∘ f | m]
Tactic: have h1 := ContinuousLinearMap.comp_condExp_comm (m := m) hf_int (L n)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondJensen (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
α : Type u_2
f : α → E
m mα : MeasurableSpace α
μ : Measure α
s : Set E
inst_3 : IsFiniteMeasure μ
inst_4 : HereditarilyLindelofSpace E
hm : m ≤ mα
hf_int : Integrable f μ
L : ℕ → StrongDual ℝ E
c : ℕ → ℝ
hs : IsClosed.{u_1} (X := E) (⋂ (n : ℕ), {x : E | (L n : (a : E) → ℝ) x ≤ c n})
hc : Convex.{0, u_1} ℝ (E := E) (⋂ (n : ℕ), {x : E | (L n : (a : E) → ℝ) x ≤ c n})
hf : ∀ (i : ℕ), ∀ᵐ (a : α) ∂μ, Membership.mem (γ := Set E) {x : E | (L i : (a : E) → ℝ) x ≤ c i} (f a)
n : ℕ
h1 : (ae μ).EventuallyEq (β := ℝ) ((⇑(L n) : (a : E) → ℝ) ∘ μ[f | m]) μ[(⇑(L n) : (a : E) → ℝ) ∘ f | m]
⊢ ∀ᵐ (a : α) ∂μ, Membership.mem (γ := Set E) {x : E | (L n : (a : E) → ℝ) x ≤ c n} (μ[f | m] a)
have h2 : (ae μ).EventuallyLE (β := ℝ) μ[fun (a : α) ↦ (L n : (a : E) → ℝ) (f a) | m] μ[fun (x : α) ↦ c n | m]
Tactic: have h2 := condExp_mono (m := m) ((L n).integrable_comp hf_int) (integrable_const (c n)) (hf n)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondJensen (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
α : Type u_2
f : α → E
m mα : MeasurableSpace α
μ : Measure α
s : Set E
inst_3 : IsFiniteMeasure μ
inst_4 : HereditarilyLindelofSpace E
hm : m ≤ mα
hf_int : Integrable f μ
L : ℕ → StrongDual ℝ E
c : ℕ → ℝ
hs : IsClosed.{u_1} (X := E) (⋂ (n : ℕ), {x : E | (L n : (a : E) → ℝ) x ≤ c n})
hc : Convex.{0, u_1} ℝ (E := E) (⋂ (n : ℕ), {x : E | (L n : (a : E) → ℝ) x ≤ c n})
hf : ∀ (i : ℕ), ∀ᵐ (a : α) ∂μ, Membership.mem (γ := Set E) {x : E | (L i : (a : E) → ℝ) x ≤ c i} (f a)
n : ℕ
h1 : (ae μ).EventuallyEq (β := ℝ) ((⇑(L n) : (a : E) → ℝ) ∘ μ[f | m]) μ[(⇑(L n) : (a : E) → ℝ) ∘ f | m]
h2 : (ae μ).EventuallyLE (β := ℝ) μ[fun (a : α) ↦ (L n : (a : E) → ℝ) (f a) | m] μ[fun (x : α) ↦ c n | m]
⊢ ∀ᵐ (a : α) ∂μ, Membership.mem (γ := Set E) {x : E | (L n : (a : E) → ℝ) x ≤ c n} (μ[f | m] a)
have h : ∀ (a : α) (ha : Eq (α := ℝ) (((⇑(L n) : (a : E) → ℝ) ∘ μ[f | m]) a) (μ[(⇑(L n) : (a : E) → ℝ) ∘ f | m] a))
  (hb : LE.le (α := ℝ) (μ[fun (a : α) ↦ (L n : (a : E) → ℝ) (f a) | m] a) (μ[fun (x : α) ↦ c n | m] a)),
  (L n : (a : E) → ℝ) (μ[f | m] a) ≤ c n
Tactic: filter_upwards [h1, h2] with a ha hb
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondJensen (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
α : Type u_2
f : α → E
m mα : MeasurableSpace α
μ : Measure α
s : Set E
inst_3 : IsFiniteMeasure μ
inst_4 : HereditarilyLindelofSpace E
hm : m ≤ mα
hf_int : Integrable f μ
L : ℕ → StrongDual ℝ E
c : ℕ → ℝ
hs : IsClosed.{u_1} (X := E) (⋂ (n : ℕ), {x : E | (L n : (a : E) → ℝ) x ≤ c n})
hc : Convex.{0, u_1} ℝ (E := E) (⋂ (n : ℕ), {x : E | (L n : (a : E) → ℝ) x ≤ c n})
hf : ∀ (i : ℕ), ∀ᵐ (a : α) ∂μ, Membership.mem (γ := Set E) {x : E | (L i : (a : E) → ℝ) x ≤ c i} (f a)
n : ℕ
h1 : (ae μ).EventuallyEq (β := ℝ) ((⇑(L n) : (a : E) → ℝ) ∘ μ[f | m]) μ[(⇑(L n) : (a : E) → ℝ) ∘ f | m]
h2 : (ae μ).EventuallyLE (β := ℝ) μ[fun (a : α) ↦ (L n : (a : E) → ℝ) (f a) | m] μ[fun (x : α) ↦ c n | m]
a : α
ha : Eq (α := ℝ) (((⇑(L n) : (a : E) → ℝ) ∘ μ[f | m]) a) (μ[(⇑(L n) : (a : E) → ℝ) ∘ f | m] a)
hb : LE.le (α := ℝ) (μ[fun (a : α) ↦ (L n : (a : E) → ℝ) (f a) | m] a) (μ[fun (x : α) ↦ c n | m] a)
⊢ (L n : (a : E) → ℝ) (μ[f | m] a) ≤ c n
have h : ∀ (h2 : (ae μ).EventuallyLE (β := ℝ) μ[fun (a : α) ↦ (L n : (a : E) → ℝ) (f a) | m] fun (x : α) ↦ c n)
  (ha : Eq (α := ℝ) ((L n : (a : E) → ℝ) (μ[f | m] a) : ℝ) (μ[(⇑(L n) : (a : E) → ℝ) ∘ f | m] a : ℝ))
  (hb : μ[fun (a : α) ↦ (L n : (a : E) → ℝ) (f a) | m] a ≤ c n), μ[(⇑(L n) : (a : E) → ℝ) ∘ f | m] a ≤ c n
Tactic: simp_all only [condExp_const, comp_apply]
Cleared hypotheses: h2, ha, hb
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondJensen (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
α : Type u_2
f : α → E
m mα : MeasurableSpace α
μ : Measure α
s : Set E
inst_3 : IsFiniteMeasure μ
hm : m ≤ mα
hf_int : Integrable f μ
hs : IsClosed s
hc : Convex ℝ s
hf : ∀ᵐ (a : α) ∂μ, f a ∈ s
⊢ ∀ᵐ (a : α) ∂μ, μ[f | m] a ∈ s
have this : let this := borel E;
BorelSpace E
Tactic: borelize E
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondJensen (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
α : Type u_2
f : α → E
m mα : MeasurableSpace α
μ : Measure α
s : Set E
inst_3 : IsFiniteMeasure μ
hm : m ≤ mα
hf_int : Integrable f μ
hs : IsClosed s
hc : Convex ℝ s
hf : ∀ᵐ (a : α) ∂μ, f a ∈ s
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
⊢ ∀ᵐ (a : α) ∂μ, μ[f | m] a ∈ s
have obtain : ∀ (t : Set E) (ht : TopologicalSpace.IsSeparable t) (htt : ∀ᵐ (x : α) ∂μ, f x ∈ t), ∀ᵐ (a : α) ∂μ, μ[f | m] a ∈ s
Tactic: obtain ⟨t, ht, htt⟩ := hf_int.aestronglyMeasurable.isSeparable_ae_range
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondJensen (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
α : Type u_2
f : α → E
m mα : MeasurableSpace α
μ : Measure α
s : Set E
inst_3 : IsFiniteMeasure μ
hm : m ≤ mα
hf_int : Integrable f μ
hs : IsClosed s
hc : Convex ℝ s
hf : ∀ᵐ (a : α) ∂μ, f a ∈ s
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
t : Set E
ht : TopologicalSpace.IsSeparable t
htt : ∀ᵐ (x : α) ∂μ, f x ∈ t
Y : Submodule ℝ E := Submodule.topologicalClosure (Submodule.span ℝ t)
⊢ ∀ᵐ (a : α) ∂μ, μ[f | m] a ∈ s
have this : CompleteSpace.{u_1} ↥Y
Tactic: have : CompleteSpace Y := (Submodule.isClosed_topologicalClosure _).completeSpace_coe
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondJensen (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
α : Type u_2
f : α → E
m mα : MeasurableSpace α
μ : Measure α
s : Set E
inst_3 : IsFiniteMeasure μ
hm : m ≤ mα
hf_int : Integrable f μ
hs : IsClosed s
hc : Convex ℝ s
hf : ∀ᵐ (a : α) ∂μ, f a ∈ s
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
t : Set E
ht : TopologicalSpace.IsSeparable t
htt : ∀ᵐ (x : α) ∂μ, f x ∈ t
Y : Submodule ℝ E := Submodule.topologicalClosure (Submodule.span ℝ t)
this : CompleteSpace.{u_1} ↥Y
⊢ ∀ᵐ (a : α) ∂μ, μ[f | m] a ∈ s
have this₁ : SecondCountableTopology.{u_1} ↥Y
Tactic: have : SecondCountableTopology Y := ht.span.closure.secondCountableTopology
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondJensen (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
α : Type u_2
f : α → E
m mα : MeasurableSpace α
μ : Measure α
s : Set E
inst_3 : IsFiniteMeasure μ
hm : m ≤ mα
hf_int : Integrable f μ
hs : IsClosed s
hc : Convex ℝ s
hf : ∀ᵐ (a : α) ∂μ, f a ∈ s
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
t : Set E
ht : TopologicalSpace.IsSeparable t
htt : ∀ᵐ (x : α) ∂μ, f x ∈ t
Y : Submodule ℝ E := Submodule.topologicalClosure (Submodule.span ℝ t)
this_3 : CompleteSpace.{u_1} ↥Y
this : SecondCountableTopology.{u_1} ↥Y
fY : α → ↥Y := fun (a : α) ↦ if h : f a ∈ Y then Subtype.mk (p := fun (x : E) ↦ x ∈ Y) (f a) h else 0
fX : α → E := (⇑Y.subtypeL : (a : ↥Y) → E) ∘ fY
⊢ ∀ᵐ (a : α) ∂μ, f a ∈ Y
have h : ∀ (a : α),
  Membership.mem (γ := Set α)
    {x : α |
      Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ f x ∈ t) x} x →
        Membership.mem (γ := Set α) {x : α | (fun (a : α) ↦ f a ∈ Y) x} x}
    a
Tactic: filter_upwards [htt] with a ha using
      (Submodule.closure_subset_topologicalClosure_span t) (subset_closure ha)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondJensen (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
α : Type u_2
f : α → E
m mα : MeasurableSpace α
μ : Measure α
s : Set E
inst_3 : IsFiniteMeasure μ
hm : m ≤ mα
hf_int : Integrable f μ
hs : IsClosed s
hc : Convex ℝ s
hf : ∀ᵐ (a : α) ∂μ, f a ∈ s
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
t : Set E
ht : TopologicalSpace.IsSeparable t
htt : ∀ᵐ (x : α) ∂μ, f x ∈ t
Y : Submodule ℝ E := Submodule.topologicalClosure (Submodule.span ℝ t)
this_3 : CompleteSpace.{u_1} ↥Y
this : SecondCountableTopology.{u_1} ↥Y
fY : α → ↥Y := fun (a : α) ↦ if h : f a ∈ Y then Subtype.mk (p := fun (x : E) ↦ x ∈ Y) (f a) h else 0
fX : α → E := (⇑Y.subtypeL : (a : ↥Y) → E) ∘ fY
h :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x : α |
        Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ f x ∈ t) x} x →
          Membership.mem (γ := Set α) {x : α | (fun (a : α) ↦ f a ∈ Y) x} x}
      a
⊢ ∀ᵐ (a : α) ∂μ, f a ∈ Y
have h₁ : ∀ (a : α), f a ∈ t → f a ∈ Y
Tactic: filter_upwards [htt] with a ha using
      (Submodule.closure_subset_topologicalClosure_span t) (subset_closure ha)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondJensen (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
α : Type u_2
f : α → E
m mα : MeasurableSpace α
μ : Measure α
s : Set E
inst_3 : IsFiniteMeasure μ
hm : m ≤ mα
hf_int : Integrable f μ
hs : IsClosed s
hc : Convex ℝ s
hf : ∀ᵐ (a : α) ∂μ, f a ∈ s
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
t : Set E
ht : TopologicalSpace.IsSeparable t
htt : ∀ᵐ (x : α) ∂μ, f x ∈ t
Y : Submodule ℝ E := Submodule.topologicalClosure (Submodule.span ℝ t)
this_3 : CompleteSpace.{u_1} ↥Y
this : SecondCountableTopology.{u_1} ↥Y
fY : α → ↥Y := fun (a : α) ↦ if h : f a ∈ Y then Subtype.mk (p := fun (x : E) ↦ x ∈ Y) (f a) h else 0
fX : α → E := (⇑Y.subtypeL : (a : ↥Y) → E) ∘ fY
⊢ ∀ᵐ (a : α) ∂μ, μ[f | m] a ∈ s
have lem0 : ∀ᵐ (a : α) ∂μ, f a ∈ Y
Tactic: have lem0 : ∀ᵐ a ∂μ, f a ∈ Y := by
    filter_upwards [htt] with a ha using
      (Submodule.closure_subset_topologicalClosure_span t) (subset_closure ha)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondJensen (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
α : Type u_2
f : α → E
m mα : MeasurableSpace α
μ : Measure α
s : Set E
inst_3 : IsFiniteMeasure μ
hm : m ≤ mα
hf_int : Integrable f μ
hs : IsClosed s
hc : Convex ℝ s
hf : ∀ᵐ (a : α) ∂μ, f a ∈ s
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
t : Set E
ht : TopologicalSpace.IsSeparable t
htt : ∀ᵐ (x : α) ∂μ, f x ∈ t
Y : Submodule ℝ E := Submodule.topologicalClosure (Submodule.span ℝ t)
this_3 : CompleteSpace.{u_1} ↥Y
this : SecondCountableTopology.{u_1} ↥Y
fY : α → ↥Y := fun (a : α) ↦ if h : f a ∈ Y then Subtype.mk (p := fun (x : E) ↦ x ∈ Y) (f a) h else 0
fX : α → E := (⇑Y.subtypeL : (a : ↥Y) → E) ∘ fY
lem0 : ∀ᵐ (a : α) ∂μ, f a ∈ Y
⊢ f =ᶠ[ae μ] fX
have h : ∀ (a : α) (ha : f a ∈ Y), f a = fX a
Tactic: filter_upwards [lem0] with a ha
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondJensen (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
α : Type u_2
f : α → E
m mα : MeasurableSpace α
μ : Measure α
s : Set E
inst_3 : IsFiniteMeasure μ
hm : m ≤ mα
hf_int : Integrable f μ
hs : IsClosed s
hc : Convex ℝ s
hf : ∀ᵐ (a : α) ∂μ, f a ∈ s
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
t : Set E
ht : TopologicalSpace.IsSeparable t
htt : ∀ᵐ (x : α) ∂μ, f x ∈ t
Y : Submodule ℝ E := Submodule.topologicalClosure (Submodule.span ℝ t)
this_3 : CompleteSpace.{u_1} ↥Y
this : SecondCountableTopology.{u_1} ↥Y
fY : α → ↥Y := fun (a : α) ↦ if h : f a ∈ Y then Subtype.mk (p := fun (x : E) ↦ x ∈ Y) (f a) h else 0
fX : α → E := (⇑Y.subtypeL : (a : ↥Y) → E) ∘ fY
lem0 : ∀ᵐ (a : α) ∂μ, f a ∈ Y
⊢ ∀ᵐ (a : α) ∂μ, μ[f | m] a ∈ s
have lem1 : f =ᶠ[ae μ] fX
Tactic: have lem1 : f =ᵐ[μ] fX := by
    filter_upwards [lem0] with a ha
    simp_all [fX, fY]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondJensen (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
α : Type u_2
f : α → E
m mα : MeasurableSpace α
μ : Measure α
s : Set E
inst_3 : IsFiniteMeasure μ
hm : m ≤ mα
hf_int : Integrable f μ
hs : IsClosed s
hc : Convex ℝ s
hf : ∀ᵐ (a : α) ∂μ, f a ∈ s
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
t : Set E
ht : TopologicalSpace.IsSeparable t
htt : ∀ᵐ (x : α) ∂μ, f x ∈ t
Y : Submodule ℝ E := Submodule.topologicalClosure (Submodule.span ℝ t)
this_3 : CompleteSpace.{u_1} ↥Y
this : SecondCountableTopology.{u_1} ↥Y
fY : α → ↥Y := fun (a : α) ↦ if h : f a ∈ Y then Subtype.mk (p := fun (x : E) ↦ x ∈ Y) (f a) h else 0
fX : α → E := (⇑Y.subtypeL : (a : ↥Y) → E) ∘ fY
lem0 : ∀ᵐ (a : α) ∂μ, f a ∈ Y
lem1 : f =ᶠ[ae μ] fX
⊢ ∀ᵐ (a : α) ∂μ, Membership.mem (γ := Set ↥Y) ((⇑Y.subtypeL : (a : ↥Y) → E) ⁻¹' s) (fY a)
have h : ∀ (a : α) (ha : f a ∈ Y) (hs : f a ∈ s), Membership.mem (γ := Set ↥Y) ((⇑Y.subtypeL : (a : ↥Y) → E) ⁻¹' s) (fY a)
Tactic: filter_upwards [lem0, hf] with a ha hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondJensen (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
α : Type u_2
f : α → E
m mα : MeasurableSpace α
μ : Measure α
s : Set E
inst_3 : IsFiniteMeasure μ
hm : m ≤ mα
hf_int : Integrable f μ
hs : IsClosed s
hc : Convex ℝ s
hf : ∀ᵐ (a : α) ∂μ, f a ∈ s
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
t : Set E
ht : TopologicalSpace.IsSeparable t
htt : ∀ᵐ (x : α) ∂μ, f x ∈ t
Y : Submodule ℝ E := Submodule.topologicalClosure (Submodule.span ℝ t)
this_3 : CompleteSpace.{u_1} ↥Y
this : SecondCountableTopology.{u_1} ↥Y
fY : α → ↥Y := fun (a : α) ↦ if h : f a ∈ Y then Subtype.mk (p := fun (x : E) ↦ x ∈ Y) (f a) h else 0
fX : α → E := (⇑Y.subtypeL : (a : ↥Y) → E) ∘ fY
lem0 : ∀ᵐ (a : α) ∂μ, f a ∈ Y
lem1 : f =ᶠ[ae μ] fX
⊢ ∀ᵐ (a : α) ∂μ, μ[f | m] a ∈ s
have lem2 : ∀ᵐ (a : α) ∂μ, Membership.mem (γ := Set ↥Y) ((⇑Y.subtypeL : (a : ↥Y) → E) ⁻¹' s) (fY a)
Tactic: have lem2 : ∀ᵐ a ∂μ, fY a ∈ Y.subtypeL ⁻¹' s := by
    filter_upwards [lem0, hf] with a ha hs
    simpa [fY, ha]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondJensen (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
α : Type u_2
f : α → E
m mα : MeasurableSpace α
μ : Measure α
s : Set E
inst_3 : IsFiniteMeasure μ
hm : m ≤ mα
hf_int : Integrable f μ
hs : IsClosed s
hc : Convex ℝ s
hf : ∀ᵐ (a : α) ∂μ, f a ∈ s
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
t : Set E
ht : TopologicalSpace.IsSeparable t
htt : ∀ᵐ (x : α) ∂μ, f x ∈ t
Y : Submodule ℝ E := Submodule.topologicalClosure (Submodule.span ℝ t)
this_3 : CompleteSpace.{u_1} ↥Y
this : SecondCountableTopology.{u_1} ↥Y
fY : α → ↥Y := fun (a : α) ↦ if h : f a ∈ Y then Subtype.mk (p := fun (x : E) ↦ x ∈ Y) (f a) h else 0
fX : α → E := (⇑Y.subtypeL : (a : ↥Y) → E) ∘ fY
lem0 : ∀ᵐ (a : α) ∂μ, f a ∈ Y
lem1 : f =ᶠ[ae μ] fX
lem2 : ∀ᵐ (a : α) ∂μ, Membership.mem (γ := Set ↥Y) ((⇑Y.subtypeL : (a : ↥Y) → E) ⁻¹' s) (fY a)
⊢ Integrable fY μ
have refine : AEStronglyMeasurable fY μ
Tactic: refine (hf_int.congr lem1).mono ?_ (by simp [fX])
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondJensen (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
α : Type u_2
f : α → E
m mα : MeasurableSpace α
μ : Measure α
s : Set E
inst_3 : IsFiniteMeasure μ
hm : m ≤ mα
hf_int : Integrable f μ
hs : IsClosed s
hc : Convex ℝ s
hf : ∀ᵐ (a : α) ∂μ, f a ∈ s
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
t : Set E
ht : TopologicalSpace.IsSeparable t
htt : ∀ᵐ (x : α) ∂μ, f x ∈ t
Y : Submodule ℝ E := Submodule.topologicalClosure (Submodule.span ℝ t)
this_3 : CompleteSpace.{u_1} ↥Y
this : SecondCountableTopology.{u_1} ↥Y
fY : α → ↥Y := fun (a : α) ↦ if h : f a ∈ Y then Subtype.mk (p := fun (x : E) ↦ x ∈ Y) (f a) h else 0
fX : α → E := (⇑Y.subtypeL : (a : ↥Y) → E) ∘ fY
lem0 : ∀ᵐ (a : α) ∂μ, f a ∈ Y
lem1 : f =ᶠ[ae μ] fX
lem2 : ∀ᵐ (a : α) ∂μ, Membership.mem (γ := Set ↥Y) ((⇑Y.subtypeL : (a : ↥Y) → E) ⁻¹' s) (fY a)
⊢ AEStronglyMeasurable fY μ
have obtain : ∀ (g : α → E) (hg1 : StronglyMeasurable g)
  (hg2 : ∀ (x : α), g x ∈ (↑(Submodule.topologicalClosure (Submodule.span ℝ t)) : Set E)) (hg3 : f =ᶠ[ae μ] g),
  AEStronglyMeasurable fY μ
Tactic: obtain ⟨g, hg1, hg2, hg3⟩ := hf_int.1.exists_stronglyMeasurable_range_subset
      ((Submodule.isClosed_topologicalClosure _).measurableSet) Nonempty.of_subtype lem0
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondJensen (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
α : Type u_2
f : α → E
m mα : MeasurableSpace α
μ : Measure α
s : Set E
inst_3 : IsFiniteMeasure μ
hm : m ≤ mα
hf_int : Integrable f μ
hs : IsClosed s
hc : Convex ℝ s
hf : ∀ᵐ (a : α) ∂μ, f a ∈ s
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
t : Set E
ht : TopologicalSpace.IsSeparable t
htt : ∀ᵐ (x : α) ∂μ, f x ∈ t
Y : Submodule ℝ E := Submodule.topologicalClosure (Submodule.span ℝ t)
this_3 : CompleteSpace.{u_1} ↥Y
this : SecondCountableTopology.{u_1} ↥Y
fY : α → ↥Y := fun (a : α) ↦ if h : f a ∈ Y then Subtype.mk (p := fun (x : E) ↦ x ∈ Y) (f a) h else 0
fX : α → E := (⇑Y.subtypeL : (a : ↥Y) → E) ∘ fY
lem0 : ∀ᵐ (a : α) ∂μ, f a ∈ Y
lem1 : f =ᶠ[ae μ] fX
lem2 : ∀ᵐ (a : α) ∂μ, Membership.mem (γ := Set ↥Y) ((⇑Y.subtypeL : (a : ↥Y) → E) ⁻¹' s) (fY a)
g : α → E
hg1 : StronglyMeasurable g
hg2 : ∀ (x : α), g x ∈ (↑(Submodule.topologicalClosure (Submodule.span ℝ t)) : Set E)
hg3 : f =ᶠ[ae μ] g
⊢ AEStronglyMeasurable fY μ
have refine : fY =ᶠ[ae μ] codRestrict g (↑Y : Set E) hg2
Tactic: refine ⟨codRestrict g Y hg2, (hg1.measurable.codRestrict hg2).stronglyMeasurable, ?_⟩