awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_7
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
f : α → E
fmeas : Measurable f
hf : Integrable f μ
inst_3 : SeparableSpace.{u_7} (↑(range f ∪ {0}) : Type u_7)
⊢ Tendsto (β := ℝ)
    (fun (n : ℕ) ↦
      ∫ (x : α), ‖HSub.hSub (α := E) ((approxOn f fmeas (range f ∪ {0}) 0 ⋯ n : (a : α) → E) x : E) (f x)‖ ∂μ)
    atTop (𝓝 0)
have h : ∀ (n : ℕ),
  ∫ (x : α), ‖HSub.hSub (α := E) ((approxOn f fmeas (range f ∪ {0}) 0 sorry n : (a : α) → E) x : E) (f x)‖ ∂μ =
    (ENNReal.toReal ∘ fun (n : ℕ) ↦
        ∫⁻ (x : α), ‖HSub.hSub (α := E) ((approxOn f fmeas (range f ∪ {0}) 0 sorry n : (a : α) → E) x : E) (f x)‖ₑ ∂μ)
      n
Tactic: convert! (tendsto_toReal zero_ne_top).comp (tendsto_approxOn_range_L1_enorm fmeas hf) with n
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_7
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
f : α → E
fmeas : Measurable f
hf : Integrable f μ
inst_3 : SeparableSpace.{u_7} (↑(range f ∪ {0}) : Type u_7)
n : ℕ
⊢ ∫ (x : α), ‖HSub.hSub (α := E) ((approxOn f fmeas (range f ∪ {0}) 0 ⋯ n : (a : α) → E) x : E) (f x)‖ ∂μ =
    (ENNReal.toReal ∘ fun (n : ℕ) ↦
        ∫⁻ (x : α), ‖HSub.hSub (α := E) ((approxOn f fmeas (range f ∪ {0}) 0 ⋯ n : (a : α) → E) x : E) (f x)‖ₑ ∂μ)
      n
have h : (∫⁻ (x : α), ‖HSub.hSub (α := E) ((approxOn f fmeas (range f ∪ {0}) 0 sorry n : (a : α) → E) x : E) (f x)‖ₑ ∂μ).toReal =
  (ENNReal.toReal ∘ fun (n : ℕ) ↦
      ∫⁻ (x : α), ‖HSub.hSub (α := E) ((approxOn f fmeas (range f ∪ {0}) 0 sorry n : (a : α) → E) x : E) (f x)‖ₑ ∂μ)
    n
Tactic: rw [integral_norm_eq_lintegral_enorm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_7
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
f : α → E
fmeas : Measurable f
hf : Integrable f μ
inst_3 : SeparableSpace.{u_7} (↑(range f ∪ {0}) : Type u_7)
n : ℕ
h :
  (∫⁻ (x : α), ‖HSub.hSub (α := E) ((approxOn f fmeas (range f ∪ {0}) 0 ⋯ n : (a : α) → E) x : E) (f x)‖ₑ ∂μ).toReal =
    (ENNReal.toReal ∘ fun (n : ℕ) ↦
        ∫⁻ (x : α), ‖HSub.hSub (α := E) ((approxOn f fmeas (range f ∪ {0}) 0 ⋯ n : (a : α) → E) x : E) (f x)‖ₑ ∂μ)
      n
⊢ ∫ (x : α), ‖HSub.hSub (α := E) ((approxOn f fmeas (range f ∪ {0}) 0 ⋯ n : (a : α) → E) x : E) (f x)‖ ∂μ =
    (ENNReal.toReal ∘ fun (n : ℕ) ↦
        ∫⁻ (x : α), ‖HSub.hSub (α := E) ((approxOn f fmeas (range f ∪ {0}) 0 ⋯ n : (a : α) → E) x : E) (f x)‖ₑ ∂μ)
      n
have h₁ : AEStronglyMeasurable.{u_1, u_7} (β := E)
  (fun (x : α) ↦ HSub.hSub (α := E) ((approxOn f fmeas (range f ∪ {0}) 0 sorry n : (a : α) → E) x : E) (f x)) μ
Tactic: rw [integral_norm_eq_lintegral_enorm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_7
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
f : α → E
fmeas : Measurable f
hf : Integrable f μ
inst_3 : SeparableSpace.{u_7} (↑(range f ∪ {0}) : Type u_7)
n : ℕ
⊢ AEStronglyMeasurable.{u_1, u_7} (β := E)
    (fun (x : α) ↦ HSub.hSub (α := E) ((approxOn f fmeas (range f ∪ {0}) 0 ⋯ n : (a : α) → E) x : E) (f x)) μ
have h : AEStronglyMeasurable f μ
Tactic: apply (SimpleFunc.aestronglyMeasurable _).sub
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_7
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
f : α → E
fmeas : Measurable f
hf : Integrable f μ
inst_3 : SeparableSpace.{u_7} (↑(range f ∪ {0}) : Type u_7)
n : ℕ
⊢ AEStronglyMeasurable f μ
have apply : IsSeparable (range f)
Tactic: apply (stronglyMeasurable_iff_measurable_separable.2 ⟨fmeas, ?_⟩).aestronglyMeasurable
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
⊢ ∫ (a : α), f a ∂μ = HSub.hSub (α := ℝ) (∫ (a : α), (↑(f a).toNNReal : ℝ) ∂μ) (∫ (a : α), (↑(-f a).toNNReal : ℝ) ∂μ)
have rw : Eq (α := ℝ) (∫ (a : α), f a ∂μ) (∫ (a : α), (↑(f a).toNNReal : ℝ) - (↑(-f a).toNNReal : ℝ) ∂μ)
Tactic: rw [← integral_sub hf.real_toNNReal]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
rw : Eq (α := ℝ) (∫ (a : α), f a ∂μ) (∫ (a : α), (↑(f a).toNNReal : ℝ) - (↑(-f a).toNNReal : ℝ) ∂μ)
⊢ ∫ (a : α), f a ∂μ = HSub.hSub (α := ℝ) (∫ (a : α), (↑(f a).toNNReal : ℝ) ∂μ) (∫ (a : α), (↑(-f a).toNNReal : ℝ) ∂μ)
have rw₁ : Integrable (ε := ℝ) (fun (a : α) ↦ (↑(-f a).toNNReal : ℝ)) μ
Tactic: rw [← integral_sub hf.real_toNNReal]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
inst_2 : PartialOrder E
inst_3 : IsOrderedAddMonoid E
inst_4 : IsOrderedModule ℝ E
inst_5 : OrderClosedTopology E
f : α → E
ν : Measure α
hle : μ ≤ ν
hf : 0 ≤ᶠ[ae ν] f
hfi : Integrable f ν
⊢ LE.le.{u_2} (α := E) (∫ (a : α), f a ∂μ) (∫ (a : α), f a ∂ν)
have pos : ∀ (hE : CompleteSpace E), LE.le.{u_2} (α := E) (∫ (a : α), f a ∂μ) (∫ (a : α), f a ∂ν)
Tactic: by_cases hE : CompleteSpace E
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
inst_2 : PartialOrder E
inst_3 : IsOrderedAddMonoid E
inst_4 : IsOrderedModule ℝ E
inst_5 : OrderClosedTopology E
f : α → E
ν : Measure α
hle : μ ≤ ν
hf : 0 ≤ᶠ[ae ν] f
hfi : Integrable f ν
pos : ∀ (hE : CompleteSpace E), LE.le.{u_2} (α := E) (∫ (a : α), f a ∂μ) (∫ (a : α), f a ∂ν)
⊢ LE.le.{u_2} (α := E) (∫ (a : α), f a ∂μ) (∫ (a : α), f a ∂ν)
have neg : ∀ (hE : ¬CompleteSpace E), LE.le.{u_2} (α := E) (∫ (a : α), f a ∂μ) (∫ (a : α), f a ∂ν)
Tactic: by_cases hE : CompleteSpace E
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (hypothesis)
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
inst_2 : PartialOrder E
inst_3 : IsOrderedAddMonoid E
inst_4 : IsOrderedModule ℝ E
inst_5 : OrderClosedTopology E
f : α → E
ν : Measure α
hle : μ ≤ ν
hf : 0 ≤ᶠ[ae ν] f
hfi : Integrable f ν
hE : CompleteSpace E
⊢ LE.le.{u_2} (α := E) (∫ (a : α), f a ∂μ) (∫ (a : α), f a ∂ν)
have this : let this := borel E;
BorelSpace E
Tactic: borelize E
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
inst_2 : PartialOrder E
inst_3 : IsOrderedAddMonoid E
inst_4 : IsOrderedModule ℝ E
inst_5 : OrderClosedTopology E
f : α → E
ν : Measure α
hle : μ ≤ ν
hf : 0 ≤ᶠ[ae ν] f
hfi : Integrable f ν
hE : CompleteSpace E
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
⊢ LE.le.{u_2} (α := E) (∫ (a : α), f a ∂μ) (∫ (a : α), f a ∂ν)
have pos : ∀ (g : α → E) (hg : StronglyMeasurable g) (hg_nonneg : ∀ (x : α), Membership.mem (γ := Set E) (Ici 0) (g x))
  (hfg : f =ᶠ[ae ν] g), LE.le.{u_2} (α := E) (∫ (a : α), f a ∂μ) (∫ (a : α), f a ∂ν)
Tactic: obtain ⟨g, hg, hg_nonneg, hfg⟩ := hfi.1.exists_stronglyMeasurable_range_subset
    isClosed_Ici.measurableSet (Set.nonempty_Ici (a := 0)) hf
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (hypothesis)
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
inst_2 : PartialOrder E
inst_3 : IsOrderedAddMonoid E
inst_4 : IsOrderedModule ℝ E
inst_5 : OrderClosedTopology E
f : α → E
ν : Measure α
hle : μ ≤ ν
hf : 0 ≤ᶠ[ae ν] f
hfi : Integrable f ν
hE : CompleteSpace E
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
g : α → E
hg : StronglyMeasurable g
hg_nonneg : ∀ (x : α), Membership.mem (γ := Set E) (Ici 0) (g x)
hfg : f =ᶠ[ae ν] g
⊢ LE.le.{u_2} (α := E) (∫ (a : α), f a ∂μ) (∫ (a : α), f a ∂ν)
have hfi₁ : Integrable g ν
Tactic: rw [integrable_congr hfg] at hfi
Cleared hypotheses: hfi, hg, hg_nonneg, hfg
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
inst_2 : PartialOrder E
inst_3 : IsOrderedAddMonoid E
inst_4 : IsOrderedModule ℝ E
inst_5 : OrderClosedTopology E
f : α → E
ν : Measure α
hle : μ ≤ ν
hf : 0 ≤ᶠ[ae ν] f
hE : CompleteSpace E
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
g : α → E
hfi : Integrable g ν
hg : StronglyMeasurable g
hg_nonneg : ∀ (x : α), Membership.mem (γ := Set E) (Ici 0) (g x)
hfg : f =ᶠ[ae ν] g
⊢ LE.le.{u_2} (α := E) (∫ (a : α), f a ∂μ) (∫ (a : α), f a ∂ν)
have pos : LE.le.{u_2} (α := E) (∫ (a : α), g a ∂μ) (∫ (a : α), g a ∂ν)
Tactic: simp only [integral_congr_ae hfg, integral_congr_ae (ae_mono hle hfg)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (hypothesis)
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
inst_2 : PartialOrder E
inst_3 : IsOrderedAddMonoid E
inst_4 : IsOrderedModule ℝ E
inst_5 : OrderClosedTopology E
f : α → E
ν : Measure α
hle : μ ≤ ν
hf : 0 ≤ᶠ[ae ν] f
hE : CompleteSpace E
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
g : α → E
hfi : Integrable g ν
hg : StronglyMeasurable g
hg_nonneg : ∀ (x : α), Membership.mem (γ := Set E) (Ici 0) (g x)
hfg : f =ᶠ[ae ν] g
⊢ LE.le.{u_2} (α := E) (∫ (a : α), g a ∂μ) (∫ (a : α), g a ∂ν)
have x : SeparableSpace.{u_2} (↑(range g ∪ {0}) : Type u_2)
Tactic: have _ := hg.separableSpace_range_union_singleton (b := 0)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (hypothesis)
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
inst_2 : PartialOrder E
inst_3 : IsOrderedAddMonoid E
inst_4 : IsOrderedModule ℝ E
inst_5 : OrderClosedTopology E
f : α → E
ν : Measure α
hle : μ ≤ ν
hf : 0 ≤ᶠ[ae ν] f
hE : CompleteSpace E
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
g : α → E
hfi : Integrable g ν
hg : StronglyMeasurable g
hg_nonneg : ∀ (x : α), Membership.mem (γ := Set E) (Ici 0) (g x)
hfg : f =ᶠ[ae ν] g
h : SeparableSpace.{u_2} (↑(range g ∪ {0}) : Type u_2)
⊢ LE.le.{u_2} (α := E) (∫ (a : α), g a ∂μ) (∫ (a : α), g a ∂ν)
have h₁ : Tendsto.{0, u_2} (β := E) (fun (n : ℕ) ↦ SimpleFunc.integral ν (approxOn g sorry (range g ∪ {0}) 0 sorry n)) atTop
  (𝓝 (∫ (x : α), g x ∂ν))
Tactic: have h₁ := tendsto_integral_approxOn_of_measurable_of_range_subset hg.measurable hfi _ le_rfl
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (hypothesis)
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
inst_2 : PartialOrder E
inst_3 : IsOrderedAddMonoid E
inst_4 : IsOrderedModule ℝ E
inst_5 : OrderClosedTopology E
f : α → E
ν : Measure α
hle : μ ≤ ν
hf : 0 ≤ᶠ[ae ν] f
hE : CompleteSpace E
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
g : α → E
hfi : Integrable g ν
hg : StronglyMeasurable g
hg_nonneg : ∀ (x : α), Membership.mem (γ := Set E) (Ici 0) (g x)
hfg : f =ᶠ[ae ν] g
h : SeparableSpace.{u_2} (↑(range g ∪ {0}) : Type u_2)
h₁ :
  Tendsto.{0, u_2} (β := E) (fun (n : ℕ) ↦ SimpleFunc.integral ν (approxOn g ⋯ (range g ∪ {0}) 0 ⋯ n)) atTop
    (𝓝 (∫ (x : α), g x ∂ν))
⊢ LE.le.{u_2} (α := E) (∫ (a : α), g a ∂μ) (∫ (a : α), g a ∂ν)
have h₂ : Tendsto.{0, u_2} (β := E) (fun (n : ℕ) ↦ SimpleFunc.integral μ (approxOn g sorry (range g ∪ {0}) 0 sorry n)) atTop
  (𝓝 (∫ (x : α), g x ∂μ))
Tactic: have h₂ := tendsto_integral_approxOn_of_measurable_of_range_subset hg.measurable
    (hfi.mono_measure hle) _ le_rfl
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
inst_2 : PartialOrder E
inst_3 : IsOrderedAddMonoid E
inst_4 : IsOrderedModule ℝ E
inst_5 : OrderClosedTopology E
f : α → E
ν : Measure α
hle : μ ≤ ν
hf : 0 ≤ᶠ[ae ν] f
hE : CompleteSpace E
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
g : α → E
hfi : Integrable g ν
hg : StronglyMeasurable g
hg_nonneg : ∀ (x : α), Membership.mem (γ := Set E) (Ici 0) (g x)
hfg : f =ᶠ[ae ν] g
h : SeparableSpace.{u_2} (↑(range g ∪ {0}) : Type u_2)
h₁ :
  Tendsto.{0, u_2} (β := E) (fun (n : ℕ) ↦ SimpleFunc.integral ν (approxOn g ⋯ (range g ∪ {0}) 0 ⋯ n)) atTop
    (𝓝 (∫ (x : α), g x ∂ν))
h₂ :
  Tendsto.{0, u_2} (β := E) (fun (n : ℕ) ↦ SimpleFunc.integral μ (approxOn g ⋯ (range g ∪ {0}) 0 ⋯ n)) atTop
    (𝓝 (∫ (x : α), g x ∂μ))
⊢ LE.le.{u_2} (α := E) (∫ (a : α), g a ∂μ) (∫ (a : α), g a ∂ν)
have pos : ∀ (x : ℕ),
  SimpleFunc.integral μ (approxOn g sorry (range g ∪ {0}) 0 sorry x) ≤
    SimpleFunc.integral ν (approxOn g sorry (range g ∪ {0}) 0 sorry x)
Tactic: apply le_of_tendsto_of_tendsto' h₂ h₁
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
inst_2 : PartialOrder E
inst_3 : IsOrderedAddMonoid E
inst_4 : IsOrderedModule ℝ E
inst_5 : ClosedIciTopology E
f : α → E
hf : f ≤ᶠ[ae μ] 0
⊢ LE.le.{u_2} (α := E) (∫ (x : α), f x ∂μ) 0
have rw : LE.le.{u_2} (α := E) 0 (∫ (a : α), -f a ∂μ)
Tactic: rw [← neg_nonneg, ← integral_neg]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
inst_2 : PartialOrder E
inst_3 : IsOrderedAddMonoid E
inst_4 : IsOrderedModule ℝ E
inst_5 : ClosedIciTopology E
f : α → E
hf : f ≤ᶠ[ae μ] 0
⊢ LE.le.{u_2} (α := E) 0 (∫ (a : α), -f a ∂μ)
have refine : EventuallyLE.{u_1, u_2} (β := E) (ae μ) 0 fun (a : α) ↦ -f a
Tactic: refine integral_nonneg_of_ae ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
inst_2 : PartialOrder E
inst_3 : IsOrderedAddMonoid E
inst_4 : IsOrderedModule ℝ E
inst_5 : ClosedIciTopology E
f : α → E
hf : f ≤ᶠ[ae μ] 0
⊢ EventuallyLE.{u_1, u_2} (β := E) (ae μ) 0 fun (a : α) ↦ -f a
have h : ∀ (x : α) (hx : f x ≤ 0 x), 0 x ≤ -f x
Tactic: filter_upwards [hf] with x hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
inst_2 : PartialOrder E
inst_3 : IsOrderedAddMonoid E
inst_4 : IsOrderedModule ℝ E
inst_5 : ClosedIciTopology E
f g : α → E
hf : Integrable f μ
hg : Integrable g μ
h : f ≤ᶠ[ae μ] g
⊢ LE.le.{u_2} (α := E) (∫ (x : α), f x ∂μ) (∫ (x : α), g x ∂μ)
have rw : LE.le.{u_2} (α := E) 0 (∫ (a : α), g a - f a ∂μ)
Tactic: rw [← sub_nonneg, ← integral_sub hg hf]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
inst_2 : PartialOrder E
inst_3 : IsOrderedAddMonoid E
inst_4 : IsOrderedModule ℝ E
inst_5 : ClosedIciTopology E
f g : α → E
hf : Integrable f μ
hg : Integrable g μ
h : f ≤ᶠ[ae μ] g
⊢ LE.le.{u_2} (α := E) 0 (∫ (a : α), g a - f a ∂μ)
have refine : EventuallyLE.{u_1, u_2} (β := E) (ae μ) 0 fun (a : α) ↦ g a - f a
Tactic: refine integral_nonneg_of_ae ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
inst_2 : PartialOrder E
inst_3 : IsOrderedAddMonoid E
inst_4 : IsOrderedModule ℝ E
inst_5 : ClosedIciTopology E
f g : α → E
hf : Integrable f μ
hg : Integrable g μ
h : f ≤ᶠ[ae μ] g
⊢ EventuallyLE.{u_1, u_2} (β := E) (ae μ) 0 fun (a : α) ↦ g a - f a
have h₁ : ∀ (x : α) (hx : f x ≤ g x), 0 x ≤ g x - f x
Tactic: filter_upwards [h] with x hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
inst_2 : PartialOrder E
inst_3 : IsOrderedAddMonoid E
inst_4 : IsOrderedModule ℝ E
inst_5 : ClosedIciTopology E
f g : α → E
hf : 0 ≤ᶠ[ae μ] f
hgi : Integrable g μ
h : f ≤ᶠ[ae μ] g
⊢ LE.le.{u_2} (α := E) (∫ (a : α), f a ∂μ) (∫ (a : α), g a ∂μ)
have pos : ∀ (hfi : Integrable f μ), LE.le.{u_2} (α := E) (∫ (a : α), f a ∂μ) (∫ (a : α), g a ∂μ)
Tactic: by_cases hfi : Integrable f μ
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
inst_2 : PartialOrder E
inst_3 : IsOrderedAddMonoid E
inst_4 : IsOrderedModule ℝ E
inst_5 : ClosedIciTopology E
f g : α → E
hf : 0 ≤ᶠ[ae μ] f
hgi : Integrable g μ
h : f ≤ᶠ[ae μ] g
pos : ∀ (hfi : Integrable f μ), LE.le.{u_2} (α := E) (∫ (a : α), f a ∂μ) (∫ (a : α), g a ∂μ)
⊢ LE.le.{u_2} (α := E) (∫ (a : α), f a ∂μ) (∫ (a : α), g a ∂μ)
have neg : ∀ (hfi : ¬Integrable f μ), LE.le.{u_2} (α := E) (∫ (a : α), f a ∂μ) (∫ (a : α), g a ∂μ)
Tactic: by_cases hfi : Integrable f μ
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
inst_2 : PartialOrder E
inst_3 : IsOrderedAddMonoid E
inst_4 : IsOrderedModule ℝ E
inst_5 : ClosedIciTopology E
β : Type u_6
inst_6 : Preorder β
f : α → β → E
s : Set β
hf_mono : ∀ᵐ (x : α) ∂μ, MonotoneOn (f x) s
hf_int : ∀ a ∈ s, Integrable.{u_2, u_1} (ε := E) (fun (x : α) ↦ f x a) μ
a : β
ha : a ∈ s
b : β
hb : b ∈ s
hab : a ≤ b
⊢ LE.le.{u_2} (α := E) ((fun (b : β) ↦ (∫ (x : α), f x b ∂μ : E)) a) ((fun (b : β) ↦ (∫ (x : α), f x b ∂μ : E)) b)
have refine : EventuallyLE.{u_1, u_2} (β := E) (ae μ) (fun (x : α) ↦ f x a) fun (x : α) ↦ f x b
Tactic: refine integral_mono_ae (hf_int a ha) (hf_int b hb) ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
inst_2 : PartialOrder E
inst_3 : IsOrderedAddMonoid E
inst_4 : IsOrderedModule ℝ E
inst_5 : ClosedIciTopology E
β : Type u_6
inst_6 : Preorder β
f : α → β → E
s : Set β
hf_mono : ∀ᵐ (x : α) ∂μ, MonotoneOn (f x) s
hf_int : ∀ a ∈ s, Integrable.{u_2, u_1} (ε := E) (fun (x : α) ↦ f x a) μ
a : β
ha : a ∈ s
b : β
hb : b ∈ s
hab : a ≤ b
⊢ EventuallyLE.{u_1, u_2} (β := E) (ae μ) (fun (x : α) ↦ f x a) fun (x : α) ↦ f x b
have h : ∀ (x : α) (hx : MonotoneOn (f x) s), f x a ≤ f x b
Tactic: filter_upwards [hf_mono] with x hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
inst_2 : PartialOrder E
inst_3 : IsOrderedAddMonoid E
inst_4 : IsOrderedModule ℝ E
inst_5 : ClosedIciTopology E
β : Type u_6
inst_6 : Preorder β
f : α → β → E
s : Set β
hf_anti : ∀ᵐ (x : α) ∂μ, AntitoneOn (f x) s
hf_int : ∀ a ∈ s, Integrable.{u_2, u_1} (ε := E) (fun (x : α) ↦ f x a) μ
a : β
ha : a ∈ s
b : β
hb : b ∈ s
hab : a ≤ b
⊢ LE.le.{u_2} (α := E) ((fun (b : β) ↦ (∫ (x : α), f x b ∂μ : E)) b) ((fun (b : β) ↦ (∫ (x : α), f x b ∂μ : E)) a)
have refine : EventuallyLE.{u_1, u_2} (β := E) (ae μ) (fun (x : α) ↦ f x b) fun (x : α) ↦ f x a
Tactic: refine integral_mono_ae (hf_int b hb) (hf_int a ha) ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
inst_2 : PartialOrder E
inst_3 : IsOrderedAddMonoid E
inst_4 : IsOrderedModule ℝ E
inst_5 : ClosedIciTopology E
β : Type u_6
inst_6 : Preorder β
f : α → β → E
s : Set β
hf_anti : ∀ᵐ (x : α) ∂μ, AntitoneOn (f x) s
hf_int : ∀ a ∈ s, Integrable.{u_2, u_1} (ε := E) (fun (x : α) ↦ f x a) μ
a : β
ha : a ∈ s
b : β
hb : b ∈ s
hab : a ≤ b
⊢ EventuallyLE.{u_1, u_2} (β := E) (ae μ) (fun (x : α) ↦ f x b) fun (x : α) ↦ f x a
have h : ∀ (x : α) (hx : AntitoneOn (f x) s), f x b ≤ f x a
Tactic: filter_upwards [hf_anti] with x hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
inst_2 : PartialOrder E
inst_3 : IsOrderedAddMonoid E
inst_4 : IsOrderedModule ℝ E
inst_5 : ClosedIciTopology E
β : Type u_6
inst_6 : AddCommMonoid β
inst_7 : Module ℝ β
f : α → β → E
s : Set β
hs : Convex ℝ s
hf_conv : ∀ᵐ (x : α) ∂μ, ConvexOn ℝ s (f x)
hf_int : ∀ a ∈ s, Integrable.{u_2, u_1} (ε := E) (fun (x : α) ↦ f x a) μ
⊢ ConvexOn.{0, u_6, u_2} ℝ (β := E) s fun (b : β) ↦ ∫ (x : α), f x b ∂μ
have refine : ∀ ⦃x : β⦄,
  x ∈ s →
    ∀ ⦃y : β⦄,
      y ∈ s →
        ∀ ⦃a b : ℝ⦄,
          0 ≤ a →
            0 ≤ b →
              a + b = 1 →
                (fun (b : β) ↦ (∫ (x : α), f x b ∂μ : E)) (a • x + b • y) ≤
                  HSMul.hSMul (β := E) a ((fun (b : β) ↦ (∫ (x : α), f x b ∂μ : E)) x) +
                    HSMul.hSMul (β := E) b ((fun (b : β) ↦ (∫ (x : α), f x b ∂μ : E)) y)
Tactic: refine ⟨hs, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
inst_2 : PartialOrder E
inst_3 : IsOrderedAddMonoid E
inst_4 : IsOrderedModule ℝ E
inst_5 : ClosedIciTopology E
β : Type u_6
inst_6 : AddCommMonoid β
inst_7 : Module ℝ β
f : α → β → E
s : Set β
hs : Convex ℝ s
hf_conv : ∀ᵐ (x : α) ∂μ, ConvexOn ℝ s (f x)
hf_int : ∀ a ∈ s, Integrable.{u_2, u_1} (ε := E) (fun (x : α) ↦ f x a) μ
a : β
ha : a ∈ s
b : β
hb : b ∈ s
p q : ℝ
hp : 0 ≤ p
hq : 0 ≤ q
hpq : p + q = 1
⊢ LE.le.{u_2} (α := E) (∫ (x : α), f x (p • a + q • b) ∂μ) (∫ (x : α), p • f x a + q • f x b ∂μ)
have refine : Integrable.{u_2, u_1} (ε := E) (fun (x : α) ↦ f x (p • a + q • b)) μ
Tactic: refine integral_mono_ae ?lhs ?rhs ?ae_le
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
inst_2 : PartialOrder E
inst_3 : IsOrderedAddMonoid E
inst_4 : IsOrderedModule ℝ E
inst_5 : ClosedIciTopology E
β : Type u_6
inst_6 : AddCommMonoid β
inst_7 : Module ℝ β
f : α → β → E
s : Set β
hs : Convex ℝ s
hf_conv : ∀ᵐ (x : α) ∂μ, ConvexOn ℝ s (f x)
hf_int : ∀ a ∈ s, Integrable.{u_2, u_1} (ε := E) (fun (x : α) ↦ f x a) μ
a : β
ha : a ∈ s
b : β
hb : b ∈ s
p q : ℝ
hp : 0 ≤ p
hq : 0 ≤ q
hpq : p + q = 1
refine : Integrable.{u_2, u_1} (ε := E) (fun (x : α) ↦ f x (p • a + q • b)) μ
⊢ LE.le.{u_2} (α := E) (∫ (x : α), f x (p • a + q • b) ∂μ) (∫ (x : α), p • f x a + q • f x b ∂μ)
have refine₁ : Integrable.{u_2, u_1} (ε := E) (fun (x : α) ↦ p • f x a + q • f x b) μ
Tactic: refine integral_mono_ae ?lhs ?rhs ?ae_le