awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
let let₁ let₂ let₃ : φ ∘ μ[f | m] ≤ᶠ[ae μ] μ[φ ∘ f | m]
⊢ φ ∘ μ[f | m] ≤ᶠ[ae μ] μ[φ ∘ f | m]
have let₄ : ∀ (lem0 : ∀ᵐ (a : α) ∂μ, f a ∈ Y), φ ∘ μ[f | m] ≤ᶠ[ae μ] μ[φ ∘ f | m]
Tactic: classical
  let fY : α → Y := fun a => if h : f a ∈ Y then ⟨f a, h⟩ else 0
  let fX : α → E := Y.subtypeL ∘ fY
  have lem0 : ∀ᵐ a ∂μ, f a ∈ Y := by
    filter_upwards [htt] with a ha using
      (Submodule.closure_subset_topologicalClosure_span t) (subset_closure ha)
  have lem1 : f =ᵐ[μ] fX := by
    filter_upwards [lem0] with a ha
    simp_all [fX, fY]
  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]
  have lem2 : μ[f | m] =ᵐ[μ] Y.subtypeL ∘ μ[fY | m] := calc
    _ =ᵐ[μ] μ[fX | m] := condExp_congr_ae lem1
    _ =ᵐ[μ] _ := (Y.subtypeL.comp_condExp_comm hfY_int).symm
  have lem3 : φ ∘ f =ᵐ[μ] φY ∘ fY := by filter_upwards [lem1] with a ha; simp [φY, ha, fX]
  calc
    φ ∘ μ[f | m]
      =ᵐ[μ] φY ∘ μ[fY | m] := by filter_upwards [lem2] with a ha; simp [φY, ha]
    _ ≤ᵐ[μ] μ[φY ∘ fY | m] := by
      refine (hφ_cvx.comp_linearMap Y.subtype).map_condExp_le_of_hereditarilyLindelofSpace
        (s := Y.subtypeL ⁻¹' s) hm ?_ ?_ ?_ hfY_int (Integrable.congr hφ_int lem3)
      · exact hφ_cont.comp (by fun_prop) fun x => by
          #adaptation_note /-- Before https://github.com/leanprover/lean4/pull/13166
          (replacing grind's canonicalizer with a type-directed normalizer), `grind` closed this
          goal. It is not yet clear whether this is due to defeq abuse in Mathlib or a problem
          in the new canonicalizer; a minimization would help. The original proof was: `grind` -/
          simp
      · filter_upwards [lem0, hf] with a ha hb
        simp_all [fY]
      · exact hs.preimage Y.subtypeL.continuous
    _ =ᵐ[μ] μ[φ ∘ f | m] := condExp_congr_ae lem3.symm
-- 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
hm : m ≤ mα
inst_3 : SigmaFinite (μ.trim hm)
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 hm₁ : range (spanningSets (μ.trim hm)) ⊆ MeasurableSet
Tactic: apply (isCountablySpanning_spanningSets (μ.trim hm)).null_of_forall_restrict_null
-- 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
hm : m ≤ mα
inst_3 : SigmaFinite (μ.trim hm)
hφ_cvx : ConvexOn ℝ s φ
hφ_cont : LowerSemicontinuousOn φ s
hf : ∀ᵐ (a : α) ∂μ, f a ∈ s
hs : IsClosed s
hf_int : Integrable f μ
hφ_int : Integrable (φ ∘ f) μ
hm₁ : range (spanningSets (μ.trim hm)) ⊆ MeasurableSet
⊢ φ ∘ μ[f | m] ≤ᶠ[ae μ] μ[φ ∘ f | m]
have ht : ∀ t ∈ range (spanningSets (μ.trim hm)),
  Eq (α := ENNReal)
    ((μ.restrict t : (a : Set α) → ENNReal) {x : α | (fun (x : α) ↦ (φ ∘ μ[f | m]) x ≤ μ[φ ∘ f | m] x) x}ᶜ : ENNReal)
    (0 : ENNReal)
Tactic: apply (isCountablySpanning_spanningSets (μ.trim hm)).null_of_forall_restrict_null
-- 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
hm : m ≤ mα
inst_3 : SigmaFinite (μ.trim hm)
hφ_cvx : ConvexOn ℝ s φ
hφ_cont : LowerSemicontinuousOn φ s
hf : ∀ᵐ (a : α) ∂μ, f a ∈ s
hs : IsClosed s
hf_int : Integrable f μ
hφ_int : Integrable (φ ∘ f) μ
n : ℕ
⊢ Eq (α := ENNReal)
    ((μ.restrict (spanningSets (μ.trim hm) n) : (a : Set α) → ENNReal)
        {x : α | (fun (x : α) ↦ (φ ∘ μ[f | m]) x ≤ μ[φ ∘ f | m] x) x}ᶜ :
      ENNReal)
    (0 : ENNReal)
have h1 : (μ.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
-- 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
hm : m ≤ mα
inst_3 : SigmaFinite (μ.trim hm)
hφ_cvx : ConvexOn ℝ s φ
hφ_cont : LowerSemicontinuousOn φ s
hf : ∀ᵐ (a : α) ∂μ, f a ∈ s
hs : IsClosed s
hf_int : Integrable f μ
hφ_int : Integrable (φ ∘ f) μ
n : ℕ
h1 : (μ.restrict (spanningSets (μ.trim hm) n))[f | m] =ᶠ[ae (μ.restrict (spanningSets (μ.trim hm) n))] μ[f | m]
⊢ Eq (α := ENNReal)
    ((μ.restrict (spanningSets (μ.trim hm) n) : (a : Set α) → ENNReal)
        {x : α | (fun (x : α) ↦ (φ ∘ μ[f | m]) x ≤ μ[φ ∘ f | m] x) x}ᶜ :
      ENNReal)
    (0 : ENNReal)
have h2 : (μ.restrict (spanningSets (μ.trim hm) n))[φ ∘ f | m] =ᶠ[ae (μ.restrict (spanningSets (μ.trim hm) n))] μ[φ ∘ f | m]
Tactic: have h2 := condExp_restrict_ae_eq_restrict hm (measurableSet_spanningSets (μ.trim hm) n) hφ_int
-- 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
hm : m ≤ mα
inst_3 : SigmaFinite (μ.trim hm)
hφ_cvx : ConvexOn ℝ s φ
hφ_cont : LowerSemicontinuousOn φ s
hf : ∀ᵐ (a : α) ∂μ, f a ∈ s
hs : IsClosed s
hf_int : Integrable f μ
hφ_int : Integrable (φ ∘ f) μ
n : ℕ
h1 : (μ.restrict (spanningSets (μ.trim hm) n))[f | m] =ᶠ[ae (μ.restrict (spanningSets (μ.trim hm) n))] μ[f | m]
h2 : (μ.restrict (spanningSets (μ.trim hm) n))[φ ∘ f | m] =ᶠ[ae (μ.restrict (spanningSets (μ.trim hm) n))] μ[φ ∘ f | m]
⊢ Eq (α := ENNReal)
    ((μ.restrict (spanningSets (μ.trim hm) n) : (a : Set α) → ENNReal)
        {x : α | (fun (x : α) ↦ (φ ∘ μ[f | m]) x ≤ μ[φ ∘ f | m] x) x}ᶜ :
      ENNReal)
    (0 : ENNReal)
have this : 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
-- 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
hm : m ≤ mα
inst_3 : SigmaFinite (μ.trim hm)
hφ_cvx : ConvexOn ℝ s φ
hφ_cont : LowerSemicontinuousOn φ s
hf : ∀ᵐ (a : α) ∂μ, f a ∈ s
hs : IsClosed s
hf_int : Integrable f μ
hφ_int : Integrable (φ ∘ f) μ
n : ℕ
h1 : (μ.restrict (spanningSets (μ.trim hm) n))[f | m] =ᶠ[ae (μ.restrict (spanningSets (μ.trim hm) n))] μ[f | m]
h2 : (μ.restrict (spanningSets (μ.trim hm) n))[φ ∘ f | m] =ᶠ[ae (μ.restrict (spanningSets (μ.trim hm) n))] μ[φ ∘ f | m]
this : IsFiniteMeasure (μ.restrict (spanningSets (μ.trim hm) n))
⊢ Eq (α := ENNReal)
    ((μ.restrict (spanningSets (μ.trim hm) n) : (a : Set α) → ENNReal)
        {x : α | (fun (x : α) ↦ (φ ∘ μ[f | m]) x ≤ μ[φ ∘ f | m] x) x}ᶜ :
      ENNReal)
    (0 : ENNReal)
have h3 : φ ∘ (μ.restrict (spanningSets (μ.trim hm) n))[f | m] ≤ᶠ[ae (μ.restrict (spanningSets (μ.trim hm) n))]
  (μ.restrict (spanningSets (μ.trim hm) n))[φ ∘ f | m]
Tactic: have h3 := hφ_cvx.map_condExp_le_of_isFiniteMeasure (μ := μ.restrict (spanningSets (μ.trim hm) n))
    hm hφ_cont (ae_restrict_of_ae hf) hs hf_int.restrict hφ_int.restrict
-- 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
hm : m ≤ mα
inst_3 : SigmaFinite (μ.trim hm)
hφ_cvx : ConvexOn ℝ s φ
hφ_cont : LowerSemicontinuousOn φ s
hf : ∀ᵐ (a : α) ∂μ, f a ∈ s
hs : IsClosed s
hf_int : Integrable f μ
hφ_int : Integrable (φ ∘ f) μ
n : ℕ
h1 : (μ.restrict (spanningSets (μ.trim hm) n))[f | m] =ᶠ[ae (μ.restrict (spanningSets (μ.trim hm) n))] μ[f | m]
h2 : (μ.restrict (spanningSets (μ.trim hm) n))[φ ∘ f | m] =ᶠ[ae (μ.restrict (spanningSets (μ.trim hm) n))] μ[φ ∘ f | m]
this : IsFiniteMeasure (μ.restrict (spanningSets (μ.trim hm) n))
h3 :
  φ ∘ (μ.restrict (spanningSets (μ.trim hm) n))[f | m] ≤ᶠ[ae (μ.restrict (spanningSets (μ.trim hm) n))]
    (μ.restrict (spanningSets (μ.trim hm) n))[φ ∘ f | m]
⊢ Eq (α := ENNReal)
    ((μ.restrict (spanningSets (μ.trim hm) n) : (a : Set α) → ENNReal)
        {x : α | (fun (x : α) ↦ (φ ∘ μ[f | m]) x ≤ μ[φ ∘ f | m] x) x}ᶜ :
      ENNReal)
    (0 : ENNReal)
have h : ∀ (a : α) (ha : (μ.restrict (spanningSets (μ.trim hm) n))[f | m] a = μ[f | m] a)
  (hb : (μ.restrict (spanningSets (μ.trim hm) n))[φ ∘ f | m] a = μ[φ ∘ f | m] a)
  (hc :
    (φ ∘ (μ.restrict (spanningSets (μ.trim hm) n))[f | m]) a ≤ (μ.restrict (spanningSets (μ.trim hm) n))[φ ∘ f | m] a),
  (φ ∘ μ[f | m]) a ≤ μ[φ ∘ f | m] a
Tactic: filter_upwards [h1, h2, h3] with a ha hb hc
-- 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
hm : m ≤ mα
inst_3 : SigmaFinite (μ.trim hm)
hφ_cvx : ConcaveOn ℝ s φ
hφ_cont : UpperSemicontinuousOn φ s
hf : ∀ᵐ (a : α) ∂μ, f a ∈ s
hs : IsClosed s
hf_int : Integrable f μ
hφ_int : Integrable (φ ∘ f) μ
⊢ μ[φ ∘ f | m] ≤ᶠ[ae μ] φ ∘ μ[f | m]
have h : ∀ (a : α) (h : ((-φ) ∘ μ[f | m]) a ≤ μ[(-φ) ∘ f | m] a) (ha : μ[-φ ∘ f | m] a = (-μ[φ ∘ f | m]) a),
  μ[φ ∘ f | m] a ≤ (φ ∘ μ[f | m]) a
Tactic: filter_upwards [hφ_cvx.neg.map_condExp_le hm hφ_cont.neg hf hs hf_int hφ_int.neg,
    condExp_neg (φ ∘ f) m] with a h 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 α
hm : m ≤ mα
inst_3 : SigmaFinite (μ.trim hm)
hφ_cvx : ConcaveOn ℝ univ φ
hφ_cont : UpperSemicontinuous φ
hf_int : Integrable f μ
hφ_int : Integrable (φ ∘ f) μ
⊢ μ[φ ∘ f | m] ≤ᶠ[ae μ] φ ∘ μ[f | m]
have h : ∀ (a : α) (h : ((-φ) ∘ μ[f | m]) a ≤ μ[(-φ) ∘ f | m] a) (ha : μ[-φ ∘ f | m] a = (-μ[φ ∘ f | m]) a),
  μ[φ ∘ f | m] a ≤ (φ ∘ μ[f | m]) a
Tactic: filter_upwards [hφ_cvx.neg.map_condExp_le_univ hm hφ_cont.neg hf_int hφ_int.neg,
    condExp_neg (φ ∘ f) m] with a h 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 α
⊢ (ae μ).EventuallyLE (β := ℝ) (fun (x : α) ↦ ‖μ[f | m] x‖) μ[fun (x : α) ↦ ‖f x‖ | m]
have pos : ∀ (hm : ¬m ≤ mα), (ae μ).EventuallyLE (β := ℝ) (fun (x : α) ↦ ‖μ[f | m] x‖) μ[fun (x : α) ↦ ‖f x‖ | m]
Tactic: by_cases! hm : ¬ m ≤ mα
-- 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 α
pos : ∀ (hm : ¬m ≤ mα), (ae μ).EventuallyLE (β := ℝ) (fun (x : α) ↦ ‖μ[f | m] x‖) μ[fun (x : α) ↦ ‖f x‖ | m]
⊢ (ae μ).EventuallyLE (β := ℝ) (fun (x : α) ↦ ‖μ[f | m] x‖) μ[fun (x : α) ↦ ‖f x‖ | m]
have neg : ∀ (hm : m ≤ mα), (ae μ).EventuallyLE (β := ℝ) (fun (x : α) ↦ ‖μ[f | m] x‖) μ[fun (x : α) ↦ ‖f x‖ | m]
Tactic: by_cases! hm : ¬ m ≤ mα
-- 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 α
hm : ¬m ≤ mα
⊢ (ae μ).EventuallyLE (β := ℝ) (fun (x : α) ↦ ‖μ[f | m] x‖) μ[fun (x : α) ↦ ‖f x‖ | m]
have pos : (ae μ).EventuallyLE (β := ℝ) (fun (x : α) ↦ 0) 0
Tactic: simp [condExp_of_not_le hm]
-- 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 α
hm : m ≤ mα
⊢ (ae μ).EventuallyLE (β := ℝ) (fun (x : α) ↦ ‖μ[f | m] x‖) μ[fun (x : α) ↦ ‖f x‖ | m]
have pos : ∀ (hμm : ¬SigmaFinite (μ.trim hm)), (ae μ).EventuallyLE (β := ℝ) (fun (x : α) ↦ ‖μ[f | m] x‖) μ[fun (x : α) ↦ ‖f x‖ | m]
Tactic: by_cases! hμm : ¬ SigmaFinite (μ.trim hm)
-- 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 α
hm : m ≤ mα
pos :
  ∀ (hμm : ¬SigmaFinite (μ.trim hm)),
    (ae μ).EventuallyLE (β := ℝ) (fun (x : α) ↦ ‖μ[f | m] x‖) μ[fun (x : α) ↦ ‖f x‖ | m]
⊢ (ae μ).EventuallyLE (β := ℝ) (fun (x : α) ↦ ‖μ[f | m] x‖) μ[fun (x : α) ↦ ‖f x‖ | m]
have neg : ∀ (hμm : SigmaFinite (μ.trim hm)), (ae μ).EventuallyLE (β := ℝ) (fun (x : α) ↦ ‖μ[f | m] x‖) μ[fun (x : α) ↦ ‖f x‖ | m]
Tactic: by_cases! hμm : ¬ SigmaFinite (μ.trim hm)
-- 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 α
hm : m ≤ mα
hμm : ¬SigmaFinite (μ.trim hm)
⊢ (ae μ).EventuallyLE (β := ℝ) (fun (x : α) ↦ ‖μ[f | m] x‖) μ[fun (x : α) ↦ ‖f x‖ | m]
have pos : (ae μ).EventuallyLE (β := ℝ) (fun (x : α) ↦ 0) 0
Tactic: simp [condExp_of_not_sigmaFinite hm hμm]
-- 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 α
hm : m ≤ mα
hμm : SigmaFinite (μ.trim hm)
⊢ (ae μ).EventuallyLE (β := ℝ) (fun (x : α) ↦ ‖μ[f | m] x‖) μ[fun (x : α) ↦ ‖f x‖ | m]
have pos : ∀ (hf_int : ¬Integrable f μ), (ae μ).EventuallyLE (β := ℝ) (fun (x : α) ↦ ‖μ[f | m] x‖) μ[fun (x : α) ↦ ‖f x‖ | m]
Tactic: by_cases! hf_int : ¬ Integrable f μ
-- 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 α
hm : m ≤ mα
hμm : SigmaFinite (μ.trim hm)
pos : ∀ (hf_int : ¬Integrable f μ), (ae μ).EventuallyLE (β := ℝ) (fun (x : α) ↦ ‖μ[f | m] x‖) μ[fun (x : α) ↦ ‖f x‖ | m]
⊢ (ae μ).EventuallyLE (β := ℝ) (fun (x : α) ↦ ‖μ[f | m] x‖) μ[fun (x : α) ↦ ‖f x‖ | m]
have neg : ∀ (hf_int : Integrable f μ), (ae μ).EventuallyLE (β := ℝ) (fun (x : α) ↦ ‖μ[f | m] x‖) μ[fun (x : α) ↦ ‖f x‖ | m]
Tactic: by_cases! hf_int : ¬ Integrable f μ
-- 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 α
hm : m ≤ mα
hμm : SigmaFinite (μ.trim hm)
hf_int : ¬Integrable f μ
⊢ (ae μ).EventuallyLE (β := ℝ) (fun (x : α) ↦ ‖μ[f | m] x‖) μ[fun (x : α) ↦ ‖f x‖ | m]
have pos : (ae μ).EventuallyLE (β := ℝ) (fun (x : α) ↦ 0) μ[fun (x : α) ↦ ‖f x‖ | m]
Tactic: simp only [condExp_of_not_integrable hf_int, Pi.zero_apply, norm_zero]
-- 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 α
hm : m ≤ mα
hμm : SigmaFinite (μ.trim hm)
hf_int : ¬Integrable f μ
⊢ (ae μ).EventuallyLE (β := ℝ) (fun (x : α) ↦ 0) μ[fun (x : α) ↦ ‖f x‖ | m]
have pos : (ae μ).EventuallyLE (β := ℝ) 0 fun (x : α) ↦ ‖f x‖
Tactic: apply condExp_nonneg
-- 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 α
hm : m ≤ mα
hμm : SigmaFinite (μ.trim hm)
hf_int : ¬Integrable f μ
⊢ (ae μ).EventuallyLE (β := ℝ) 0 fun (x : α) ↦ ‖f x‖
have pos : ∀ (a : α), 0 a ≤ ‖f a‖
Tactic: filter_upwards with a
-- 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 α
inst_3 : FiniteDimensional ℝ E
hm : m ≤ mα
inst_4 : SigmaFinite (μ.trim hm)
hφ_cvx : ConcaveOn ℝ univ φ
hf_int : Integrable f μ
hφ_int : Integrable (φ ∘ f) μ
⊢ μ[φ ∘ f | m] ≤ᶠ[ae μ] φ ∘ μ[f | m]
have h : ∀ (a : α) (h : ((-φ) ∘ μ[f | m]) a ≤ μ[(-φ) ∘ f | m] a) (ha : μ[-φ ∘ f | m] a = (-μ[φ ∘ f | m]) a),
  μ[φ ∘ f | m] a ≤ (φ ∘ μ[f | m]) a
Tactic: filter_upwards [hφ_cvx.neg.map_condExp_le_of_finiteDimensional hm hf_int hφ_int.neg,
    condExp_neg (φ ∘ f) m] with a h ha
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1 (goal)
Goal:
α : Type u_1
G : Type u_4
inst : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst_1 : NormedSpace ℝ G
hm : m ≤ m0
inst_2 : SigmaFinite (μ.trim hm)
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
x : G
⊢ MemLp (↑(↑(condExpIndSMul (s := s) hm hs hμs x) : α →ₘ[μ] G) : α → G) 1 μ
have rw : Integrable (↑(↑(condExpIndSMul (s := s) hm hs hμs x) : α →ₘ[μ] G) : α → G) μ
Tactic: rw [memLp_one_iff_integrable]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1 (goal)
Goal:
α : Type u_1
G : Type u_4
inst : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst_1 : NormedSpace ℝ G
hm : m ≤ m0
inst_2 : SigmaFinite (μ.trim hm)
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
x y : G
⊢ condExpIndL1Fin (s := s) hm hs hμs (x + y) =
    HAdd.hAdd (α := ↥(Lp G 1 μ)) (condExpIndL1Fin (s := s) hm hs hμs x) (condExpIndL1Fin (s := s) hm hs hμs y)
have h : (↑(↑(condExpIndL1Fin (s := s) hm hs hμs (x + y)) : α →ₘ[μ] G) : α → G) =ᶠ[ae μ]
  (↑(↑(HAdd.hAdd (α := ↥(Lp G 1 μ)) (condExpIndL1Fin (s := s) hm hs hμs x) (condExpIndL1Fin (s := s) hm hs hμs y)) :
        α →ₘ[μ] G) :
    α → G)
Tactic: ext1
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1 (goal)
Goal:
α : Type u_1
G : Type u_4
inst : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst_1 : NormedSpace ℝ G
hm : m ≤ m0
inst_2 : SigmaFinite (μ.trim hm)
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
x y : G
⊢ (↑(↑(condExpIndL1Fin (s := s) hm hs hμs (x + y)) : α →ₘ[μ] G) : α → G) =ᶠ[ae μ]
    (↑(↑(HAdd.hAdd (α := ↥(Lp G 1 μ)) (condExpIndL1Fin (s := s) hm hs hμs x) (condExpIndL1Fin (s := s) hm hs hμs y)) :
          α →ₘ[μ] G) :
      α → G)
have h : (↑(↑(MemLp.toLp (↑(↑(condExpIndSMul (s := s) hm hs hμs (x + y)) : α →ₘ[μ] G) : α → G) sorry) : α →ₘ[μ] G) : α → G) =ᶠ[ae μ]
  (↑(↑(MemLp.toLp (↑(↑(condExpIndSMul (s := s) hm hs hμs x) : α →ₘ[μ] G) : α → G) sorry +
            MemLp.toLp (↑(↑(condExpIndSMul (s := s) hm hs hμs y) : α →ₘ[μ] G) : α → G) sorry) :
        α →ₘ[μ] G) :
    α → G)
Tactic: unfold condExpIndL1Fin Integrable.toL1
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1 (goal)
Goal:
α : Type u_1
G : Type u_4
inst : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst_1 : NormedSpace ℝ G
hm : m ≤ m0
inst_2 : SigmaFinite (μ.trim hm)
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
x y : G
⊢ (↑(↑(MemLp.toLp (↑(↑(condExpIndSMul (s := s) hm hs hμs (x + y)) : α →ₘ[μ] G) : α → G) ⋯) : α →ₘ[μ] G) :
      α → G) =ᶠ[ae μ]
    (↑(↑(MemLp.toLp (↑(↑(condExpIndSMul (s := s) hm hs hμs x) : α →ₘ[μ] G) : α → G) ⋯ +
              MemLp.toLp (↑(↑(condExpIndSMul (s := s) hm hs hμs y) : α →ₘ[μ] G) : α → G) ⋯) :
          α →ₘ[μ] G) :
      α → G)
have h : (↑(↑(MemLp.toLp (↑(↑(condExpIndSMul (s := s) hm hs hμs (x + y)) : α →ₘ[μ] G) : α → G) sorry) : α →ₘ[μ] G) : α → G) =ᶠ[ae μ]
  (↑(↑(MemLp.toLp (↑(↑(condExpIndSMul (s := s) hm hs hμs x) : α →ₘ[μ] G) : α → G) sorry) : α →ₘ[μ] G) : α → G) +
    (↑(↑(MemLp.toLp (↑(↑(condExpIndSMul (s := s) hm hs hμs y) : α →ₘ[μ] G) : α → G) sorry) : α →ₘ[μ] G) : α → G)
Tactic: grw [Lp.coeFn_add, MemLp.coeFn_toLp, MemLp.coeFn_toLp, MemLp.coeFn_toLp, condExpIndSMul_add,
    Lp.coeFn_add]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1 (goal)
Goal:
α : Type u_1
G : Type u_4
inst : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst_1 : NormedSpace ℝ G
hm : m ≤ m0
inst_2 : SigmaFinite (μ.trim hm)
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
x y : G
h :
  (↑(↑(MemLp.toLp (↑(↑(condExpIndSMul (s := s) hm hs hμs (x + y)) : α →ₘ[μ] G) : α → G) ⋯) : α →ₘ[μ] G) :
      α → G) =ᶠ[ae μ]
    (↑(↑(MemLp.toLp (↑(↑(condExpIndSMul (s := s) hm hs hμs x) : α →ₘ[μ] G) : α → G) ⋯) : α →ₘ[μ] G) : α → G) +
      (↑(↑(MemLp.toLp (↑(↑(condExpIndSMul (s := s) hm hs hμs y) : α →ₘ[μ] G) : α → G) ⋯) : α →ₘ[μ] G) : α → G)
⊢ (↑(↑(MemLp.toLp (↑(↑(condExpIndSMul (s := s) hm hs hμs (x + y)) : α →ₘ[μ] G) : α → G) ⋯) : α →ₘ[μ] G) :
      α → G) =ᶠ[ae μ]
    (↑(↑(MemLp.toLp (↑(↑(condExpIndSMul (s := s) hm hs hμs x) : α →ₘ[μ] G) : α → G) ⋯ +
              MemLp.toLp (↑(↑(condExpIndSMul (s := s) hm hs hμs y) : α →ₘ[μ] G) : α → G) ⋯) :
          α →ₘ[μ] G) :
      α → G)
have h₁ : (↑(↑(condExpIndSMul (s := s) hm hs hμs (x + y)) : α →ₘ[μ] G) : α → G) =ᶠ[ae μ]
  (↑(↑(MemLp.toLp (↑(↑(condExpIndSMul (s := s) hm hs hμs x) : α →ₘ[μ] G) : α → G) sorry) : α →ₘ[μ] G) : α → G) +
    (↑(↑(MemLp.toLp (↑(↑(condExpIndSMul (s := s) hm hs hμs y) : α →ₘ[μ] G) : α → G) sorry) : α →ₘ[μ] G) : α → G)
Tactic: grw [Lp.coeFn_add, MemLp.coeFn_toLp, MemLp.coeFn_toLp, MemLp.coeFn_toLp, condExpIndSMul_add,
    Lp.coeFn_add]