awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable (goal)
Goal:
f : ℝ → ℝ
a b : ℝ
hf : MonotoneOn f (Icc a b)
hab : a ≤ b
G : ℕ → ℝ → ℝ
hGf : ∀ᵐ (x : ℝ), x ∈ uIcc a b → Tendsto (fun (n : ℕ) ↦ G n x) atTop (𝓝 (deriv f x))
hG : ∀ (n : ℕ), AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) (G n) (Measure.restrict volume (uIcc a b))
hG' : liminf (fun (n : ℕ) ↦ ∫⁻ (x : ℝ) in uIcc a b, ‖G n x‖ₑ) atTop ≤ ENNReal.ofReal (f b - f a)
h₁ : ∀ᵐ (x : ℝ), x ≠ a
h₂ : ∀ᵐ (x : ℝ), x ≠ b
hG'₀ : Ne (α := ENNReal) (liminf (fun (n : ℕ) ↦ ∫⁻ (x : ℝ) in Icc a b, ‖G n x‖ₑ) atTop) ⊤
integrable_f_deriv : @Integrable _ _ _ _ Real.measurableSpace (deriv f) (Measure.restrict volume (Icc a b))
this : f a ≤ f b
f_deriv_nonneg : ∀ {x : ℝ} (hx : x ∈ Ioo a b), 0 ≤ deriv f x
⊢ LE.le (α := ℝ) 0 (∫ (x : ℝ) in a..b, deriv f x) ∧ ∫ (x : ℝ) in a..b, deriv f x ≤ f b - f a
have left : LE.le (α := ℝ) 0 (∫ (x : ℝ) in a..b, deriv f x)
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable (goal)
Goal:
f : ℝ → ℝ
a b : ℝ
hf : MonotoneOn f (Icc a b)
hab : a ≤ b
G : ℕ → ℝ → ℝ
hGf : ∀ᵐ (x : ℝ), x ∈ uIcc a b → Tendsto (fun (n : ℕ) ↦ G n x) atTop (𝓝 (deriv f x))
hG : ∀ (n : ℕ), AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) (G n) (Measure.restrict volume (uIcc a b))
hG' : liminf (fun (n : ℕ) ↦ ∫⁻ (x : ℝ) in uIcc a b, ‖G n x‖ₑ) atTop ≤ ENNReal.ofReal (f b - f a)
h₁ : ∀ᵐ (x : ℝ), x ≠ a
h₂ : ∀ᵐ (x : ℝ), x ≠ b
hG'₀ : Ne (α := ENNReal) (liminf (fun (n : ℕ) ↦ ∫⁻ (x : ℝ) in Icc a b, ‖G n x‖ₑ) atTop) ⊤
integrable_f_deriv : @Integrable _ _ _ _ Real.measurableSpace (deriv f) (Measure.restrict volume (Icc a b))
this : f a ≤ f b
f_deriv_nonneg : ∀ {x : ℝ} (hx : x ∈ Ioo a b), 0 ≤ deriv f x
left : LE.le (α := ℝ) 0 (∫ (x : ℝ) in a..b, deriv f x)
⊢ LE.le (α := ℝ) 0 (∫ (x : ℝ) in a..b, deriv f x) ∧ ∫ (x : ℝ) in a..b, deriv f x ≤ f b - f a
have right : ∫ (x : ℝ) in a..b, deriv f x ≤ f b - f a
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable (goal)
Goal:
f : ℝ → ℝ
a b : ℝ
hf : MonotoneOn f (Icc a b)
hab : a ≤ b
G : ℕ → ℝ → ℝ
hGf : ∀ᵐ (x : ℝ), x ∈ uIcc a b → Tendsto (fun (n : ℕ) ↦ G n x) atTop (𝓝 (deriv f x))
hG : ∀ (n : ℕ), AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) (G n) (Measure.restrict volume (uIcc a b))
hG' : liminf (fun (n : ℕ) ↦ ∫⁻ (x : ℝ) in uIcc a b, ‖G n x‖ₑ) atTop ≤ ENNReal.ofReal (f b - f a)
h₁ : ∀ᵐ (x : ℝ), x ≠ a
h₂ : ∀ᵐ (x : ℝ), x ≠ b
hG'₀ : Ne (α := ENNReal) (liminf (fun (n : ℕ) ↦ ∫⁻ (x : ℝ) in Icc a b, ‖G n x‖ₑ) atTop) ⊤
integrable_f_deriv : @Integrable _ _ _ _ Real.measurableSpace (deriv f) (Measure.restrict volume (Icc a b))
this : f a ≤ f b
f_deriv_nonneg : ∀ {x : ℝ} (hx : x ∈ Ioo a b), 0 ≤ deriv f x
⊢ LE.le (α := ℝ) 0 (∫ (x : ℝ) in a..b, deriv f x)
have left : 0 ≤ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Icc a b))] deriv f
Tactic: apply intervalIntegral.integral_nonneg_of_ae_restrict hab
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable (goal)
Goal:
f : ℝ → ℝ
a b : ℝ
hf : MonotoneOn f (Icc a b)
hab : a ≤ b
G : ℕ → ℝ → ℝ
hGf : ∀ᵐ (x : ℝ), x ∈ uIcc a b → Tendsto (fun (n : ℕ) ↦ G n x) atTop (𝓝 (deriv f x))
hG : ∀ (n : ℕ), AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) (G n) (Measure.restrict volume (uIcc a b))
hG' : liminf (fun (n : ℕ) ↦ ∫⁻ (x : ℝ) in uIcc a b, ‖G n x‖ₑ) atTop ≤ ENNReal.ofReal (f b - f a)
h₁ : ∀ᵐ (x : ℝ), x ≠ a
h₂ : ∀ᵐ (x : ℝ), x ≠ b
hG'₀ : Ne (α := ENNReal) (liminf (fun (n : ℕ) ↦ ∫⁻ (x : ℝ) in Icc a b, ‖G n x‖ₑ) atTop) ⊤
integrable_f_deriv : @Integrable _ _ _ _ Real.measurableSpace (deriv f) (Measure.restrict volume (Icc a b))
this : f a ≤ f b
f_deriv_nonneg : ∀ {x : ℝ} (hx : x ∈ Ioo a b), 0 ≤ deriv f x
⊢ 0 ≤ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Icc a b))] deriv f
have left : ∀ᵐ (x : ℝ), x ∈ Icc a b → 0 x ≤ deriv f x
Tactic: rw [Filter.EventuallyLE, MeasureTheory.ae_restrict_iff' (by simp)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable (goal)
Goal:
f : ℝ → ℝ
a b : ℝ
hf : MonotoneOn f (Icc a b)
hab : a ≤ b
G : ℕ → ℝ → ℝ
hGf : ∀ᵐ (x : ℝ), x ∈ uIcc a b → Tendsto (fun (n : ℕ) ↦ G n x) atTop (𝓝 (deriv f x))
hG : ∀ (n : ℕ), AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) (G n) (Measure.restrict volume (uIcc a b))
hG' : liminf (fun (n : ℕ) ↦ ∫⁻ (x : ℝ) in uIcc a b, ‖G n x‖ₑ) atTop ≤ ENNReal.ofReal (f b - f a)
h₁ : ∀ᵐ (x : ℝ), x ≠ a
h₂ : ∀ᵐ (x : ℝ), x ≠ b
hG'₀ : Ne (α := ENNReal) (liminf (fun (n : ℕ) ↦ ∫⁻ (x : ℝ) in Icc a b, ‖G n x‖ₑ) atTop) ⊤
integrable_f_deriv : @Integrable _ _ _ _ Real.measurableSpace (deriv f) (Measure.restrict volume (Icc a b))
this : f a ≤ f b
f_deriv_nonneg : ∀ {x : ℝ} (hx : x ∈ Ioo a b), 0 ≤ deriv f x
⊢ ∀ᵐ (x : ℝ), x ∈ Icc a b → 0 x ≤ deriv f x
have h : ∀ (x : ℝ), x ≠ a → x ≠ b → x ∈ Icc a b → 0 x ≤ deriv f x
Tactic: filter_upwards [h₁, h₂] with x _ _ _
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable (hypothesis)
Goal:
f : ℝ → ℝ
a b : ℝ
hf : MonotoneOn f (Icc a b)
hab : a ≤ b
G : ℕ → ℝ → ℝ
hGf : ∀ᵐ (x : ℝ), x ∈ uIcc a b → Tendsto (fun (n : ℕ) ↦ G n x) atTop (𝓝 (deriv f x))
hG : ∀ (n : ℕ), AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) (G n) (Measure.restrict volume (uIcc a b))
hG' : liminf (fun (n : ℕ) ↦ ∫⁻ (x : ℝ) in uIcc a b, ‖G n x‖ₑ) atTop ≤ ENNReal.ofReal (f b - f a)
h₁ : ∀ᵐ (x : ℝ), x ≠ a
h₂ : ∀ᵐ (x : ℝ), x ≠ b
hG'₀ : Ne (α := ENNReal) (liminf (fun (n : ℕ) ↦ ∫⁻ (x : ℝ) in Icc a b, ‖G n x‖ₑ) atTop) ⊤
integrable_f_deriv : @Integrable _ _ _ _ Real.measurableSpace (deriv f) (Measure.restrict volume (Icc a b))
this : f a ≤ f b
f_deriv_nonneg : ∀ {x : ℝ} (hx : x ∈ Ioo a b), 0 ≤ deriv f x
⊢ ∫ (x : ℝ) in a..b, deriv f x ≤ f b - f a
have ebound : ∫⁻ (x : ℝ) in uIcc a b, ‖deriv f x‖ₑ ∂volume ≤ liminf (fun (n : ℕ) ↦ ∫⁻ (x : ℝ) in uIcc a b, ‖G n x‖ₑ ∂volume) atTop
Tactic: have ebound := lintegral_enorm_le_liminf_of_tendsto
      ((MeasureTheory.ae_restrict_iff' (by measurability) |>.mpr hGf))
      (fun n ↦ (hG n).aemeasurable.enorm)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable (hypothesis)
Goal:
f : ℝ → ℝ
a b : ℝ
hf : MonotoneOn f (Icc a b)
hab : a ≤ b
G : ℕ → ℝ → ℝ
hGf : ∀ᵐ (x : ℝ), x ∈ uIcc a b → Tendsto (fun (n : ℕ) ↦ G n x) atTop (𝓝 (deriv f x))
hG : ∀ (n : ℕ), AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) (G n) (Measure.restrict volume (uIcc a b))
hG' : liminf (fun (n : ℕ) ↦ ∫⁻ (x : ℝ) in uIcc a b, ‖G n x‖ₑ) atTop ≤ ENNReal.ofReal (f b - f a)
h₁ : ∀ᵐ (x : ℝ), x ≠ a
h₂ : ∀ᵐ (x : ℝ), x ≠ b
hG'₀ : Ne (α := ENNReal) (liminf (fun (n : ℕ) ↦ ∫⁻ (x : ℝ) in Icc a b, ‖G n x‖ₑ) atTop) ⊤
integrable_f_deriv : @Integrable _ _ _ _ Real.measurableSpace (deriv f) (Measure.restrict volume (Icc a b))
this : f a ≤ f b
f_deriv_nonneg : ∀ {x : ℝ} (hx : x ∈ Ioo a b), 0 ≤ deriv f x
ebound :
  ∫⁻ (x : ℝ) in uIcc a b, ‖deriv f x‖ₑ ∂volume ≤ liminf (fun (n : ℕ) ↦ ∫⁻ (x : ℝ) in uIcc a b, ‖G n x‖ₑ ∂volume) atTop
⊢ ∫ (x : ℝ) in a..b, deriv f x ≤ f b - f a
have ebound₁ : ∫⁻ (x : ℝ) in uIcc a b, ‖deriv f x‖ₑ ∂volume ≤ ENNReal.ofReal (f b - f a)
Tactic: grw [hG'] at ebound
Cleared hypotheses: ebound
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable (goal)
Goal:
f : ℝ → ℝ
a b : ℝ
hf : MonotoneOn f (Icc a b)
hab : a ≤ b
G : ℕ → ℝ → ℝ
hGf : ∀ᵐ (x : ℝ), x ∈ uIcc a b → Tendsto (fun (n : ℕ) ↦ G n x) atTop (𝓝 (deriv f x))
hG : ∀ (n : ℕ), AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) (G n) (Measure.restrict volume (uIcc a b))
hG' : liminf (fun (n : ℕ) ↦ ∫⁻ (x : ℝ) in uIcc a b, ‖G n x‖ₑ) atTop ≤ ENNReal.ofReal (f b - f a)
h₁ : ∀ᵐ (x : ℝ), x ≠ a
h₂ : ∀ᵐ (x : ℝ), x ≠ b
hG'₀ : Ne (α := ENNReal) (liminf (fun (n : ℕ) ↦ ∫⁻ (x : ℝ) in Icc a b, ‖G n x‖ₑ) atTop) ⊤
integrable_f_deriv : @Integrable _ _ _ _ Real.measurableSpace (deriv f) (Measure.restrict volume (Icc a b))
this : f a ≤ f b
f_deriv_nonneg : ∀ {x : ℝ} (hx : x ∈ Ioo a b), 0 ≤ deriv f x
ebound :
  ENNReal.ofReal
      (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Icc a b)) fun (x : ℝ) ↦ ‖deriv f x‖) ≤
    ENNReal.ofReal (f b - f a)
⊢ 0 ≤ f b - f a
have linarith : f b - f a < 0 → f a - f b + (f b - f a - 0) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable (hypothesis)
Goal:
f : ℝ → ℝ
a b : ℝ
hf : MonotoneOn f (Icc a b)
hab : a ≤ b
G : ℕ → ℝ → ℝ
hGf : ∀ᵐ (x : ℝ), x ∈ uIcc a b → Tendsto (fun (n : ℕ) ↦ G n x) atTop (𝓝 (deriv f x))
hG : ∀ (n : ℕ), AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) (G n) (Measure.restrict volume (uIcc a b))
hG' : liminf (fun (n : ℕ) ↦ ∫⁻ (x : ℝ) in uIcc a b, ‖G n x‖ₑ) atTop ≤ ENNReal.ofReal (f b - f a)
h₁ : ∀ᵐ (x : ℝ), x ≠ a
h₂ : ∀ᵐ (x : ℝ), x ≠ b
hG'₀ : Ne (α := ENNReal) (liminf (fun (n : ℕ) ↦ ∫⁻ (x : ℝ) in Icc a b, ‖G n x‖ₑ) atTop) ⊤
integrable_f_deriv : @Integrable _ _ _ _ Real.measurableSpace (deriv f) (Measure.restrict volume (Icc a b))
this : f a ≤ f b
f_deriv_nonneg : ∀ {x : ℝ} (hx : x ∈ Ioo a b), 0 ≤ deriv f x
ebound : ∫⁻ (x : ℝ) in uIcc a b, ‖deriv f x‖ₑ ∂volume ≤ ENNReal.ofReal (f b - f a)
⊢ ∫ (x : ℝ) in a..b, deriv f x ≤ f b - f a
have ebound₁ : ∫ (x : ℝ) in a..b, ‖deriv f x‖ ≤ f b - f a
Tactic: rw [uIcc_of_le hab,
        ← MeasureTheory.ofReal_integral_norm_eq_lintegral_enorm integrable_f_deriv,
        ENNReal.ofReal_le_ofReal_iff (by linarith),
        integral_Icc_eq_integral_Ioc,
        ← intervalIntegral.integral_of_le hab] at ebound
Cleared hypotheses: ebound
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable (goal)
Goal:
f : ℝ → ℝ
a b : ℝ
hf : MonotoneOn f (Icc a b)
hab : a ≤ b
G : ℕ → ℝ → ℝ
hGf : ∀ᵐ (x : ℝ), x ∈ uIcc a b → Tendsto (fun (n : ℕ) ↦ G n x) atTop (𝓝 (deriv f x))
hG : ∀ (n : ℕ), AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) (G n) (Measure.restrict volume (uIcc a b))
hG' : liminf (fun (n : ℕ) ↦ ∫⁻ (x : ℝ) in uIcc a b, ‖G n x‖ₑ) atTop ≤ ENNReal.ofReal (f b - f a)
h₁ : ∀ᵐ (x : ℝ), x ≠ a
h₂ : ∀ᵐ (x : ℝ), x ≠ b
hG'₀ : Ne (α := ENNReal) (liminf (fun (n : ℕ) ↦ ∫⁻ (x : ℝ) in Icc a b, ‖G n x‖ₑ) atTop) ⊤
integrable_f_deriv : @Integrable _ _ _ _ Real.measurableSpace (deriv f) (Measure.restrict volume (Icc a b))
this : f a ≤ f b
f_deriv_nonneg : ∀ {x : ℝ} (hx : x ∈ Ioo a b), 0 ≤ deriv f x
ebound : ∫ (x : ℝ) in a..b, ‖deriv f x‖ ≤ f b - f a
⊢ ∫ (x : ℝ) in a..b, deriv f x ≤ f b - f a
have h : Eq (α := ℝ) (∫ (x : ℝ) in a..b, deriv f x) (∫ (x : ℝ) in a..b, ‖deriv f x‖)
Tactic: convert! ebound using 1
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable (goal)
Goal:
f : ℝ → ℝ
a b : ℝ
hf : MonotoneOn f (Icc a b)
hab : a ≤ b
G : ℕ → ℝ → ℝ
hGf : ∀ᵐ (x : ℝ), x ∈ uIcc a b → Tendsto (fun (n : ℕ) ↦ G n x) atTop (𝓝 (deriv f x))
hG : ∀ (n : ℕ), AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) (G n) (Measure.restrict volume (uIcc a b))
hG' : liminf (fun (n : ℕ) ↦ ∫⁻ (x : ℝ) in uIcc a b, ‖G n x‖ₑ) atTop ≤ ENNReal.ofReal (f b - f a)
h₁ : ∀ᵐ (x : ℝ), x ≠ a
h₂ : ∀ᵐ (x : ℝ), x ≠ b
hG'₀ : Ne (α := ENNReal) (liminf (fun (n : ℕ) ↦ ∫⁻ (x : ℝ) in Icc a b, ‖G n x‖ₑ) atTop) ⊤
integrable_f_deriv : @Integrable _ _ _ _ Real.measurableSpace (deriv f) (Measure.restrict volume (Icc a b))
this : f a ≤ f b
f_deriv_nonneg : ∀ {x : ℝ} (hx : x ∈ Ioo a b), 0 ≤ deriv f x
ebound : ∫ (x : ℝ) in a..b, ‖deriv f x‖ ≤ f b - f a
⊢ Eq (α := ℝ) (∫ (x : ℝ) in a..b, deriv f x) (∫ (x : ℝ) in a..b, ‖deriv f x‖)
have h : ∀ᵐ (x : ℝ), x ∈ uIoc a b → deriv f x = ‖deriv f x‖
Tactic: refine intervalIntegral.integral_congr_ae ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable (goal)
Goal:
f : ℝ → ℝ
a b : ℝ
hf : MonotoneOn f (Icc a b)
hab : a ≤ b
G : ℕ → ℝ → ℝ
hGf : ∀ᵐ (x : ℝ), x ∈ uIcc a b → Tendsto (fun (n : ℕ) ↦ G n x) atTop (𝓝 (deriv f x))
hG : ∀ (n : ℕ), AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) (G n) (Measure.restrict volume (uIcc a b))
hG' : liminf (fun (n : ℕ) ↦ ∫⁻ (x : ℝ) in uIcc a b, ‖G n x‖ₑ) atTop ≤ ENNReal.ofReal (f b - f a)
h₁ : ∀ᵐ (x : ℝ), x ≠ a
h₂ : ∀ᵐ (x : ℝ), x ≠ b
hG'₀ : Ne (α := ENNReal) (liminf (fun (n : ℕ) ↦ ∫⁻ (x : ℝ) in Icc a b, ‖G n x‖ₑ) atTop) ⊤
integrable_f_deriv : @Integrable _ _ _ _ Real.measurableSpace (deriv f) (Measure.restrict volume (Icc a b))
this : f a ≤ f b
f_deriv_nonneg : ∀ {x : ℝ} (hx : x ∈ Ioo a b), 0 ≤ deriv f x
ebound : ∫ (x : ℝ) in a..b, ‖deriv f x‖ ≤ f b - f a
⊢ ∀ᵐ (x : ℝ), x ∈ uIoc a b → deriv f x = ‖deriv f x‖
have h : ∀ᵐ (x : ℝ), x ∈ Ioc a b → deriv f x = ‖deriv f x‖
Tactic: rw [uIoc_of_le hab]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable (goal)
Goal:
f : ℝ → ℝ
a b : ℝ
hf : MonotoneOn f (Icc a b)
hab : a ≤ b
G : ℕ → ℝ → ℝ
hGf : ∀ᵐ (x : ℝ), x ∈ uIcc a b → Tendsto (fun (n : ℕ) ↦ G n x) atTop (𝓝 (deriv f x))
hG : ∀ (n : ℕ), AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) (G n) (Measure.restrict volume (uIcc a b))
hG' : liminf (fun (n : ℕ) ↦ ∫⁻ (x : ℝ) in uIcc a b, ‖G n x‖ₑ) atTop ≤ ENNReal.ofReal (f b - f a)
h₁ : ∀ᵐ (x : ℝ), x ≠ a
h₂ : ∀ᵐ (x : ℝ), x ≠ b
hG'₀ : Ne (α := ENNReal) (liminf (fun (n : ℕ) ↦ ∫⁻ (x : ℝ) in Icc a b, ‖G n x‖ₑ) atTop) ⊤
integrable_f_deriv : @Integrable _ _ _ _ Real.measurableSpace (deriv f) (Measure.restrict volume (Icc a b))
this : f a ≤ f b
f_deriv_nonneg : ∀ {x : ℝ} (hx : x ∈ Ioo a b), 0 ≤ deriv f x
ebound : ∫ (x : ℝ) in a..b, ‖deriv f x‖ ≤ f b - f a
⊢ ∀ᵐ (x : ℝ), x ∈ Ioc a b → deriv f x = ‖deriv f x‖
have h : ∀ (x : ℝ), x ≠ b → x ∈ Ioc a b → deriv f x = ‖deriv f x‖
Tactic: filter_upwards [h₂] with x _ _
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable (goal)
Goal:
f : ℝ → ℝ
a b : ℝ
hf : BoundedVariationOn f (uIcc a b)
⊢ IntervalIntegrable (deriv f) volume a b
have obtain : ∀ (p q : ℝ → ℝ) (hp : MonotoneOn p (uIcc a b)) (hq : MonotoneOn q (uIcc a b))
  (hf : BoundedVariationOn (p - q) (uIcc a b)), IntervalIntegrable (deriv (p - q)) volume a b
Tactic: obtain ⟨p, q, hp, hq, rfl⟩ := hf.locallyBoundedVariationOn.exists_monotoneOn_sub_monotoneOn
Cleared hypotheses: f, hf
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable (hypothesis)
Goal:
a b : ℝ
p q : ℝ → ℝ
hp : MonotoneOn p (uIcc a b)
hq : MonotoneOn q (uIcc a b)
hf : BoundedVariationOn (p - q) (uIcc a b)
⊢ IntervalIntegrable (deriv (p - q)) volume a b
have h₂ : ∀ᵐ (x : ℝ), x ≠ max a b
Tactic: have h₂ : ∀ᵐ x, x ≠ max a b := by simp [ae_iff, measure_singleton]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable (goal)
Goal:
a b : ℝ
p q : ℝ → ℝ
hp : MonotoneOn p (uIcc a b)
hq : MonotoneOn q (uIcc a b)
hf : BoundedVariationOn (p - q) (uIcc a b)
h₂ : ∀ᵐ (x : ℝ), x ≠ max a b
⊢ IntervalIntegrable (deriv (p - q)) volume a b
have apply : (fun (x : ℝ) ↦ deriv p x - deriv q x) =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (uIoc a b))] deriv (p - q)
Tactic: apply (hp.intervalIntegrable_deriv.sub hq.intervalIntegrable_deriv).congr_ae
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable (goal)
Goal:
a b : ℝ
p q : ℝ → ℝ
hp : MonotoneOn p (uIcc a b)
hq : MonotoneOn q (uIcc a b)
hf : BoundedVariationOn (p - q) (uIcc a b)
h₂ : ∀ᵐ (x : ℝ), x ≠ max a b
⊢ (fun (x : ℝ) ↦ deriv p x - deriv q x) =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (uIoc a b))] deriv (p - q)
have rw : ∀ᵐ (x : ℝ), x ∈ uIoc a b → deriv p x - deriv q x = deriv (p - q) x
Tactic: rw [Filter.EventuallyEq, MeasureTheory.ae_restrict_iff' (by simp [uIoc])]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable (goal)
Goal:
a b : ℝ
p q : ℝ → ℝ
hp : MonotoneOn p (uIcc a b)
hq : MonotoneOn q (uIcc a b)
hf : BoundedVariationOn (p - q) (uIcc a b)
h₂ : ∀ᵐ (x : ℝ), x ≠ max a b
⊢ ∀ᵐ (x : ℝ), x ∈ uIoc a b → deriv p x - deriv q x = deriv (p - q) x
have h : ∀ (x : ℝ) (hx₁ : x ∈ uIcc a b → DifferentiableWithinAt ℝ p (uIcc a b) x)
  (hx₂ : x ∈ uIcc a b → DifferentiableWithinAt ℝ q (uIcc a b) x) (hx₃ : x ≠ max a b) (hx₄ : x ∈ uIoc a b),
  deriv p x - deriv q x = deriv (p - q) x
Tactic: filter_upwards [hp.ae_differentiableWithinAt_of_mem, hq.ae_differentiableWithinAt_of_mem, h₂]
    with x hx₁ hx₂ hx₃ hx₄
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable (hypothesis)
Goal:
a b : ℝ
p q : ℝ → ℝ
hp : MonotoneOn p (uIcc a b)
hq : MonotoneOn q (uIcc a b)
hf : BoundedVariationOn (p - q) (uIcc a b)
h₂ : ∀ᵐ (x : ℝ), x ≠ max a b
x : ℝ
hx₁ : x ∈ uIcc a b → DifferentiableWithinAt ℝ p (uIcc a b) x
hx₂ : x ∈ uIcc a b → DifferentiableWithinAt ℝ q (uIcc a b) x
hx₃ : x ≠ max a b
hx₄ : x ∈ uIoc a b
⊢ deriv p x - deriv q x = deriv (p - q) x
have hx₅ : x ∈ uIcc a b
Tactic: have hx₅ : x ∈ uIcc a b := Ioc_subset_Icc_self hx₄
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable (hypothesis)
Goal:
a b : ℝ
p q : ℝ → ℝ
hp : MonotoneOn p (uIcc a b)
hq : MonotoneOn q (uIcc a b)
hf : BoundedVariationOn (p - q) (uIcc a b)
h₂ : ∀ᵐ (x : ℝ), x ≠ max a b
x : ℝ
hx₁ : x ∈ uIcc a b → DifferentiableWithinAt ℝ p (uIcc a b) x
hx₂ : x ∈ uIcc a b → DifferentiableWithinAt ℝ q (uIcc a b) x
hx₃ : x ≠ max a b
hx₄ : x ∈ uIoc a b
hx₅ : x ∈ uIcc a b
⊢ deriv p x - deriv q x = deriv (p - q) x
have hx₆ : min a b < x ∧ x ≤ max a b
Tactic: rw [uIoc, mem_Ioc] at hx₄
Cleared hypotheses: hx₄, hx₅
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable (hypothesis)
Goal:
a b : ℝ
p q : ℝ → ℝ
hp : MonotoneOn p (uIcc a b)
hq : MonotoneOn q (uIcc a b)
hf : BoundedVariationOn (p - q) (uIcc a b)
h₂ : ∀ᵐ (x : ℝ), x ≠ max a b
x : ℝ
hx₁ : x ∈ uIcc a b → DifferentiableWithinAt ℝ p (uIcc a b) x
hx₂ : x ∈ uIcc a b → DifferentiableWithinAt ℝ q (uIcc a b) x
hx₃ : x ≠ max a b
hx₄ : min a b < x ∧ x ≤ max a b
hx₅ : x ∈ uIcc a b
⊢ deriv p x - deriv q x = deriv (p - q) x
have hx₆ : uIcc a b ∈ 𝓝 x
Tactic: have hx₆ : uIcc a b ∈ 𝓝 x := Icc_mem_nhds hx₄.left (lt_of_le_of_ne hx₄.right hx₃)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable (hypothesis)
Goal:
a b : ℝ
p q : ℝ → ℝ
hp : MonotoneOn p (uIcc a b)
hq : MonotoneOn q (uIcc a b)
hf : BoundedVariationOn (p - q) (uIcc a b)
h₂ : ∀ᵐ (x : ℝ), x ≠ max a b
x : ℝ
hx₁ : x ∈ uIcc a b → DifferentiableWithinAt ℝ p (uIcc a b) x
hx₂ : x ∈ uIcc a b → DifferentiableWithinAt ℝ q (uIcc a b) x
hx₃ : x ≠ max a b
hx₄ : min a b < x ∧ x ≤ max a b
hx₅ : x ∈ uIcc a b
hx₆ : uIcc a b ∈ 𝓝 x
⊢ deriv p x - deriv q x = deriv (p - q) x
have hx₇ : HasDerivAt p (deriv p x) x
Tactic: replace hx₁ := (hx₁ hx₅).differentiableAt hx₆ |>.hasDerivAt
Cleared hypotheses: hx₁
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable (hypothesis)
Goal:
a b : ℝ
p q : ℝ → ℝ
hp : MonotoneOn p (uIcc a b)
hq : MonotoneOn q (uIcc a b)
hf : BoundedVariationOn (p - q) (uIcc a b)
h₂ : ∀ᵐ (x : ℝ), x ≠ max a b
x : ℝ
hx₂ : x ∈ uIcc a b → DifferentiableWithinAt ℝ q (uIcc a b) x
hx₃ : x ≠ max a b
hx₄ : min a b < x ∧ x ≤ max a b
hx₅ : x ∈ uIcc a b
hx₆ : uIcc a b ∈ 𝓝 x
hx₁ : HasDerivAt p (deriv p x) x
⊢ deriv p x - deriv q x = deriv (p - q) x
have hx₇ : HasDerivAt q (deriv q x) x
Tactic: replace hx₂ := (hx₂ hx₅).differentiableAt hx₆ |>.hasDerivAt
Cleared hypotheses: hx₂
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
B : ℝ → ℝ
hab : a ≤ b
hfc : ContinuousOn f (Icc a b)
hfd : DifferentiableOn ℝ f (Ioo a b)
hfB : ∀ᵐ (t : ℝ), t ∈ Ioo a b → ‖deriv f t‖ ≤ B t
hBi : IntervalIntegrable B volume a b
⊢ ‖f b - f a‖ ≤ ∫ (t : ℝ) in a..b, B t
have inr : ∀
  (this :
    ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_2 : NormedSpace ℝ E] {f : ℝ → E}
      (hfc : ContinuousOn f (Icc a b)) (hfd : DifferentiableOn ℝ f (Ioo a b))
      (hfB : ∀ᵐ (t : ℝ), t ∈ Ioo a b → ‖deriv f t‖ ≤ B t) (hE : CompleteSpace E), ‖f b - f a‖ ≤ ∫ (t : ℝ) in a..b, B t)
  (hE : ¬CompleteSpace E), ‖f b - f a‖ ≤ ∫ (t : ℝ) in a..b, B t
Tactic: wlog hE : CompleteSpace E generalizing E
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
B : ℝ → ℝ
hab : a ≤ b
hfc : ContinuousOn f (Icc a b)
hfd : DifferentiableOn ℝ f (Ioo a b)
hfB : ∀ᵐ (t : ℝ), t ∈ Ioo a b → ‖deriv f t‖ ≤ B t
hBi : IntervalIntegrable B volume a b
inr :
  ∀
    (this :
      ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_2 : NormedSpace ℝ E] {f : ℝ → E}
        (hfc : ContinuousOn f (Icc a b)) (hfd : DifferentiableOn ℝ f (Ioo a b))
        (hfB : ∀ᵐ (t : ℝ), t ∈ Ioo a b → ‖deriv f t‖ ≤ B t) (hE : CompleteSpace E),
        ‖f b - f a‖ ≤ ∫ (t : ℝ) in a..b, B t)
    (hE : ¬CompleteSpace E), ‖f b - f a‖ ≤ ∫ (t : ℝ) in a..b, B t
⊢ ‖f b - f a‖ ≤ ∫ (t : ℝ) in a..b, B t
have wlog : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_2 : NormedSpace ℝ E] {f : ℝ → E} (hfc : ContinuousOn f (Icc a b))
  (hfd : DifferentiableOn ℝ f (Ioo a b)) (hfB : ∀ᵐ (t : ℝ), t ∈ Ioo a b → ‖deriv f t‖ ≤ B t) (hE : CompleteSpace E),
  ‖f b - f a‖ ≤ ∫ (t : ℝ) in a..b, B t
Tactic: wlog hE : CompleteSpace E generalizing E
Cleared hypotheses: hfc, hfd, hfB
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
B : ℝ → ℝ
hab : a ≤ b
hfc : ContinuousOn f (Icc a b)
hfd : DifferentiableOn ℝ f (Ioo a b)
hfB : ∀ᵐ (t : ℝ), t ∈ Ioo a b → ‖deriv f t‖ ≤ B t
hBi : IntervalIntegrable B volume a b
this :
  ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_2 : NormedSpace ℝ E] {f : ℝ → E} (hfc : ContinuousOn f (Icc a b))
    (hfd : DifferentiableOn ℝ f (Ioo a b)) (hfB : ∀ᵐ (t : ℝ), t ∈ Ioo a b → ‖deriv f t‖ ≤ B t) (hE : CompleteSpace E),
    ‖f b - f a‖ ≤ ∫ (t : ℝ) in a..b, B t
hE : ¬CompleteSpace E
⊢ ‖f b - f a‖ ≤ ∫ (t : ℝ) in a..b, B t
have hg : let g : ℝ → UniformSpace.Completion E := UniformSpace.Completion.coe' ∘ f;
g = UniformSpace.Completion.coe' ∘ f
Tactic: set g : ℝ → UniformSpace.Completion E := (↑) ∘ f with hg
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
B : ℝ → ℝ
hab : a ≤ b
hfc : ContinuousOn f (Icc a b)
hfd : DifferentiableOn ℝ f (Ioo a b)
hfB : ∀ᵐ (t : ℝ), t ∈ Ioo a b → ‖deriv f t‖ ≤ B t
hBi : IntervalIntegrable B volume a b
this :
  ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_2 : NormedSpace ℝ E] {f : ℝ → E} (hfc : ContinuousOn f (Icc a b))
    (hfd : DifferentiableOn ℝ f (Ioo a b)) (hfB : ∀ᵐ (t : ℝ), t ∈ Ioo a b → ‖deriv f t‖ ≤ B t) (hE : CompleteSpace E),
    ‖f b - f a‖ ≤ ∫ (t : ℝ) in a..b, B t
hE : ¬CompleteSpace E
g : ℝ → UniformSpace.Completion E := UniformSpace.Completion.coe' ∘ f
hg : g = UniformSpace.Completion.coe' ∘ f
⊢ ‖f b - f a‖ ≤ ∫ (t : ℝ) in a..b, B t
have hgc : ContinuousOn g (Icc a b)
Tactic: have hgc : ContinuousOn g (Icc a b) :=
      (UniformSpace.Completion.continuous_coe E).comp_continuousOn hfc
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
B : ℝ → ℝ
hab : a ≤ b
hfc : ContinuousOn f (Icc a b)
hfd : DifferentiableOn ℝ f (Ioo a b)
hfB : ∀ᵐ (t : ℝ), t ∈ Ioo a b → ‖deriv f t‖ ≤ B t
hBi : IntervalIntegrable B volume a b
this :
  ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_2 : NormedSpace ℝ E] {f : ℝ → E} (hfc : ContinuousOn f (Icc a b))
    (hfd : DifferentiableOn ℝ f (Ioo a b)) (hfB : ∀ᵐ (t : ℝ), t ∈ Ioo a b → ‖deriv f t‖ ≤ B t) (hE : CompleteSpace E),
    ‖f b - f a‖ ≤ ∫ (t : ℝ) in a..b, B t
hE : ¬CompleteSpace E
g : ℝ → UniformSpace.Completion E := UniformSpace.Completion.coe' ∘ f
hg : g = UniformSpace.Completion.coe' ∘ f
hgc : ContinuousOn g (Icc a b)
⊢ ‖f b - f a‖ ≤ ∫ (t : ℝ) in a..b, B t
have hgd : DifferentiableOn ℝ g (Ioo a b)
Tactic: have hgd : DifferentiableOn ℝ g (Ioo a b) :=
      UniformSpace.Completion.toComplL.differentiable.comp_differentiableOn hfd