awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondJensen
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)
obtain :
  ∀ (g : α → E) (hg1 : StronglyMeasurable g)
    (hg2 : ∀ (x : α), g x ∈ (↑(Submodule.topologicalClosure (Submodule.span ℝ t)) : Set E)) (hg3 : f =ᶠ[ae μ] g),
    AEStronglyMeasurable fY μ
⊢ AEStronglyMeasurable fY μ

Tactic:
obtain ⟨g, hg1, hg2, hg3⟩ := hf_int.1.exists_stronglyMeasurable_range_subset
      ((Submodule.isClosed_topologicalClosure _).measurableSet) Nonempty.of_subtype lem0

Premises used: Set.Nonempty.of_subtype, Submodule.isClosed_topologicalClosure, IsClosed.measurableSet, And.left, MeasureTheory.AEStronglyMeasurable.exists_stronglyMeasurable_range_subset
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondJensen
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 μ

Tactic:
⟨codRestrict g Y hg2, (hg1.measurable.codRestrict hg2).stronglyMeasurable, ?_⟩

Premises used: Measurable.codRestrict, Measurable.stronglyMeasurable, MeasureTheory.StronglyMeasurable.measurable, SetLike.coe, And.intro, Exists.intro, Set.codRestrict, MeasureTheory.AEStronglyMeasurable
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondJensen
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
refine : fY =ᶠ[ae μ] codRestrict g (↑Y : Set E) hg2
⊢ AEStronglyMeasurable fY μ

Tactic:
refine ⟨codRestrict g Y hg2, (hg1.measurable.codRestrict hg2).stronglyMeasurable, ?_⟩
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondJensen
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
h : ∀ (a : α) (ha : f a = g a), fY a = codRestrict g (↑Y : Set E) hg2 a
⊢ fY =ᶠ[ae μ] codRestrict g (↑Y : Set E) hg2

Tactic:
filter_upwards [hg3] with a ha
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondJensen
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
a : α
ha : f a = g a
⊢ g a ∈ Y

Tactic:
have : g a ∈ Y := hg2 a
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondJensen
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_4 : 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
a : α
ha : f a = g a
this : g a ∈ Y
⊢ fY a = codRestrict g (↑Y : Set E) hg2 a

Tactic:
simp_all [fY, codRestrict]

Premises used: Set.codRestrict
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondJensen
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 μ

Tactic:
have hfY_int : Integrable fY μ := by
    refine (hf_int.congr lem1).mono ?_ (by simp [fX])
    obtain ⟨g, hg1, hg2, hg3⟩ := hf_int.1.exists_stronglyMeasurable_range_subset
      ((Submodule.isClosed_topologicalClosure _).measurableSet) Nonempty.of_subtype lem0
    refine ⟨codRestrict g Y hg2, (hg1.measurable.codRestrict hg2).stronglyMeasurable, ?_⟩
    filter_upwards [hg3] with a ha
    have : g a ∈ Y := hg2 a
    simp_all [fY, codRestrict]
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondJensen
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)
hfY_int : Integrable fY μ
⊢ μ[f | m] =ᶠ[ae μ] (⇑Y.subtypeL : (a : ↥Y) → E) ∘ μ[fY | m]

Tactic:
have lem3 : μ[f | m] =ᵐ[μ] Y.subtypeL ∘ μ[fY | m] := calc
    _ =ᵐ[μ] μ[fX | m] := condExp_congr_ae lem1
    _ =ᵐ[μ] _ := (Y.subtypeL.comp_condExp_comm hfY_int).symm
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondJensen
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)
hfY_int : Integrable fY μ
lem3 : μ[f | m] =ᶠ[ae μ] (⇑Y.subtypeL : (a : ↥Y) → E) ∘ μ[fY | m]
h :
  ∀ (a : α) (ha : Membership.mem (γ := Set ↥Y) ((⇑Y.subtypeL : (a : ↥Y) → E) ⁻¹' s) (μ[fY | m] a))
    (hb : μ[f | m] a = ((⇑Y.subtypeL : (a : ↥Y) → E) ∘ μ[fY | m]) a), μ[f | m] a ∈ s
⊢ ∀ᵐ (a : α) ∂μ, μ[f | m] a ∈ s

Tactic:
filter_upwards [(hc.linear_preimage Y.subtype).condExp_mem_of_hereditarilyLindelofSpace
    hm hfY_int (hs.preimage Y.subtypeL.continuous) lem2, lem3] with a ha hb

Premises used: Submodule.subtypeL, _private.0.Convex.condExp_mem_of_hereditarilyLindelofSpace, ContinuousLinearMap.continuous, Submodule.subtype, IsClosed.preimage, Convex.linear_preimage
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondJensen
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)
hfY_int : Integrable fY μ
lem3 : μ[f | m] =ᶠ[ae μ] (⇑Y.subtypeL : (a : ↥Y) → E) ∘ μ[fY | m]
a : α
ha : Membership.mem (γ := Set ↥Y) ((⇑Y.subtypeL : (a : ↥Y) → E) ⁻¹' s) (μ[fY | m] a)
hb : μ[f | m] a = ((⇑Y.subtypeL : (a : ↥Y) → E) ∘ μ[fY | m]) a
⊢ μ[f | m] a ∈ s

Tactic:
simp_all
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondJensen
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
hm : m ≤ mα
inst_3 : SigmaFinite (μ.trim hm)
hf_int : Integrable f μ
hs : IsClosed s
hc : Convex ℝ s
hf : ∀ᵐ (a : α) ∂μ, f a ∈ s
hm₁ : range (spanningSets (μ.trim hm)) ⊆ MeasurableSet
ht :
  ∀ t ∈ range (spanningSets (μ.trim hm)),
    Eq (α := ENNReal) ((μ.restrict t : (a : Set α) → ENNReal) {x : α | (fun (a : α) ↦ μ[f | m] a ∈ s) x}ᶜ : ENNReal)
      (0 : ENNReal)
⊢ ∀ᵐ (a : α) ∂μ, μ[f | m] a ∈ s

Tactic:
apply (isCountablySpanning_spanningSets (μ.trim hm)).null_of_forall_restrict_null

Premises used: MeasureTheory.Measure.trim, MeasureTheory.isCountablySpanning_spanningSets, IsCountablySpanning.null_of_forall_restrict_null
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondJensen
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
hm : m ≤ mα
inst_3 : SigmaFinite (μ.trim hm)
hf_int : Integrable f μ
hs : IsClosed s
hc : Convex ℝ s
hf : ∀ᵐ (a : α) ∂μ, f a ∈ s
n : ℕ
⊢ Membership.mem (γ := Set (Set α)) MeasurableSet (spanningSets (μ.trim hm) n)

Tactic:
hm _ (measurableSet_spanningSets (μ.trim hm) n)

Premises used: MeasurableSet, Set.Mem, MeasureTheory.Measure.trim, MeasureTheory.measurableSet_spanningSets
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondJensen
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
hm : m ≤ mα
inst_3 : SigmaFinite (μ.trim hm)
hf_int : Integrable f μ
hs : IsClosed s
hc : Convex ℝ s
hf : ∀ᵐ (a : α) ∂μ, f a ∈ s
n : ℕ
⊢ Membership.mem (γ := Set (Set α)) MeasurableSet (spanningSets (μ.trim hm) n)

Tactic:
exact hm _ (measurableSet_spanningSets (μ.trim hm) n)

Premises used: MeasureTheory.Measure.trim, MeasureTheory.measurableSet_spanningSets
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondJensen
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
hm : m ≤ mα
inst_3 : SigmaFinite (μ.trim hm)
hf_int : Integrable f μ
hs : IsClosed s
hc : Convex ℝ s
hf : ∀ᵐ (a : α) ∂μ, f a ∈ s
n : ℕ
⊢ (μ.restrict (spanningSets (μ.trim hm) n))[f | m] =ᶠ[ae (μ.restrict (spanningSets (μ.trim hm) n))] μ[f | m]

Tactic:
have h1 := condExp_restrict_ae_eq_restrict hm (measurableSet_spanningSets (μ.trim hm) n) hf_int
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondJensen
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
hm : m ≤ mα
inst_3 : SigmaFinite (μ.trim hm)
hf_int : Integrable f μ
hs : IsClosed s
hc : Convex ℝ s
hf : ∀ᵐ (a : α) ∂μ, f a ∈ s
n : ℕ
h1 : (μ.restrict (spanningSets (μ.trim hm) n))[f | m] =ᶠ[ae (μ.restrict (spanningSets (μ.trim hm) n))] μ[f | m]
⊢ IsFiniteMeasure (μ.restrict (spanningSets (μ.trim hm) n))

Tactic:
have : IsFiniteMeasure (μ.restrict (spanningSets (μ.trim hm) n)) := isFiniteMeasure_restrict.2
    ((le_trim hm).trans_lt (measure_spanningSets_lt_top (μ.trim hm) n)).ne
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondJensen
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
hm : m ≤ mα
inst_3 : SigmaFinite (μ.trim hm)
hf_int : Integrable f μ
hs : IsClosed s
hc : Convex ℝ s
hf : ∀ᵐ (a : α) ∂μ, f a ∈ s
n : ℕ
h1 : (μ.restrict (spanningSets (μ.trim hm) n))[f | m] =ᶠ[ae (μ.restrict (spanningSets (μ.trim hm) n))] μ[f | m]
this : IsFiniteMeasure (μ.restrict (spanningSets (μ.trim hm) n))
⊢ ∀ᵐ (a : α) ∂μ.restrict (spanningSets (μ.trim hm) n), (μ.restrict (spanningSets (μ.trim hm) n))[f | m] a ∈ s

Tactic:
have h2 := hc.condExp_mem_of_isFiniteMeasure (μ := μ.restrict (spanningSets (μ.trim hm) n)) hm
    hf_int.restrict hs (ae_restrict_of_ae hf)
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondJensen
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
hm : m ≤ mα
inst_3 : SigmaFinite (μ.trim hm)
hf_int : Integrable f μ
hs : IsClosed s
hc : Convex ℝ s
hf : ∀ᵐ (a : α) ∂μ, f a ∈ s
n : ℕ
h1 : (μ.restrict (spanningSets (μ.trim hm) n))[f | m] =ᶠ[ae (μ.restrict (spanningSets (μ.trim hm) n))] μ[f | m]
this : IsFiniteMeasure (μ.restrict (spanningSets (μ.trim hm) n))
h2 : ∀ᵐ (a : α) ∂μ.restrict (spanningSets (μ.trim hm) n), (μ.restrict (spanningSets (μ.trim hm) n))[f | m] a ∈ s
h :
  ∀ (a : α) (ha : (μ.restrict (spanningSets (μ.trim hm) n))[f | m] a = μ[f | m] a)
    (hb : (μ.restrict (spanningSets (μ.trim hm) n))[f | m] a ∈ s), μ[f | m] a ∈ s
⊢ Eq (α := ENNReal)
    ((μ.restrict (spanningSets (μ.trim hm) n) : (a : Set α) → ENNReal) {x : α | (fun (a : α) ↦ μ[f | m] a ∈ s) x}ᶜ :
      ENNReal)
    (0 : ENNReal)

Tactic:
filter_upwards [h1, h2] with a ha hb
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondJensen
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
hm : m ≤ mα
inst_3 : SigmaFinite (μ.trim hm)
hf_int : Integrable f μ
hs : IsClosed s
hc : Convex ℝ s
hf : ∀ᵐ (a : α) ∂μ, f a ∈ s
n : ℕ
h1 : (μ.restrict (spanningSets (μ.trim hm) n))[f | m] =ᶠ[ae (μ.restrict (spanningSets (μ.trim hm) n))] μ[f | m]
this : IsFiniteMeasure (μ.restrict (spanningSets (μ.trim hm) n))
h2 : ∀ᵐ (a : α) ∂μ.restrict (spanningSets (μ.trim hm) n), (μ.restrict (spanningSets (μ.trim hm) n))[f | m] a ∈ s
a : α
ha : (μ.restrict (spanningSets (μ.trim hm) n))[f | m] a = μ[f | m] a
hb : (μ.restrict (spanningSets (μ.trim hm) n))[f | m] a ∈ s
⊢ μ[f | m] a ∈ s

Tactic:
simp_all
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondJensen
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
α : Type u_2
f : α → E
φ : E → ℝ
m mα : MeasurableSpace α
μ : Measure α
s : Set E
inst_3 : IsFiniteMeasure μ
inst_4 : HereditarilyLindelofSpace E
hm : m ≤ mα
hφ_cvx : ConvexOn ℝ s φ
hφ_cont : LowerSemicontinuousOn φ s
hf : ∀ᵐ (a : α) ∂μ, f a ∈ s
hs : IsClosed s
hf_int : Integrable f μ
hφ_int : Integrable (φ ∘ f) μ
obtain :
  ∀ (L : ℕ → E →L[ℝ] ℝ) (c : ℕ → ℝ)
    (hLc1 :
      ∀ (i : ℕ),
        HAdd.hAdd (α := (a : (↑s : Type u_1)) → ℝ) (β := (↑s : Type u_1) → ℝ)
            (s.restrict (π := fun (a : E) ↦ ℝ) (⇑(L i) : (a : E) → ℝ) : (a : (↑s : Type u_1)) → ℝ)
            (const (↑s : Type u_1) (c i)) ≤
          s.restrict (π := fun (a : E) ↦ ℝ) φ)
    (hLc2 :
      ⨆ (i : ℕ),
          HAdd.hAdd (α := (a : (↑s : Type u_1)) → ℝ) (β := (↑s : Type u_1) → ℝ)
            (s.restrict (π := fun (a : E) ↦ ℝ) (⇑(L i) : (a : E) → ℝ) : (a : (↑s : Type u_1)) → ℝ)
            (const (↑s : Type u_1) (c i)) =
        s.restrict (π := fun (a : E) ↦ ℝ) φ),
    ∀ᵐ (a : α) ∂μ, φ (μ[f | m] a) ≤ μ[φ ∘ f | m] a
⊢ ∀ᵐ (a : α) ∂μ, φ (μ[f | m] a) ≤ μ[φ ∘ f | m] a

Tactic:
obtain ⟨L, c, hLc1, hLc2⟩ := hφ_cvx.real_sSup_of_nat_affine_eq hs hφ_cont

Premises used: ConvexOn.real_sSup_of_nat_affine_eq
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondJensen
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
α : Type u_2
f : α → E
φ : E → ℝ
m mα : MeasurableSpace α
μ : Measure α
s : Set E
inst_3 : IsFiniteMeasure μ
inst_4 : HereditarilyLindelofSpace E
hm : m ≤ mα
hφ_cvx : ConvexOn ℝ s φ
hφ_cont : LowerSemicontinuousOn φ s
hf : ∀ᵐ (a : α) ∂μ, f a ∈ s
hs : IsClosed s
hf_int : Integrable f μ
hφ_int : Integrable (φ ∘ f) μ
L : ℕ → E →L[ℝ] ℝ
c : ℕ → ℝ
hLc1 :
  ∀ (i : ℕ),
    HAdd.hAdd (α := (a : (↑s : Type u_1)) → ℝ) (β := (↑s : Type u_1) → ℝ)
        (s.restrict (π := fun (a : E) ↦ ℝ) (⇑(L i) : (a : E) → ℝ) : (a : (↑s : Type u_1)) → ℝ)
        (const (↑s : Type u_1) (c i)) ≤
      s.restrict (π := fun (a : E) ↦ ℝ) φ
hLc2 :
  ⨆ (i : ℕ),
      HAdd.hAdd (α := (a : (↑s : Type u_1)) → ℝ) (β := (↑s : Type u_1) → ℝ)
        (s.restrict (π := fun (a : E) ↦ ℝ) (⇑(L i) : (a : E) → ℝ) : (a : (↑s : Type u_1)) → ℝ)
        (const (↑s : Type u_1) (c i)) =
    s.restrict (π := fun (a : E) ↦ ℝ) φ
⊢ ∀ᵐ (a : α) ∂μ,
    ∀ (i : ℕ),
      Eq (α := ℝ) ((fun (x : α) ↦ HAdd.hAdd (α := ℝ) ((L i : (a : E) → ℝ) (μ[f | m] x) : ℝ) (c i)) a)
        (μ[fun (y : α) ↦ HAdd.hAdd (α := ℝ) ((L i : (a : E) → ℝ) (f y) : ℝ) (c i) | m] a)

Tactic:
have hp := ae_all_iff.2 fun i => (L i).comp_condExp_add_const_comm hm hf_int (c i)
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondJensen
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
α : Type u_2
f : α → E
φ : E → ℝ
m mα : MeasurableSpace α
μ : Measure α
s : Set E
inst_3 : IsFiniteMeasure μ
inst_4 : HereditarilyLindelofSpace E
hm : m ≤ mα
hφ_cvx : ConvexOn ℝ s φ
hφ_cont : LowerSemicontinuousOn φ s
hf : ∀ᵐ (a : α) ∂μ, f a ∈ s
hs : IsClosed s
hf_int : Integrable f μ
hφ_int : Integrable (φ ∘ f) μ
L : ℕ → E →L[ℝ] ℝ
c : ℕ → ℝ
hLc1 :
  ∀ (i : ℕ),
    HAdd.hAdd (α := (a : (↑s : Type u_1)) → ℝ) (β := (↑s : Type u_1) → ℝ)
        (s.restrict (π := fun (a : E) ↦ ℝ) (⇑(L i) : (a : E) → ℝ) : (a : (↑s : Type u_1)) → ℝ)
        (const (↑s : Type u_1) (c i)) ≤
      s.restrict (π := fun (a : E) ↦ ℝ) φ
hLc2 :
  ⨆ (i : ℕ),
      HAdd.hAdd (α := (a : (↑s : Type u_1)) → ℝ) (β := (↑s : Type u_1) → ℝ)
        (s.restrict (π := fun (a : E) ↦ ℝ) (⇑(L i) : (a : E) → ℝ) : (a : (↑s : Type u_1)) → ℝ)
        (const (↑s : Type u_1) (c i)) =
    s.restrict (π := fun (a : E) ↦ ℝ) φ
hp :
  ∀ᵐ (a : α) ∂μ,
    ∀ (i : ℕ),
      Eq (α := ℝ) ((fun (x : α) ↦ HAdd.hAdd (α := ℝ) ((L i : (a : E) → ℝ) (μ[f | m] x) : ℝ) (c i)) a)
        (μ[fun (y : α) ↦ HAdd.hAdd (α := ℝ) ((L i : (a : E) → ℝ) (f y) : ℝ) (c i) | m] a)
⊢ ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), μ[(⇑(L i) : (a : E) → ℝ) ∘ f + const α (c i) | m] a ≤ μ[φ ∘ f | m] a

Tactic:
ae_all_iff.2 fun i => condExp_mono ?_ hφ_int ?_

Premises used: Iff.mpr, MeasureTheory.condExp_mono, MeasureTheory.ae_all_iff