awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus (goal)
Goal:
ι : Type u_1
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
c : E
l l' : Filter ℝ
lt : Filter ι
μ : Measure ℝ
u v : ι → ℝ
inst_2 : l'.IsMeasurablyGenerated
inst_3 : TendstoIxxClass Ioc l l'
hfm : StronglyMeasurableAtFilter f l' μ
hf : Tendsto f (l' ⊓ ae μ) (𝓝 c)
hl : μ.FiniteAtFilter l'
hu : Tendsto u lt l
hv : Tendsto v lt l
⊢ IsLittleO.{u_1, u_3, 0} (E := E) (F := ℝ) lt
    (fun (t : ι) ↦ HSub.hSub (α := E) (∫ (x : ℝ) in u t..v t, f x ∂μ) (∫ (x : ℝ) in u t..v t, c ∂μ)) fun (t : ι) ↦
    ∫ (x : ℝ) in u t..v t, 1 ∂μ
have pos : ∀ (hE : CompleteSpace E),
  IsLittleO.{u_1, u_3, 0} (E := E) (F := ℝ) lt
    (fun (t : ι) ↦ HSub.hSub (α := E) (∫ (x : ℝ) in u t..v t, f x ∂μ) (∫ (x : ℝ) in u t..v t, c ∂μ)) fun (t : ι) ↦
    ∫ (x : ℝ) in u t..v t, 1 ∂μ
Tactic: by_cases hE : CompleteSpace E
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus (goal)
Goal:
ι : Type u_1
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
c : E
l l' : Filter ℝ
lt : Filter ι
μ : Measure ℝ
u v : ι → ℝ
inst_2 : l'.IsMeasurablyGenerated
inst_3 : TendstoIxxClass Ioc l l'
hfm : StronglyMeasurableAtFilter f l' μ
hf : Tendsto f (l' ⊓ ae μ) (𝓝 c)
hl : μ.FiniteAtFilter l'
hu : Tendsto u lt l
hv : Tendsto v lt l
pos :
  ∀ (hE : CompleteSpace E),
    IsLittleO.{u_1, u_3, 0} (E := E) (F := ℝ) lt
      (fun (t : ι) ↦ HSub.hSub (α := E) (∫ (x : ℝ) in u t..v t, f x ∂μ) (∫ (x : ℝ) in u t..v t, c ∂μ)) fun (t : ι) ↦
      ∫ (x : ℝ) in u t..v t, 1 ∂μ
⊢ IsLittleO.{u_1, u_3, 0} (E := E) (F := ℝ) lt
    (fun (t : ι) ↦ HSub.hSub (α := E) (∫ (x : ℝ) in u t..v t, f x ∂μ) (∫ (x : ℝ) in u t..v t, c ∂μ)) fun (t : ι) ↦
    ∫ (x : ℝ) in u t..v t, 1 ∂μ
have neg : ∀ (hE : ¬CompleteSpace E),
  IsLittleO.{u_1, u_3, 0} (E := E) (F := ℝ) lt
    (fun (t : ι) ↦ HSub.hSub (α := E) (∫ (x : ℝ) in u t..v t, f x ∂μ) (∫ (x : ℝ) in u t..v t, c ∂μ)) fun (t : ι) ↦
    ∫ (x : ℝ) in u t..v t, 1 ∂μ
Tactic: by_cases hE : CompleteSpace E
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus (hypothesis)
Goal:
ι : Type u_1
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
c : E
l l' : Filter ℝ
lt : Filter ι
μ : Measure ℝ
u v : ι → ℝ
inst_2 : l'.IsMeasurablyGenerated
inst_3 : TendstoIxxClass Ioc l l'
hfm : StronglyMeasurableAtFilter f l' μ
hf : Tendsto f (l' ⊓ ae μ) (𝓝 c)
hl : μ.FiniteAtFilter l'
hu : Tendsto u lt l
hv : Tendsto v lt l
hE : CompleteSpace E
⊢ IsLittleO.{u_1, u_3, 0} (E := E) (F := ℝ) lt
    (fun (t : ι) ↦ HSub.hSub (α := E) (∫ (x : ℝ) in u t..v t, f x ∂μ) (∫ (x : ℝ) in u t..v t, c ∂μ)) fun (t : ι) ↦
    ∫ (x : ℝ) in u t..v t, 1 ∂μ
have A : IsLittleO.{u_1, u_3, 0} (E := E) (F := ℝ) lt
  (fun (i : ι) ↦ ∫ (x : ℝ) in Ioc (u i) (v i), f x ∂μ - μ.real (Ioc (u i) (v i)) • c) fun (i : ι) ↦
  μ.real (Ioc (u i) (v i))
Tactic: have A := hf.integral_sub_linear_isLittleO_ae hfm hl (hu.Ioc hv)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus (hypothesis)
Goal:
ι : Type u_1
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
c : E
l l' : Filter ℝ
lt : Filter ι
μ : Measure ℝ
u v : ι → ℝ
inst_2 : l'.IsMeasurablyGenerated
inst_3 : TendstoIxxClass Ioc l l'
hfm : StronglyMeasurableAtFilter f l' μ
hf : Tendsto f (l' ⊓ ae μ) (𝓝 c)
hl : μ.FiniteAtFilter l'
hu : Tendsto u lt l
hv : Tendsto v lt l
hE : CompleteSpace E
A :
  IsLittleO.{u_1, u_3, 0} (E := E) (F := ℝ) lt
    (fun (i : ι) ↦ ∫ (x : ℝ) in Ioc (u i) (v i), f x ∂μ - μ.real (Ioc (u i) (v i)) • c) fun (i : ι) ↦
    μ.real (Ioc (u i) (v i))
⊢ IsLittleO.{u_1, u_3, 0} (E := E) (F := ℝ) lt
    (fun (t : ι) ↦ HSub.hSub (α := E) (∫ (x : ℝ) in u t..v t, f x ∂μ) (∫ (x : ℝ) in u t..v t, c ∂μ)) fun (t : ι) ↦
    ∫ (x : ℝ) in u t..v t, 1 ∂μ
have B : IsLittleO.{u_1, u_3, 0} (E := E) (F := ℝ) lt
  (fun (i : ι) ↦ ∫ (x : ℝ) in Ioc (v i) (u i), f x ∂μ - μ.real (Ioc (v i) (u i)) • c) fun (i : ι) ↦
  μ.real (Ioc (v i) (u i))
Tactic: have B := hf.integral_sub_linear_isLittleO_ae hfm hl (hv.Ioc hu)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus (goal)
Goal:
ι : Type u_1
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
c : E
l l' : Filter ℝ
lt : Filter ι
μ : Measure ℝ
u v : ι → ℝ
inst_2 : l'.IsMeasurablyGenerated
inst_3 : TendstoIxxClass Ioc l l'
hfm : StronglyMeasurableAtFilter f l' μ
hf : Tendsto f (l' ⊓ ae μ) (𝓝 c)
hl : μ.FiniteAtFilter l'
hu : Tendsto u lt l
hv : Tendsto v lt l
hE : CompleteSpace E
A :
  IsLittleO.{u_1, u_3, 0} (E := E) (F := ℝ) lt
    (fun (i : ι) ↦ ∫ (x : ℝ) in Ioc (u i) (v i), f x ∂μ - μ.real (Ioc (u i) (v i)) • c) fun (i : ι) ↦
    μ.real (Ioc (u i) (v i))
B :
  IsLittleO.{u_1, u_3, 0} (E := E) (F := ℝ) lt
    (fun (i : ι) ↦ ∫ (x : ℝ) in Ioc (v i) (u i), f x ∂μ - μ.real (Ioc (v i) (u i)) • c) fun (i : ι) ↦
    μ.real (Ioc (v i) (u i))
⊢ IsLittleO.{u_1, u_3, 0} (E := E) (F := ℝ) lt
    (fun (t : ι) ↦ HSub.hSub (α := E) (∫ (x : ℝ) in u t..v t, f x ∂μ) (∫ (x : ℝ) in u t..v t, c ∂μ)) fun (t : ι) ↦
    ∫ (x : ℝ) in u t..v t, 1 ∂μ
have pos : IsLittleO.{u_1, u_3, 0} (E := E) (F := ℝ) lt
  (fun (t : ι) ↦ ∫ (x : ℝ) in u t..v t, f x ∂μ - (μ.real (Ioc (u t) (v t)) • c - μ.real (Ioc (v t) (u t)) • c))
  fun (t : ι) ↦ HSMul.hSMul (β := ℝ) (μ.real (Ioc (u t) (v t))) 1 - HSMul.hSMul (β := ℝ) (μ.real (Ioc (v t) (u t))) 1
Tactic: simp_rw [integral_const', sub_smul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus (goal)
Goal:
ι : Type u_1
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
c : E
l l' : Filter ℝ
lt : Filter ι
μ : Measure ℝ
u v : ι → ℝ
inst_2 : l'.IsMeasurablyGenerated
inst_3 : TendstoIxxClass Ioc l l'
hfm : StronglyMeasurableAtFilter f l' μ
hf : Tendsto f (l' ⊓ ae μ) (𝓝 c)
hl : μ.FiniteAtFilter l'
hu : Tendsto u lt l
hv : Tendsto v lt l
hE : CompleteSpace E
A :
  IsLittleO.{u_1, u_3, 0} (E := E) (F := ℝ) lt
    (fun (i : ι) ↦ ∫ (x : ℝ) in Ioc (u i) (v i), f x ∂μ - μ.real (Ioc (u i) (v i)) • c) fun (i : ι) ↦
    μ.real (Ioc (u i) (v i))
B :
  IsLittleO.{u_1, u_3, 0} (E := E) (F := ℝ) lt
    (fun (i : ι) ↦ ∫ (x : ℝ) in Ioc (v i) (u i), f x ∂μ - μ.real (Ioc (v i) (u i)) • c) fun (i : ι) ↦
    μ.real (Ioc (v i) (u i))
⊢ IsLittleO.{u_1, u_3, 0} (E := E) (F := ℝ) lt
    (fun (t : ι) ↦ ∫ (x : ℝ) in u t..v t, f x ∂μ - (μ.real (Ioc (u t) (v t)) • c - μ.real (Ioc (v t) (u t)) • c))
    fun (t : ι) ↦ HSMul.hSMul (β := ℝ) (μ.real (Ioc (u t) (v t))) 1 - HSMul.hSMul (β := ℝ) (μ.real (Ioc (v t) (u t))) 1
have pos : ∀ (t : ι),
  ‖μ.real (Ioc (u t) (v t))‖ ≤
    ‖HSMul.hSMul (β := ℝ) (μ.real (Ioc (u t) (v t))) 1 - HSMul.hSMul (β := ℝ) (μ.real (Ioc (v t) (u t))) 1‖
Tactic: refine ((A.trans_le fun t ↦ ?_).sub (B.trans_le fun t ↦ ?_)).congr_left fun t ↦ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus (goal)
Goal:
ι : Type u_1
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
c : E
l l' : Filter ℝ
lt : Filter ι
μ : Measure ℝ
u v : ι → ℝ
inst_2 : l'.IsMeasurablyGenerated
inst_3 : TendstoIxxClass Ioc l l'
hfm : StronglyMeasurableAtFilter f l' μ
hf : Tendsto f (l' ⊓ ae μ) (𝓝 c)
hl : μ.FiniteAtFilter l'
hu : Tendsto u lt l
hv : Tendsto v lt l
hE : CompleteSpace E
A :
  IsLittleO.{u_1, u_3, 0} (E := E) (F := ℝ) lt
    (fun (i : ι) ↦ ∫ (x : ℝ) in Ioc (u i) (v i), f x ∂μ - μ.real (Ioc (u i) (v i)) • c) fun (i : ι) ↦
    μ.real (Ioc (u i) (v i))
B :
  IsLittleO.{u_1, u_3, 0} (E := E) (F := ℝ) lt
    (fun (i : ι) ↦ ∫ (x : ℝ) in Ioc (v i) (u i), f x ∂μ - μ.real (Ioc (v i) (u i)) • c) fun (i : ι) ↦
    μ.real (Ioc (v i) (u i))
pos :
  ∀ (t : ι),
    ‖μ.real (Ioc (u t) (v t))‖ ≤
      ‖HSMul.hSMul (β := ℝ) (μ.real (Ioc (u t) (v t))) 1 - HSMul.hSMul (β := ℝ) (μ.real (Ioc (v t) (u t))) 1‖
⊢ IsLittleO.{u_1, u_3, 0} (E := E) (F := ℝ) lt
    (fun (t : ι) ↦ ∫ (x : ℝ) in u t..v t, f x ∂μ - (μ.real (Ioc (u t) (v t)) • c - μ.real (Ioc (v t) (u t)) • c))
    fun (t : ι) ↦ HSMul.hSMul (β := ℝ) (μ.real (Ioc (u t) (v t))) 1 - HSMul.hSMul (β := ℝ) (μ.real (Ioc (v t) (u t))) 1
have pos₁ : ∀ (t : ι),
  ‖μ.real (Ioc (v t) (u t))‖ ≤
    ‖HSMul.hSMul (β := ℝ) (μ.real (Ioc (u t) (v t))) 1 - HSMul.hSMul (β := ℝ) (μ.real (Ioc (v t) (u t))) 1‖
Tactic: refine ((A.trans_le fun t ↦ ?_).sub (B.trans_le fun t ↦ ?_)).congr_left fun t ↦ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus (goal)
Goal:
ι : Type u_1
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
c : E
l l' : Filter ℝ
lt : Filter ι
μ : Measure ℝ
u v : ι → ℝ
inst_2 : l'.IsMeasurablyGenerated
inst_3 : TendstoIxxClass Ioc l l'
hfm : StronglyMeasurableAtFilter f l' μ
hf : Tendsto f (l' ⊓ ae μ) (𝓝 c)
hl : μ.FiniteAtFilter l'
hu : Tendsto u lt l
hv : Tendsto v lt l
hE : CompleteSpace E
A :
  IsLittleO.{u_1, u_3, 0} (E := E) (F := ℝ) lt
    (fun (i : ι) ↦ ∫ (x : ℝ) in Ioc (u i) (v i), f x ∂μ - μ.real (Ioc (u i) (v i)) • c) fun (i : ι) ↦
    μ.real (Ioc (u i) (v i))
B :
  IsLittleO.{u_1, u_3, 0} (E := E) (F := ℝ) lt
    (fun (i : ι) ↦ ∫ (x : ℝ) in Ioc (v i) (u i), f x ∂μ - μ.real (Ioc (v i) (u i)) • c) fun (i : ι) ↦
    μ.real (Ioc (v i) (u i))
pos :
  ∀ (t : ι),
    ‖μ.real (Ioc (u t) (v t))‖ ≤
      ‖HSMul.hSMul (β := ℝ) (μ.real (Ioc (u t) (v t))) 1 - HSMul.hSMul (β := ℝ) (μ.real (Ioc (v t) (u t))) 1‖
pos₁ :
  ∀ (t : ι),
    ‖μ.real (Ioc (v t) (u t))‖ ≤
      ‖HSMul.hSMul (β := ℝ) (μ.real (Ioc (u t) (v t))) 1 - HSMul.hSMul (β := ℝ) (μ.real (Ioc (v t) (u t))) 1‖
⊢ IsLittleO.{u_1, u_3, 0} (E := E) (F := ℝ) lt
    (fun (t : ι) ↦ ∫ (x : ℝ) in u t..v t, f x ∂μ - (μ.real (Ioc (u t) (v t)) • c - μ.real (Ioc (v t) (u t)) • c))
    fun (t : ι) ↦ HSMul.hSMul (β := ℝ) (μ.real (Ioc (u t) (v t))) 1 - HSMul.hSMul (β := ℝ) (μ.real (Ioc (v t) (u t))) 1
have pos₂ : ∀ (t : ι),
  ∫ (x : ℝ) in Ioc (u t) (v t), f x ∂μ - μ.real (Ioc (u t) (v t)) • c -
      (∫ (x : ℝ) in Ioc (v t) (u t), f x ∂μ - μ.real (Ioc (v t) (u t)) • c) =
    ∫ (x : ℝ) in u t..v t, f x ∂μ - (μ.real (Ioc (u t) (v t)) • c - μ.real (Ioc (v t) (u t)) • c)
Tactic: refine ((A.trans_le fun t ↦ ?_).sub (B.trans_le fun t ↦ ?_)).congr_left fun t ↦ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus (goal)
Goal:
ι : Type u_1
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
c : E
l l' : Filter ℝ
lt : Filter ι
μ : Measure ℝ
u v : ι → ℝ
inst_2 : l'.IsMeasurablyGenerated
inst_3 : TendstoIxxClass Ioc l l'
hfm : StronglyMeasurableAtFilter f l' μ
hf : Tendsto f (l' ⊓ ae μ) (𝓝 c)
hl : μ.FiniteAtFilter l'
hu : Tendsto u lt l
hv : Tendsto v lt l
hE : CompleteSpace E
A :
  IsLittleO.{u_1, u_3, 0} (E := E) (F := ℝ) lt
    (fun (i : ι) ↦ ∫ (x : ℝ) in Ioc (u i) (v i), f x ∂μ - μ.real (Ioc (u i) (v i)) • c) fun (i : ι) ↦
    μ.real (Ioc (u i) (v i))
B :
  IsLittleO.{u_1, u_3, 0} (E := E) (F := ℝ) lt
    (fun (i : ι) ↦ ∫ (x : ℝ) in Ioc (v i) (u i), f x ∂μ - μ.real (Ioc (v i) (u i)) • c) fun (i : ι) ↦
    μ.real (Ioc (v i) (u i))
t : ι
⊢ ‖μ.real (Ioc (u t) (v t))‖ ≤
    ‖HSMul.hSMul (β := ℝ) (μ.real (Ioc (u t) (v t))) 1 - HSMul.hSMul (β := ℝ) (μ.real (Ioc (v t) (u t))) 1‖
have pos : u t ≤ v t →
  ‖μ.real (Ioc (u t) (v t))‖ ≤
    ‖HSMul.hSMul (β := ℝ) (μ.real (Ioc (u t) (v t))) 1 - HSMul.hSMul (β := ℝ) (μ.real (Ioc (v t) (u t))) 1‖
Tactic: cases le_total (u t) (v t)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus (goal)
Goal:
ι : Type u_1
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
c : E
l l' : Filter ℝ
lt : Filter ι
μ : Measure ℝ
u v : ι → ℝ
inst_2 : l'.IsMeasurablyGenerated
inst_3 : TendstoIxxClass Ioc l l'
hfm : StronglyMeasurableAtFilter f l' μ
hf : Tendsto f (l' ⊓ ae μ) (𝓝 c)
hl : μ.FiniteAtFilter l'
hu : Tendsto u lt l
hv : Tendsto v lt l
hE : CompleteSpace E
A :
  IsLittleO.{u_1, u_3, 0} (E := E) (F := ℝ) lt
    (fun (i : ι) ↦ ∫ (x : ℝ) in Ioc (u i) (v i), f x ∂μ - μ.real (Ioc (u i) (v i)) • c) fun (i : ι) ↦
    μ.real (Ioc (u i) (v i))
B :
  IsLittleO.{u_1, u_3, 0} (E := E) (F := ℝ) lt
    (fun (i : ι) ↦ ∫ (x : ℝ) in Ioc (v i) (u i), f x ∂μ - μ.real (Ioc (v i) (u i)) • c) fun (i : ι) ↦
    μ.real (Ioc (v i) (u i))
t : ι
pos :
  u t ≤ v t →
    ‖μ.real (Ioc (u t) (v t))‖ ≤
      ‖HSMul.hSMul (β := ℝ) (μ.real (Ioc (u t) (v t))) 1 - HSMul.hSMul (β := ℝ) (μ.real (Ioc (v t) (u t))) 1‖
⊢ ‖μ.real (Ioc (u t) (v t))‖ ≤
    ‖HSMul.hSMul (β := ℝ) (μ.real (Ioc (u t) (v t))) 1 - HSMul.hSMul (β := ℝ) (μ.real (Ioc (v t) (u t))) 1‖
have pos₁ : v t ≤ u t →
  ‖μ.real (Ioc (u t) (v t))‖ ≤
    ‖HSMul.hSMul (β := ℝ) (μ.real (Ioc (u t) (v t))) 1 - HSMul.hSMul (β := ℝ) (μ.real (Ioc (v t) (u t))) 1‖
Tactic: cases le_total (u t) (v t)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus (goal)
Goal:
ι : Type u_1
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
c : E
l l' : Filter ℝ
lt : Filter ι
μ : Measure ℝ
u v : ι → ℝ
inst_2 : l'.IsMeasurablyGenerated
inst_3 : TendstoIxxClass Ioc l l'
hfm : StronglyMeasurableAtFilter f l' μ
hf : Tendsto f (l' ⊓ ae μ) (𝓝 c)
hl : μ.FiniteAtFilter l'
hu : Tendsto u lt l
hv : Tendsto v lt l
hE : CompleteSpace E
A :
  IsLittleO.{u_1, u_3, 0} (E := E) (F := ℝ) lt
    (fun (i : ι) ↦ ∫ (x : ℝ) in Ioc (u i) (v i), f x ∂μ - μ.real (Ioc (u i) (v i)) • c) fun (i : ι) ↦
    μ.real (Ioc (u i) (v i))
B :
  IsLittleO.{u_1, u_3, 0} (E := E) (F := ℝ) lt
    (fun (i : ι) ↦ ∫ (x : ℝ) in Ioc (v i) (u i), f x ∂μ - μ.real (Ioc (v i) (u i)) • c) fun (i : ι) ↦
    μ.real (Ioc (v i) (u i))
t : ι
⊢ ‖μ.real (Ioc (v t) (u t))‖ ≤
    ‖HSMul.hSMul (β := ℝ) (μ.real (Ioc (u t) (v t))) 1 - HSMul.hSMul (β := ℝ) (μ.real (Ioc (v t) (u t))) 1‖
have pos : u t ≤ v t →
  ‖μ.real (Ioc (v t) (u t))‖ ≤
    ‖HSMul.hSMul (β := ℝ) (μ.real (Ioc (u t) (v t))) 1 - HSMul.hSMul (β := ℝ) (μ.real (Ioc (v t) (u t))) 1‖
Tactic: cases le_total (u t) (v t)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus (goal)
Goal:
ι : Type u_1
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
c : E
l l' : Filter ℝ
lt : Filter ι
μ : Measure ℝ
u v : ι → ℝ
inst_2 : l'.IsMeasurablyGenerated
inst_3 : TendstoIxxClass Ioc l l'
hfm : StronglyMeasurableAtFilter f l' μ
hf : Tendsto f (l' ⊓ ae μ) (𝓝 c)
hl : μ.FiniteAtFilter l'
hu : Tendsto u lt l
hv : Tendsto v lt l
hE : CompleteSpace E
A :
  IsLittleO.{u_1, u_3, 0} (E := E) (F := ℝ) lt
    (fun (i : ι) ↦ ∫ (x : ℝ) in Ioc (u i) (v i), f x ∂μ - μ.real (Ioc (u i) (v i)) • c) fun (i : ι) ↦
    μ.real (Ioc (u i) (v i))
B :
  IsLittleO.{u_1, u_3, 0} (E := E) (F := ℝ) lt
    (fun (i : ι) ↦ ∫ (x : ℝ) in Ioc (v i) (u i), f x ∂μ - μ.real (Ioc (v i) (u i)) • c) fun (i : ι) ↦
    μ.real (Ioc (v i) (u i))
t : ι
pos :
  u t ≤ v t →
    ‖μ.real (Ioc (v t) (u t))‖ ≤
      ‖HSMul.hSMul (β := ℝ) (μ.real (Ioc (u t) (v t))) 1 - HSMul.hSMul (β := ℝ) (μ.real (Ioc (v t) (u t))) 1‖
⊢ ‖μ.real (Ioc (v t) (u t))‖ ≤
    ‖HSMul.hSMul (β := ℝ) (μ.real (Ioc (u t) (v t))) 1 - HSMul.hSMul (β := ℝ) (μ.real (Ioc (v t) (u t))) 1‖
have pos₁ : v t ≤ u t →
  ‖μ.real (Ioc (v t) (u t))‖ ≤
    ‖HSMul.hSMul (β := ℝ) (μ.real (Ioc (u t) (v t))) 1 - HSMul.hSMul (β := ℝ) (μ.real (Ioc (v t) (u t))) 1‖
Tactic: cases le_total (u t) (v t)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus (goal)
Goal:
ι : Type u_1
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
c : E
l l' : Filter ℝ
lt : Filter ι
μ : Measure ℝ
u v : ι → ℝ
inst_2 : l'.IsMeasurablyGenerated
inst_3 : TendstoIxxClass Ioc l l'
hfm : StronglyMeasurableAtFilter f l' μ
hf : Tendsto f (l' ⊓ ae μ) (𝓝 c)
hl : μ.FiniteAtFilter l'
hu : Tendsto u lt l
hv : Tendsto v lt l
hE : CompleteSpace E
A :
  IsLittleO.{u_1, u_3, 0} (E := E) (F := ℝ) lt
    (fun (i : ι) ↦ ∫ (x : ℝ) in Ioc (u i) (v i), f x ∂μ - μ.real (Ioc (u i) (v i)) • c) fun (i : ι) ↦
    μ.real (Ioc (u i) (v i))
B :
  IsLittleO.{u_1, u_3, 0} (E := E) (F := ℝ) lt
    (fun (i : ι) ↦ ∫ (x : ℝ) in Ioc (v i) (u i), f x ∂μ - μ.real (Ioc (v i) (u i)) • c) fun (i : ι) ↦
    μ.real (Ioc (v i) (u i))
t : ι
⊢ ∫ (x : ℝ) in Ioc (u t) (v t), f x ∂μ - μ.real (Ioc (u t) (v t)) • c -
      (∫ (x : ℝ) in Ioc (v t) (u t), f x ∂μ - μ.real (Ioc (v t) (u t)) • c) =
    ∫ (x : ℝ) in u t..v t, f x ∂μ - (μ.real (Ioc (u t) (v t)) • c - μ.real (Ioc (v t) (u t)) • c)
have pos : ∫ (x : ℝ) in Ioc (u t) (v t), f x ∂μ - μ.real (Ioc (u t) (v t)) • c -
    (∫ (x : ℝ) in Ioc (v t) (u t), f x ∂μ - μ.real (Ioc (v t) (u t)) • c) =
  HSub.hSub (α := E) (∫ (x : ℝ) in Ioc (u t) (v t), f x ∂μ) (∫ (x : ℝ) in Ioc (v t) (u t), f x ∂μ) -
    (μ.real (Ioc (u t) (v t)) • c - μ.real (Ioc (v t) (u t)) • c)
Tactic: simp_rw [intervalIntegral]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus (hypothesis)
Goal:
ι : Type u_1
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
ca cb : E
la la' lb lb' : Filter ℝ
lt : Filter ι
μ : Measure ℝ
ua va ub vb : ι → ℝ
inst_2 : IsLocallyFiniteMeasure μ
inst_3 : FTCFilter a la la'
inst_4 : FTCFilter b lb lb'
hab : IntervalIntegrable f μ a b
hmeas_a : StronglyMeasurableAtFilter f la' μ
hmeas_b : StronglyMeasurableAtFilter f lb' μ
ha_lim : Tendsto f (la' ⊓ ae μ) (𝓝 ca)
hb_lim : Tendsto f (lb' ⊓ ae μ) (𝓝 cb)
hua : Tendsto ua lt la
hva : Tendsto va lt la
hub : Tendsto ub lt lb
hvb : Tendsto vb lt lb
⊢ IsLittleO.{u_1, u_3, 0} (E := E) (F := ℝ) lt
    (fun (t : ι) ↦
      HSub.hSub (α := E) (∫ (x : ℝ) in va t..vb t, f x ∂μ) (∫ (x : ℝ) in ua t..ub t, f x ∂μ) -
        HSub.hSub (α := E) (∫ (x : ℝ) in ub t..vb t, cb ∂μ) (∫ (x : ℝ) in ua t..va t, ca ∂μ))
    fun (t : ι) ↦ norm (E := ℝ) (∫ (x : ℝ) in ua t..va t, 1 ∂μ) + norm (E := ℝ) (∫ (x : ℝ) in ub t..vb t, 1 ∂μ)
have this : la'.IsMeasurablyGenerated
Tactic: haveI := FTCFilter.meas_gen la
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus (hypothesis)
Goal:
ι : Type u_1
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
ca cb : E
la la' lb lb' : Filter ℝ
lt : Filter ι
μ : Measure ℝ
ua va ub vb : ι → ℝ
inst_2 : IsLocallyFiniteMeasure μ
inst_3 : FTCFilter a la la'
inst_4 : FTCFilter b lb lb'
hab : IntervalIntegrable f μ a b
hmeas_a : StronglyMeasurableAtFilter f la' μ
hmeas_b : StronglyMeasurableAtFilter f lb' μ
ha_lim : Tendsto f (la' ⊓ ae μ) (𝓝 ca)
hb_lim : Tendsto f (lb' ⊓ ae μ) (𝓝 cb)
hua : Tendsto ua lt la
hva : Tendsto va lt la
hub : Tendsto ub lt lb
hvb : Tendsto vb lt lb
this : la'.IsMeasurablyGenerated
⊢ IsLittleO.{u_1, u_3, 0} (E := E) (F := ℝ) lt
    (fun (t : ι) ↦
      HSub.hSub (α := E) (∫ (x : ℝ) in va t..vb t, f x ∂μ) (∫ (x : ℝ) in ua t..ub t, f x ∂μ) -
        HSub.hSub (α := E) (∫ (x : ℝ) in ub t..vb t, cb ∂μ) (∫ (x : ℝ) in ua t..va t, ca ∂μ))
    fun (t : ι) ↦ norm (E := ℝ) (∫ (x : ℝ) in ua t..va t, 1 ∂μ) + norm (E := ℝ) (∫ (x : ℝ) in ub t..vb t, 1 ∂μ)
have this₁ : lb'.IsMeasurablyGenerated
Tactic: haveI := FTCFilter.meas_gen lb
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus (goal)
Goal:
ι : Type u_1
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
ca cb : E
la la' lb lb' : Filter ℝ
lt : Filter ι
μ : Measure ℝ
ua va ub vb : ι → ℝ
inst_2 : IsLocallyFiniteMeasure μ
inst_3 : FTCFilter a la la'
inst_4 : FTCFilter b lb lb'
hab : IntervalIntegrable f μ a b
hmeas_a : StronglyMeasurableAtFilter f la' μ
hmeas_b : StronglyMeasurableAtFilter f lb' μ
ha_lim : Tendsto f (la' ⊓ ae μ) (𝓝 ca)
hb_lim : Tendsto f (lb' ⊓ ae μ) (𝓝 cb)
hua : Tendsto ua lt la
hva : Tendsto va lt la
hub : Tendsto ub lt lb
hvb : Tendsto vb lt lb
this_1 : la'.IsMeasurablyGenerated
this : lb'.IsMeasurablyGenerated
⊢ IsLittleO.{u_1, u_3, 0} (E := E) (F := ℝ) lt
    (fun (t : ι) ↦
      HSub.hSub (α := E) (∫ (x : ℝ) in va t..vb t, f x ∂μ) (∫ (x : ℝ) in ua t..ub t, f x ∂μ) -
        HSub.hSub (α := E) (∫ (x : ℝ) in ub t..vb t, cb ∂μ) (∫ (x : ℝ) in ua t..va t, ca ∂μ))
    fun (t : ι) ↦ norm (E := ℝ) (∫ (x : ℝ) in ua t..va t, 1 ∂μ) + norm (E := ℝ) (∫ (x : ℝ) in ub t..vb t, 1 ∂μ)
have hmeas_a₁ : EventuallyEq.{u_1, u_3} (β := E) lt
  (fun (x : ι) ↦
    -HSub.hSub (α := E) (∫ (x : ℝ) in ua x..va x, f x ∂μ) (∫ (x : ℝ) in ua x..va x, ca ∂μ) +
      HSub.hSub (α := E) (∫ (x : ℝ) in ub x..vb x, f x ∂μ) (∫ (x : ℝ) in ub x..vb x, cb ∂μ))
  fun (t : ι) ↦
  HSub.hSub (α := E) (∫ (x : ℝ) in va t..vb t, f x ∂μ) (∫ (x : ℝ) in ua t..ub t, f x ∂μ) -
    HSub.hSub (α := E) (∫ (x : ℝ) in ub t..vb t, cb ∂μ) (∫ (x : ℝ) in ua t..va t, ca ∂μ)
Tactic: refine
    ((measure_integral_sub_linear_isLittleO_of_tendsto_ae hmeas_a ha_lim hua hva).neg_left.add_add
          (measure_integral_sub_linear_isLittleO_of_tendsto_ae hmeas_b hb_lim hub hvb)).congr'
      ?_ EventuallyEq.rfl
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus (hypothesis)
Goal:
ι : Type u_1
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
ca cb : E
la la' lb lb' : Filter ℝ
lt : Filter ι
μ : Measure ℝ
ua va ub vb : ι → ℝ
inst_2 : IsLocallyFiniteMeasure μ
inst_3 : FTCFilter a la la'
inst_4 : FTCFilter b lb lb'
hab : IntervalIntegrable f μ a b
hmeas_a : StronglyMeasurableAtFilter f la' μ
hmeas_b : StronglyMeasurableAtFilter f lb' μ
ha_lim : Tendsto f (la' ⊓ ae μ) (𝓝 ca)
hb_lim : Tendsto f (lb' ⊓ ae μ) (𝓝 cb)
hua : Tendsto ua lt la
hva : Tendsto va lt la
hub : Tendsto ub lt lb
hvb : Tendsto vb lt lb
this_1 : la'.IsMeasurablyGenerated
this : lb'.IsMeasurablyGenerated
⊢ EventuallyEq.{u_1, u_3} (β := E) lt
    (fun (x : ι) ↦
      -HSub.hSub (α := E) (∫ (x : ℝ) in ua x..va x, f x ∂μ) (∫ (x : ℝ) in ua x..va x, ca ∂μ) +
        HSub.hSub (α := E) (∫ (x : ℝ) in ub x..vb x, f x ∂μ) (∫ (x : ℝ) in ub x..vb x, cb ∂μ))
    fun (t : ι) ↦
    HSub.hSub (α := E) (∫ (x : ℝ) in va t..vb t, f x ∂μ) (∫ (x : ℝ) in ua t..ub t, f x ∂μ) -
      HSub.hSub (α := E) (∫ (x : ℝ) in ub t..vb t, cb ∂μ) (∫ (x : ℝ) in ua t..va t, ca ∂μ)
have A : ∀ᶠ (t : ι) in lt, IntervalIntegrable f μ (ua t) (va t)
Tactic: have A : ∀ᶠ t in lt, IntervalIntegrable f μ (ua t) (va t) :=
    ha_lim.eventually_intervalIntegrable_ae hmeas_a (FTCFilter.finiteAt_inner la) hua hva
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus (hypothesis)
Goal:
ι : Type u_1
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
ca cb : E
la la' lb lb' : Filter ℝ
lt : Filter ι
μ : Measure ℝ
ua va ub vb : ι → ℝ
inst_2 : IsLocallyFiniteMeasure μ
inst_3 : FTCFilter a la la'
inst_4 : FTCFilter b lb lb'
hab : IntervalIntegrable f μ a b
hmeas_a : StronglyMeasurableAtFilter f la' μ
hmeas_b : StronglyMeasurableAtFilter f lb' μ
ha_lim : Tendsto f (la' ⊓ ae μ) (𝓝 ca)
hb_lim : Tendsto f (lb' ⊓ ae μ) (𝓝 cb)
hua : Tendsto ua lt la
hva : Tendsto va lt la
hub : Tendsto ub lt lb
hvb : Tendsto vb lt lb
this_1 : la'.IsMeasurablyGenerated
this : lb'.IsMeasurablyGenerated
A : ∀ᶠ (t : ι) in lt, IntervalIntegrable f μ (ua t) (va t)
⊢ EventuallyEq.{u_1, u_3} (β := E) lt
    (fun (x : ι) ↦
      -HSub.hSub (α := E) (∫ (x : ℝ) in ua x..va x, f x ∂μ) (∫ (x : ℝ) in ua x..va x, ca ∂μ) +
        HSub.hSub (α := E) (∫ (x : ℝ) in ub x..vb x, f x ∂μ) (∫ (x : ℝ) in ub x..vb x, cb ∂μ))
    fun (t : ι) ↦
    HSub.hSub (α := E) (∫ (x : ℝ) in va t..vb t, f x ∂μ) (∫ (x : ℝ) in ua t..ub t, f x ∂μ) -
      HSub.hSub (α := E) (∫ (x : ℝ) in ub t..vb t, cb ∂μ) (∫ (x : ℝ) in ua t..va t, ca ∂μ)
have A' : ∀ᶠ (t : ι) in lt, IntervalIntegrable f μ a (ua t)
Tactic: have A' : ∀ᶠ t in lt, IntervalIntegrable f μ a (ua t) :=
    ha_lim.eventually_intervalIntegrable_ae hmeas_a (FTCFilter.finiteAt_inner la)
      (tendsto_const_pure.mono_right FTCFilter.pure_le) hua