awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
φ : 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 : α) ∂μ, φ (μ[f | m] a) ≤ μ[φ ∘ f | m] a
have 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)
Tactic: have hp := ae_all_iff.2 fun i => (L i).comp_condExp_add_const_comm hm hf_int (c i)
-- 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
φ : 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
have refine_1 : ∀ (i : ℕ), Integrable ((⇑(L i) : (a : E) → ℝ) ∘ f + const α (c i)) μ
Tactic: refine ae_all_iff.2 fun i => condExp_mono ?_ hφ_int ?_
-- 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
φ : 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)) μ
⊢ ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), μ[(⇑(L i) : (a : E) → ℝ) ∘ f + const α (c i) | m] a ≤ μ[φ ∘ f | m] a
have refine_2 : ∀ (i : ℕ), (⇑(L i) : (a : E) → ℝ) ∘ f + const α (c i) ≤ᶠ[ae μ] φ ∘ f
Tactic: refine ae_all_iff.2 fun i => condExp_mono ?_ hφ_int ?_
-- 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
φ : 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 : ℕ
⊢ (⇑(L i) : (a : E) → ℝ) ∘ f + const α (c i) ≤ᶠ[ae μ] φ ∘ f
have 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
Tactic: filter_upwards [hf] with a ha using hLc1 i ⟨f a, 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
φ : 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
⊢ (⇑(L i) : (a : E) → ℝ) ∘ f + const α (c i) ≤ᶠ[ae μ] φ ∘ f
have h₁ : ∀ (a : α), f a ∈ s → HAdd.hAdd (α := α → ℝ) ((⇑(L i) : (a : E) → ℝ) ∘ f) (const α (c i)) a ≤ (φ ∘ f) a
Tactic: filter_upwards [hf] with a ha using hLc1 i ⟨f 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
φ : 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 : α) ∂μ, φ (μ[f | m] a) ≤ μ[φ ∘ f | m] a
have hw : ∀ᵐ (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⟩
-- 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
φ : 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
⊢ ∀ᵐ (a : α) ∂μ, φ (μ[f | m] a) ≤ μ[φ ∘ f | m] a
have 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
Tactic: filter_upwards [hp, hw, hφ_cvx.1.condExp_mem hm hf_int hs hf] with a hp hw hq
-- 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
φ : 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) ≤ μ[φ ∘ f | m] a
have 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
Tactic: rw [show φ (μ[f | m] a) = s.restrict φ ⟨μ[f | m] a, hq⟩ by simp, ← hLc2]
-- 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
φ : 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) μ
⊢ φ ∘ μ[f | m] ≤ᶠ[ae μ] μ[φ ∘ f | m]
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
φ : 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
⊢ φ ∘ μ[f | m] ≤ᶠ[ae μ] μ[φ ∘ f | m]
have obtain : ∀ (t : Set E) (ht : TopologicalSpace.IsSeparable t) (htt : ∀ᵐ (x : α) ∂μ, f x ∈ t), φ ∘ μ[f | m] ≤ᶠ[ae μ] μ[φ ∘ f | m]
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
φ : 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)
⊢ φ ∘ μ[f | m] ≤ᶠ[ae μ] μ[φ ∘ f | m]
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
φ : 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
⊢ φ ∘ μ[f | m] ≤ᶠ[ae μ] μ[φ ∘ f | m]
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
φ : 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
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
φ : 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
⊢ ∀ᵐ (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
φ : 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
⊢ φ ∘ μ[f | m] ≤ᶠ[ae μ] μ[φ ∘ f | m]
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
φ : 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
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
φ : 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
lem0 : ∀ᵐ (a : α) ∂μ, f a ∈ Y
⊢ φ ∘ μ[f | m] ≤ᶠ[ae μ] μ[φ ∘ f | m]
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
φ : 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
lem0 : ∀ᵐ (a : α) ∂μ, f a ∈ Y
lem1 : f =ᶠ[ae μ] fX
⊢ Integrable fY μ
have refine : AEStronglyMeasurable fY μ
Tactic: refine (hf_int.congr lem1).mono ?_ (by simp [fX])