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
φ : 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)
refine_1 : ∀ (i : ℕ), Integrable ((⇑(L i) : (a : E) → ℝ) ∘ f + const α (c i)) μ
refine_2 : ∀ (i : ℕ), (⇑(L i) : (a : E) → ℝ) ∘ f + const α (c i) ≤ᶠ[ae μ] φ ∘ f
⊢ ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), μ[(⇑(L i) : (a : E) → ℝ) ∘ f + const α (c i) | m] a ≤ μ[φ ∘ f | m] a

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

Premises used: Iff.mpr, MeasureTheory.condExp_mono, MeasureTheory.ae_all_iff
-- 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)
i : ℕ
⊢ Integrable ((⇑(L i) : (a : E) → ℝ) ∘ f + const α (c i)) μ

Tactic:
((L i).integrable_comp hf_int).add (integrable_const (c i))

Premises used: ContinuousLinearMap.integrable_comp, MeasureTheory.Integrable.add, MeasureTheory.integrable_const
-- 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)
i : ℕ
⊢ Integrable ((⇑(L i) : (a : E) → ℝ) ∘ f + const α (c i)) μ

Tactic:
exact ((L i).integrable_comp hf_int).add (integrable_const (c i))

Premises used: ContinuousLinearMap.integrable_comp, MeasureTheory.Integrable.add, MeasureTheory.integrable_const
-- 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)
i : ℕ
a : α
ha : f a ∈ s
⊢ HAdd.hAdd (α := α → ℝ) ((⇑(L i) : (a : E) → ℝ) ∘ f) (const α (c i)) a ≤ (φ ∘ f) a

Tactic:
hLc1 i ⟨f a, ha⟩

Premises used: Subtype.mk, Set.restrict
-- 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)
i : ℕ
h :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x : α |
        Membership.mem (γ := Set α) {x : α | (fun (a : α) ↦ f a ∈ s) x} x →
          Membership.mem (γ := Set α)
            {x : α |
              (fun (x : α) ↦ HAdd.hAdd (α := α → ℝ) ((⇑(L i) : (a : E) → ℝ) ∘ f) (const α (c i)) x ≤ (φ ∘ f) x) x}
            x}
      a
h₁ h₂ : ∀ (a : α) (ha : f a ∈ s), HAdd.hAdd (α := α → ℝ) ((⇑(L i) : (a : E) → ℝ) ∘ f) (const α (c i)) a ≤ (φ ∘ f) a
⊢ (⇑(L i) : (a : E) → ℝ) ∘ f + const α (c i) ≤ᶠ[ae μ] φ ∘ f

Tactic:
filter_upwards [hf] with a ha using hLc1 i ⟨f 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
φ : 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:
have hw : ∀ᵐ a ∂μ, ∀ i : ℕ, μ[(L i) ∘ f + const α (c i) | m] a ≤ μ[φ ∘ f | m] a := by
    refine ae_all_iff.2 fun i => condExp_mono ?_ hφ_int ?_
    · exact ((L i).integrable_comp hf_int).add (integrable_const (c i))
    · filter_upwards [hf] with a ha using hLc1 i ⟨f 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
φ : 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)
hw : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), μ[(⇑(L i) : (a : E) → ℝ) ∘ f + const α (c i) | m] a ≤ μ[φ ∘ f | m] a
h :
  ∀ (a : α)
    (hp :
      ∀ (i : ℕ),
        HAdd.hAdd (α := ℝ) ((L i : (a : E) → ℝ) (μ[f | m] a) : ℝ) (c i) =
          μ[fun (y : α) ↦ HAdd.hAdd (α := ℝ) ((L i : (a : E) → ℝ) (f y) : ℝ) (c i) | m] a)
    (hw : ∀ (i : ℕ), μ[(⇑(L i) : (a : E) → ℝ) ∘ f + const α (c i) | m] a ≤ μ[φ ∘ f | m] a) (hq : μ[f | m] a ∈ s),
    φ (μ[f | m] a) ≤ μ[φ ∘ f | m] a
⊢ ∀ᵐ (a : α) ∂μ, φ (μ[f | m] a) ≤ μ[φ ∘ f | m] a

Tactic:
filter_upwards [hp, hw, hφ_cvx.1.condExp_mem hm hf_int hs hf] with a hp hw hq

Premises used: And.left, Convex.condExp_mem
-- 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_1 :
  ∀ᵐ (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)
hw_1 : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), μ[(⇑(L i) : (a : E) → ℝ) ∘ f + const α (c i) | m] a ≤ μ[φ ∘ f | m] a
a : α
hp :
  ∀ (i : ℕ),
    HAdd.hAdd (α := ℝ) ((L i : (a : E) → ℝ) (μ[f | m] a) : ℝ) (c i) =
      μ[fun (y : α) ↦ HAdd.hAdd (α := ℝ) ((L i : (a : E) → ℝ) (f y) : ℝ) (c i) | m] a
hw : ∀ (i : ℕ), μ[(⇑(L i) : (a : E) → ℝ) ∘ f + const α (c i) | m] a ≤ μ[φ ∘ f | m] a
hq : μ[f | m] a ∈ s
⊢ φ (μ[f | m] a) = s.restrict (π := fun (a : E) ↦ ℝ) φ (Subtype.mk (p := fun (x : E) ↦ x ∈ s) (μ[f | m] a) hq)

Tactic:
simp
-- 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_1 :
  ∀ᵐ (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)
hw_1 : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), μ[(⇑(L i) : (a : E) → ℝ) ∘ f + const α (c i) | m] a ≤ μ[φ ∘ f | m] a
a : α
hp :
  ∀ (i : ℕ),
    HAdd.hAdd (α := ℝ) ((L i : (a : E) → ℝ) (μ[f | m] a) : ℝ) (c i) =
      μ[fun (y : α) ↦ HAdd.hAdd (α := ℝ) ((L i : (a : E) → ℝ) (f y) : ℝ) (c i) | m] a
hw : ∀ (i : ℕ), μ[(⇑(L i) : (a : E) → ℝ) ∘ f + const α (c i) | m] a ≤ μ[φ ∘ f | m] a
hq : μ[f | m] a ∈ s
h :
  (⨆ (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)))
      (Subtype.mk (p := fun (x : E) ↦ x ∈ s) (μ[f | m] a) hq) ≤
    μ[φ ∘ f | m] a
⊢ φ (μ[f | m] a) ≤ μ[φ ∘ f | m] a

Tactic:
rw [show φ (μ[f | m] a) = s.restrict φ ⟨μ[f | m] a, hq⟩ by simp, ← hLc2]
-- 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_1 :
  ∀ᵐ (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)
hw_1 : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), μ[(⇑(L i) : (a : E) → ℝ) ∘ f + const α (c i) | m] a ≤ μ[φ ∘ f | m] a
a : α
hp :
  ∀ (i : ℕ),
    HAdd.hAdd (α := ℝ) ((L i : (a : E) → ℝ) (μ[f | m] a) : ℝ) (c i) =
      μ[fun (y : α) ↦ HAdd.hAdd (α := ℝ) ((L i : (a : E) → ℝ) (f y) : ℝ) (c i) | m] a
hw : ∀ (i : ℕ), μ[(⇑(L i) : (a : E) → ℝ) ∘ f + const α (c i) | m] a ≤ μ[φ ∘ f | m] a
hq : μ[f | m] a ∈ s
⊢ (⨆ (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)))
      (Subtype.mk (p := fun (x : E) ↦ x ∈ s) (μ[f | m] a) hq) ≤
    μ[φ ∘ f | m] a

Tactic:
simpa [iSup_congr hp] using ciSup_le hw

Premises used: iSup_congr, ciSup_le
-- 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 μ
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) μ
⊢ let this := borel E;
  BorelSpace E

Tactic:
borelize E
-- 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 μ
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) μ
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
obtain :
  ∀ (t : Set E) (ht : TopologicalSpace.IsSeparable t) (htt : ∀ᵐ (x : α) ∂μ, f x ∈ t), φ ∘ μ[f | m] ≤ᶠ[ae μ] μ[φ ∘ f | m]
⊢ φ ∘ μ[f | m] ≤ᶠ[ae μ] μ[φ ∘ f | m]

Tactic:
obtain ⟨t, ht, htt⟩ := hf_int.aestronglyMeasurable.isSeparable_ae_range

Premises used: MeasureTheory.Integrable.aestronglyMeasurable, MeasureTheory.AEStronglyMeasurable.isSeparable_ae_range
-- 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 μ
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) μ
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)
⊢ CompleteSpace.{u_1} ↥Y

Tactic:
have : CompleteSpace Y := (Submodule.isClosed_topologicalClosure _).completeSpace_coe
-- 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 μ
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) μ
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
⊢ SecondCountableTopology.{u_1} ↥Y

Tactic:
have : SecondCountableTopology Y := ht.span.closure.secondCountableTopology
-- 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 μ
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) μ
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
φY : ↥Y → ℝ := φ ∘ (⇑Y.subtypeL : (a : ↥Y) → E)
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 : α
ha : f a ∈ t
⊢ f a ∈ Y

Tactic:
(Submodule.closure_subset_topologicalClosure_span t) (subset_closure ha)

Premises used: Submodule.closure_subset_topologicalClosure_span, Set.Mem, subset_closure
-- 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 μ
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) μ
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
φY : ↥Y → ℝ := φ ∘ (⇑Y.subtypeL : (a : ↥Y) → E)
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
h₁ h₂ : ∀ (a : α) (ha : f a ∈ t), f a ∈ Y
⊢ ∀ᵐ (a : α) ∂μ, f a ∈ Y

Tactic:
filter_upwards [htt] with a ha using
      (Submodule.closure_subset_topologicalClosure_span t) (subset_closure 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
φ : E → ℝ
m mα : MeasurableSpace α
μ : Measure α
s : Set E
inst_3 : IsFiniteMeasure μ
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) μ
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
φY : ↥Y → ℝ := φ ∘ (⇑Y.subtypeL : (a : ↥Y) → E)
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

Tactic:
have lem0 : ∀ᵐ a ∂μ, f a ∈ Y := by
    filter_upwards [htt] with a ha using
      (Submodule.closure_subset_topologicalClosure_span t) (subset_closure ha)