E : Type ?u.408885
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.408981
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf' : DifferentiableOn ℝ f (interior D)
C : (fun x => ℝ) 1
le_hf' : ∀ (x : ℝ), x ∈ interior D → deriv f x ≤ C
x✝ : ℝ
hx✝ : x✝ ∈ D
y : ℝ
hy : y ∈ D
hxy : x✝ ≤ y
x : ℝ
hx : x ∈ interior D
⊢ deriv (fun y => f y) x ≤ C
E : Type ?u.408885
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.408981
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf' : DifferentiableOn ℝ f (interior D)
C : (fun x => ℝ) 1
le_hf' : ∀ (x : ℝ), x ∈ interior D → deriv f x ≤ C
x✝ : ℝ
hx✝ : x✝ ∈ D
y : ℝ
hy : y ∈ D
hxy : x✝ ≤ y
x : ℝ
hx : x ∈ interior D
⊢ -C ≤ deriv (fun y => -f y) x
rw [deriv.neg, neg_le_neg_iff]
no goals
E : Type ?u.408885
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.408981
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf' : DifferentiableOn ℝ f (interior D)
C : (fun x => ℝ) 1
le_hf' : ∀ (x : ℝ), x ∈ interior D → deriv f x ≤ C
x✝ : ℝ
hx✝ : x✝ ∈ D
y : ℝ
hy : y ∈ D
hxy : x✝ ≤ y
x : ℝ
hx : x ∈ interior D
⊢ deriv (fun y => f y) x ≤ C
exact le_hf' x hx
no goals
E : Type ?u.408885
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.408981
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf' : DifferentiableOn ℝ f (interior D)
C : (fun x => ℝ) 1
le_hf' : ∀ (x : ℝ), x ∈ interior D → deriv f x ≤ C
x : ℝ
hx : x ∈ D
y : ℝ
hy : y ∈ D
hxy : x ≤ y
hf'_ge : ∀ (x : ℝ), x ∈ interior D → -C ≤ deriv (fun y => -f y) x
⊢ f y - f x ≤ C * (y - x)
linarith [hD.mul_sub_le_image_sub_of_le_deriv hf.neg hf'.neg hf'_ge x hx y hy hxy]