E : Type ?u.405058
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.405154
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
lt_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.405058
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.405154
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
lt_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_lt_neg_iff]
no goals
E : Type ?u.405058
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.405154
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
lt_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 lt_hf' x hx
no goals
E : Type ?u.405058
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.405154
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
lt_hf' : ∀ (x : ℝ), x ∈ interior D → deriv f x < C
x : ℝ
hx : x ∈ D
y : ℝ
hy : y ∈ D
hxy : x < y
hf'_gt : ∀ (x : ℝ), x ∈ interior D → -C < deriv (fun y => -f y) x
⊢ f y - f x < C * (y - x)
linarith [hD.mul_sub_lt_image_sub_of_lt_deriv hf.neg hf'.neg hf'_gt x hx y hy hxy]