E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.31247
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → E
a b : ℝ
f' : ℝ → E
C : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ (x : ℝ), x ∈ Ico a b → HasDerivWithinAt f (f' x) (Ici x) x
bound : ∀ (x : ℝ), x ∈ Ico a b → ‖f' x‖ ≤ C
g : ℝ → E := fun x => f x - f a
⊢ ∀ (x : ℝ), x ∈ Icc a b → ‖f x - f a‖ ≤ C * (x - a)
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.31247
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → E
a b : ℝ
f' : ℝ → E
C : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ (x : ℝ), x ∈ Ico a b → HasDerivWithinAt f (f' x) (Ici x) x
bound : ∀ (x : ℝ), x ∈ Ico a b → ‖f' x‖ ≤ C
⊢ ∀ (x : ℝ), x ∈ Icc a b → ‖f x - f a‖ ≤ C * (x - a)
let g x := f x - f a
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.31247
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → E
a b : ℝ
f' : ℝ → E
C : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ (x : ℝ), x ∈ Ico a b → HasDerivWithinAt f (f' x) (Ici x) x
bound : ∀ (x : ℝ), x ∈ Ico a b → ‖f' x‖ ≤ C
g : ℝ → E := fun x => f x - f a
hg : ContinuousOn g (Icc a b)
⊢ ∀ (x : ℝ), x ∈ Icc a b → ‖f x - f a‖ ≤ C * (x - a)
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.31247
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → E
a b : ℝ
f' : ℝ → E
C : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ (x : ℝ), x ∈ Ico a b → HasDerivWithinAt f (f' x) (Ici x) x
bound : ∀ (x : ℝ), x ∈ Ico a b → ‖f' x‖ ≤ C
g : ℝ → E := fun x => f x - f a
⊢ ∀ (x : ℝ), x ∈ Icc a b → ‖f x - f a‖ ≤ C * (x - a)
have hg : ContinuousOn g (Icc a b) := hf.sub continuousOn_const
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.31247
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → E
a b : ℝ
f' : ℝ → E
C : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ (x : ℝ), x ∈ Ico a b → HasDerivWithinAt f (f' x) (Ici x) x
bound : ∀ (x : ℝ), x ∈ Ico a b → ‖f' x‖ ≤ C
g : ℝ → E := fun x => f x - f a
hg : ContinuousOn g (Icc a b)
hg' : ∀ (x : ℝ), x ∈ Ico a b → HasDerivWithinAt g (f' x) (Ici x) x
⊢ ∀ (x : ℝ), x ∈ Icc a b → ‖f x - f a‖ ≤ C * (x - a)
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.31247
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → E
a b : ℝ
f' : ℝ → E
C : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ (x : ℝ), x ∈ Ico a b → HasDerivWithinAt f (f' x) (Ici x) x
bound : ∀ (x : ℝ), x ∈ Ico a b → ‖f' x‖ ≤ C
g : ℝ → E := fun x => f x - f a
hg : ContinuousOn g (Icc a b)
⊢ ∀ (x : ℝ), x ∈ Icc a b → ‖f x - f a‖ ≤ C * (x - a)
have hg' : ∀ x ∈ Ico a b, HasDerivWithinAt g (f' x) (Ici x) x := by
  intro x hx
  simpa using (hf' x hx).sub (hasDerivWithinAt_const _ _ _)
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.31247
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → E
a b : ℝ
f' : ℝ → E
C : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ (x : ℝ), x ∈ Ico a b → HasDerivWithinAt f (f' x) (Ici x) x
bound : ∀ (x : ℝ), x ∈ Ico a b → ‖f' x‖ ≤ C
g : ℝ → E := fun x => f x - f a
hg : ContinuousOn g (Icc a b)
hg' : ∀ (x : ℝ), x ∈ Ico a b → HasDerivWithinAt g (f' x) (Ici x) x
B : ℝ → ℝ := fun x => C * (x - a)
⊢ ∀ (x : ℝ), x ∈ Icc a b → ‖f x - f a‖ ≤ C * (x - a)
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.31247
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → E
a b : ℝ
f' : ℝ → E
C : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ (x : ℝ), x ∈ Ico a b → HasDerivWithinAt f (f' x) (Ici x) x
bound : ∀ (x : ℝ), x ∈ Ico a b → ‖f' x‖ ≤ C
g : ℝ → E := fun x => f x - f a
hg : ContinuousOn g (Icc a b)
hg' : ∀ (x : ℝ), x ∈ Ico a b → HasDerivWithinAt g (f' x) (Ici x) x
⊢ ∀ (x : ℝ), x ∈ Icc a b → ‖f x - f a‖ ≤ C * (x - a)
let B x := C * (x - a)
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.31247
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → E
a b : ℝ
f' : ℝ → E
C : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ (x : ℝ), x ∈ Ico a b → HasDerivWithinAt f (f' x) (Ici x) x
bound : ∀ (x : ℝ), x ∈ Ico a b → ‖f' x‖ ≤ C
g : ℝ → E := fun x => f x - f a
hg : ContinuousOn g (Icc a b)
hg' : ∀ (x : ℝ), x ∈ Ico a b → HasDerivWithinAt g (f' x) (Ici x) x
B : ℝ → ℝ := fun x => C * (x - a)
hB : ∀ (x : ℝ), HasDerivAt B C x
⊢ ∀ (x : ℝ), x ∈ Icc a b → ‖f x - f a‖ ≤ C * (x - a)
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.31247
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → E
a b : ℝ
f' : ℝ → E
C : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ (x : ℝ), x ∈ Ico a b → HasDerivWithinAt f (f' x) (Ici x) x
bound : ∀ (x : ℝ), x ∈ Ico a b → ‖f' x‖ ≤ C
g : ℝ → E := fun x => f x - f a
hg : ContinuousOn g (Icc a b)
hg' : ∀ (x : ℝ), x ∈ Ico a b → HasDerivWithinAt g (f' x) (Ici x) x
B : ℝ → ℝ := fun x => C * (x - a)
⊢ ∀ (x : ℝ), x ∈ Icc a b → ‖f x - f a‖ ≤ C * (x - a)
have hB : ∀ x, HasDerivAt B C x := by
  intro x
  simpa using (hasDerivAt_const x C).mul ((hasDerivAt_id x).sub (hasDerivAt_const x a))
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.31247
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → E
a b : ℝ
f' : ℝ → E
C : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ (x : ℝ), x ∈ Ico a b → HasDerivWithinAt f (f' x) (Ici x) x
bound : ∀ (x : ℝ), x ∈ Ico a b → ‖f' x‖ ≤ C
g : ℝ → E := fun x => f x - f a
hg : ContinuousOn g (Icc a b)
hg' : ∀ (x : ℝ), x ∈ Ico a b → HasDerivWithinAt g (f' x) (Ici x) x
B : ℝ → ℝ := fun x => C * (x - a)
hB : ∀ (x : ℝ), HasDerivAt B C x
⊢ ‖g a‖ ≤ B a
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.31247
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → E
a b : ℝ
f' : ℝ → E
C : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ (x : ℝ), x ∈ Ico a b → HasDerivWithinAt f (f' x) (Ici x) x
bound : ∀ (x : ℝ), x ∈ Ico a b → ‖f' x‖ ≤ C
g : ℝ → E := fun x => f x - f a
hg : ContinuousOn g (Icc a b)
hg' : ∀ (x : ℝ), x ∈ Ico a b → HasDerivWithinAt g (f' x) (Ici x) x
B : ℝ → ℝ := fun x => C * (x - a)
hB : ∀ (x : ℝ), HasDerivAt B C x
⊢ ∀ (x : ℝ), x ∈ Icc a b → ‖f x - f a‖ ≤ C * (x - a)
convert image_norm_le_of_norm_deriv_right_le_deriv_boundary hg hg' _ hB bound
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.31247
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → E
a b : ℝ
f' : ℝ → E
C : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ (x : ℝ), x ∈ Ico a b → HasDerivWithinAt f (f' x) (Ici x) x
bound : ∀ (x : ℝ), x ∈ Ico a b → ‖f' x‖ ≤ C
g : ℝ → E := fun x => f x - f a
hg : ContinuousOn g (Icc a b)
hg' : ∀ (x : ℝ), x ∈ Ico a b → HasDerivWithinAt g (f' x) (Ici x) x
B : ℝ → ℝ := fun x => C * (x - a)
hB : ∀ (x : ℝ), HasDerivAt B C x
⊢ ‖f a - f a‖ ≤ C * (a - a)
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.31247
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → E
a b : ℝ
f' : ℝ → E
C : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ (x : ℝ), x ∈ Ico a b → HasDerivWithinAt f (f' x) (Ici x) x
bound : ∀ (x : ℝ), x ∈ Ico a b → ‖f' x‖ ≤ C
g : ℝ → E := fun x => f x - f a
hg : ContinuousOn g (Icc a b)
hg' : ∀ (x : ℝ), x ∈ Ico a b → HasDerivWithinAt g (f' x) (Ici x) x
B : ℝ → ℝ := fun x => C * (x - a)
hB : ∀ (x : ℝ), HasDerivAt B C x
⊢ ‖g a‖ ≤ B a
simp only
no goals
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.31247
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → E
a b : ℝ
f' : ℝ → E
C : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ (x : ℝ), x ∈ Ico a b → HasDerivWithinAt f (f' x) (Ici x) x
bound : ∀ (x : ℝ), x ∈ Ico a b → ‖f' x‖ ≤ C
g : ℝ → E := fun x => f x - f a
hg : ContinuousOn g (Icc a b)
hg' : ∀ (x : ℝ), x ∈ Ico a b → HasDerivWithinAt g (f' x) (Ici x) x
B : ℝ → ℝ := fun x => C * (x - a)
hB : ∀ (x : ℝ), HasDerivAt B C x
⊢ ‖f a - f a‖ ≤ C * (a - a)
rw [sub_self, norm_zero, sub_self, mul_zero]
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.31247
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → E
a b : ℝ
f' : ℝ → E
C : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ (x : ℝ), x ∈ Ico a b → HasDerivWithinAt f (f' x) (Ici x) x
bound : ∀ (x : ℝ), x ∈ Ico a b → ‖f' x‖ ≤ C
g : ℝ → E := fun x => f x - f a
hg : ContinuousOn g (Icc a b)
x : ℝ
hx : x ∈ Ico a b
⊢ HasDerivWithinAt g (f' x) (Ici x) x
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.31247
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → E
a b : ℝ
f' : ℝ → E
C : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ (x : ℝ), x ∈ Ico a b → HasDerivWithinAt f (f' x) (Ici x) x
bound : ∀ (x : ℝ), x ∈ Ico a b → ‖f' x‖ ≤ C
g : ℝ → E := fun x => f x - f a
hg : ContinuousOn g (Icc a b)
⊢ ∀ (x : ℝ), x ∈ Ico a b → HasDerivWithinAt g (f' x) (Ici x) x
intro x hx
no goals
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.31247
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → E
a b : ℝ
f' : ℝ → E
C : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ (x : ℝ), x ∈ Ico a b → HasDerivWithinAt f (f' x) (Ici x) x
bound : ∀ (x : ℝ), x ∈ Ico a b → ‖f' x‖ ≤ C
g : ℝ → E := fun x => f x - f a
hg : ContinuousOn g (Icc a b)
x : ℝ
hx : x ∈ Ico a b
⊢ HasDerivWithinAt g (f' x) (Ici x) x
simpa using (hf' x hx).sub (hasDerivWithinAt_const _ _ _)
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.31247
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → E
a b : ℝ
f' : ℝ → E
C : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ (x : ℝ), x ∈ Ico a b → HasDerivWithinAt f (f' x) (Ici x) x
bound : ∀ (x : ℝ), x ∈ Ico a b → ‖f' x‖ ≤ C
g : ℝ → E := fun x => f x - f a
hg : ContinuousOn g (Icc a b)
hg' : ∀ (x : ℝ), x ∈ Ico a b → HasDerivWithinAt g (f' x) (Ici x) x
B : ℝ → ℝ := fun x => C * (x - a)
x : ℝ
⊢ HasDerivAt B C x
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.31247
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → E
a b : ℝ
f' : ℝ → E
C : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ (x : ℝ), x ∈ Ico a b → HasDerivWithinAt f (f' x) (Ici x) x
bound : ∀ (x : ℝ), x ∈ Ico a b → ‖f' x‖ ≤ C
g : ℝ → E := fun x => f x - f a
hg : ContinuousOn g (Icc a b)
hg' : ∀ (x : ℝ), x ∈ Ico a b → HasDerivWithinAt g (f' x) (Ici x) x
B : ℝ → ℝ := fun x => C * (x - a)
⊢ ∀ (x : ℝ), HasDerivAt B C x
intro x
no goals
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.31247
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → E
a b : ℝ
f' : ℝ → E
C : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ (x : ℝ), x ∈ Ico a b → HasDerivWithinAt f (f' x) (Ici x) x
bound : ∀ (x : ℝ), x ∈ Ico a b → ‖f' x‖ ≤ C
g : ℝ → E := fun x => f x - f a
hg : ContinuousOn g (Icc a b)
hg' : ∀ (x : ℝ), x ∈ Ico a b → HasDerivWithinAt g (f' x) (Ici x) x
B : ℝ → ℝ := fun x => C * (x - a)
x : ℝ
⊢ HasDerivAt B C x
simpa using (hasDerivAt_const x C).mul ((hasDerivAt_id x).sub (hasDerivAt_const x a))