Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

[Merged by Bors] - chore: replace right_deriv by rightDeriv in lemma names #21076

Closed
wants to merge 1 commit into from
Closed

[Merged by Bors] - chore: replace right_deriv by rightDeriv in lemma names #21076

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
40 changes: 32 additions & 8 deletions Mathlib/Analysis/Convex/Deriv.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -395,11 +395,14 @@ lemma le_slope_of_hasDerivWithinAt_Ioi (hfc : ConvexOn ℝ S f)
exact hfc.1.ordConnected.out hx hy ⟨ht'.le, ht.le⟩

/-- Reformulation of `ConvexOn.le_slope_of_hasDerivWithinAt_Ioi` using `derivWithin`. -/
lemma right_deriv_le_slope (hfc : ConvexOn ℝ S f) (hx : x ∈ S) (hy : y ∈ S) (hxy : x < y)
lemma rightDeriv_le_slope (hfc : ConvexOn ℝ S f) (hx : x ∈ S) (hy : y ∈ S) (hxy : x < y)
(hfd : DifferentiableWithinAt ℝ f (Ioi x) x) :
derivWithin f (Ioi x) x ≤ slope f x y :=
le_slope_of_hasDerivWithinAt_Ioi hfc hx hy hxy hfd.hasDerivWithinAt

@[deprecated (since := "2025-01-26")]
alias right_deriv_le_slope := rightDeriv_le_slope

/-- If `f : ℝ → ℝ` is convex on `S` and differentiable within `S` at `x`, then the slope of any
secant line with left endpoint at `x` is bounded below by the derivative of `f` within `S` at `x`.

Expand Down Expand Up @@ -449,11 +452,14 @@ lemma slope_le_of_hasDerivWithinAt_Iio (hfc : ConvexOn ℝ S f)
exact hfc.1.ordConnected.out hx hy ⟨ht.le, ht'.le⟩

/-- Reformulation of `ConvexOn.slope_le_of_hasDerivWithinAt_Iio` using `derivWithin`. -/
lemma slope_le_left_deriv (hfc : ConvexOn ℝ S f) (hx : x ∈ S) (hy : y ∈ S) (hxy : x < y)
lemma slope_le_leftDeriv (hfc : ConvexOn ℝ S f) (hx : x ∈ S) (hy : y ∈ S) (hxy : x < y)
(hfd : DifferentiableWithinAt ℝ f (Iio y) y) :
slope f x y ≤ derivWithin f (Iio y) y :=
hfc.slope_le_of_hasDerivWithinAt_Iio hx hy hxy hfd.hasDerivWithinAt

@[deprecated (since := "2025-01-26")]
alias slope_le_left_deriv := slope_le_leftDeriv

/-- If `f : ℝ → ℝ` is convex on `S` and differentiable within `S` at `y`, then the slope of any
secant line with right endpoint at `y` is bounded above by the derivative of `f` within `S` at `y`.

Expand Down Expand Up @@ -531,11 +537,14 @@ lemma lt_slope_of_hasDerivWithinAt_Ioi (hfc : StrictConvexOn ℝ S f)
simp only [← slope_def_field] at this
exact (hfc.convexOn.le_slope_of_hasDerivWithinAt_Ioi hx hu hxu hf').trans_lt this

lemma right_deriv_lt_slope (hfc : StrictConvexOn ℝ S f) (hx : x ∈ S) (hy : y ∈ S) (hxy : x < y)
lemma rightDeriv_lt_slope (hfc : StrictConvexOn ℝ S f) (hx : x ∈ S) (hy : y ∈ S) (hxy : x < y)
(hfd : DifferentiableWithinAt ℝ f (Ioi x) x) :
derivWithin f (Ioi x) x < slope f x y :=
hfc.lt_slope_of_hasDerivWithinAt_Ioi hx hy hxy hfd.hasDerivWithinAt

@[deprecated (since := "2025-01-26")]
alias right_deriv_lt_slope := rightDeriv_lt_slope

/-- If `f : ℝ → ℝ` is strictly convex on `S` and differentiable within `S` at `x ∈ S`, then the
slope of any secant line with left endpoint at `x` is strictly greater than the derivative of `f`
within `S` at `x`.
Expand Down Expand Up @@ -583,11 +592,14 @@ lemma slope_lt_of_hasDerivWithinAt_Iio (hfc : StrictConvexOn ℝ S f)
simp_rw [← slope_def_field, slope_comm _ y] at this
exact this.trans_le <| hfc.convexOn.slope_le_of_hasDerivWithinAt_Iio hu hy huy hf'

lemma slope_lt_left_deriv (hfc : StrictConvexOn ℝ S f) (hx : x ∈ S) (hy : y ∈ S) (hxy : x < y)
lemma slope_lt_leftDeriv (hfc : StrictConvexOn ℝ S f) (hx : x ∈ S) (hy : y ∈ S) (hxy : x < y)
(hfd : DifferentiableWithinAt ℝ f (Iio y) y) :
slope f x y < derivWithin f (Iio y) y :=
hfc.slope_lt_of_hasDerivWithinAt_Iio hx hy hxy hfd.hasDerivWithinAt

@[deprecated (since := "2025-01-26")]
alias slope_lt_left_deriv := slope_lt_leftDeriv

/-- If `f : ℝ → ℝ` is strictly convex on `S` and differentiable within `S` at `y ∈ S`, then the
slope of any secant line with right endpoint at `y` is strictly less than the derivative of `f`
within `S` at `y`.
Expand Down Expand Up @@ -657,11 +669,14 @@ lemma slope_le_of_hasDerivWithinAt_Ioi (hfc : ConcaveOn ℝ S f)
simpa only [Pi.neg_def, slope_neg, neg_neg] using
neg_le_neg (hfc.neg.le_slope_of_hasDerivWithinAt_Ioi hx hy hxy hf'.neg)

lemma slope_le_right_deriv (hfc : ConcaveOn ℝ S f) (hx : x ∈ S) (hy : y ∈ S) (hxy : x < y)
lemma slope_le_rightDeriv (hfc : ConcaveOn ℝ S f) (hx : x ∈ S) (hy : y ∈ S) (hxy : x < y)
(hfd : DifferentiableWithinAt ℝ f (Ioi x) x) :
slope f x y ≤ derivWithin f (Ioi x) x :=
hfc.slope_le_of_hasDerivWithinAt_Ioi hx hy hxy hfd.hasDerivWithinAt

@[deprecated (since := "2025-01-26")]
alias slope_le_right_deriv := slope_le_rightDeriv

lemma slope_le_of_hasDerivWithinAt (hfc : ConcaveOn ℝ S f) (hx : x ∈ S) (hy : y ∈ S) (hxy : x < y)
(hfd : HasDerivWithinAt f f' S x) :
slope f x y ≤ f' :=
Expand Down Expand Up @@ -696,11 +711,14 @@ lemma le_slope_of_hasDerivWithinAt_Iio (hfc : ConcaveOn ℝ S f)
simpa only [neg_neg, Pi.neg_def, slope_neg] using
neg_le_neg (hfc.neg.slope_le_of_hasDerivWithinAt_Iio hx hy hxy hf'.neg)

lemma left_deriv_le_slope (hfc : ConcaveOn ℝ S f) (hx : x ∈ S) (hy : y ∈ S) (hxy : x < y)
lemma leftDeriv_le_slope (hfc : ConcaveOn ℝ S f) (hx : x ∈ S) (hy : y ∈ S) (hxy : x < y)
(hfd : DifferentiableWithinAt ℝ f (Iio y) y) :
derivWithin f (Iio y) y ≤ slope f x y :=
hfc.le_slope_of_hasDerivWithinAt_Iio hx hy hxy hfd.hasDerivWithinAt

@[deprecated (since := "2025-01-26")]
alias left_deriv_le_slope := leftDeriv_le_slope

lemma le_slope_of_hasDerivWithinAt (hfc : ConcaveOn ℝ S f) (hx : x ∈ S) (hy : y ∈ S) (hxy : x < y)
(hf' : HasDerivWithinAt f f' S y) :
f' ≤ slope f x y :=
Expand Down Expand Up @@ -757,11 +775,14 @@ lemma slope_lt_of_hasDerivWithinAt_Ioi (hfc : StrictConcaveOn ℝ S f)
simpa only [Pi.neg_def, slope_neg, neg_neg] using
neg_lt_neg (hfc.neg.lt_slope_of_hasDerivWithinAt_Ioi hx hy hxy hf'.neg)

lemma slope_lt_right_deriv (hfc : StrictConcaveOn ℝ S f) (hx : x ∈ S) (hy : y ∈ S) (hxy : x < y)
lemma slope_lt_rightDeriv (hfc : StrictConcaveOn ℝ S f) (hx : x ∈ S) (hy : y ∈ S) (hxy : x < y)
(hfd : DifferentiableWithinAt ℝ f (Ioi x) x) :
slope f x y < derivWithin f (Ioi x) x :=
hfc.slope_lt_of_hasDerivWithinAt_Ioi hx hy hxy hfd.hasDerivWithinAt

@[deprecated (since := "2025-01-26")]
alias slope_lt_right_deriv := slope_lt_rightDeriv

lemma slope_lt_of_hasDerivWithinAt (hfc : StrictConcaveOn ℝ S f)
(hx : x ∈ S) (hy : y ∈ S) (hxy : x < y) (hfd : HasDerivWithinAt f f' S x) :
slope f x y < f' := by
Expand Down Expand Up @@ -797,11 +818,14 @@ lemma lt_slope_of_hasDerivWithinAt_Iio (hfc : StrictConcaveOn ℝ S f)
simpa only [Pi.neg_def, slope_neg, neg_neg] using
neg_lt_neg (hfc.neg.slope_lt_of_hasDerivWithinAt_Iio hx hy hxy hf'.neg)

lemma left_deriv_lt_slope (hfc : StrictConcaveOn ℝ S f) (hx : x ∈ S) (hy : y ∈ S) (hxy : x < y)
lemma leftDeriv_lt_slope (hfc : StrictConcaveOn ℝ S f) (hx : x ∈ S) (hy : y ∈ S) (hxy : x < y)
(hfd : DifferentiableWithinAt ℝ f (Iio y) y) :
derivWithin f (Iio y) y < slope f x y :=
hfc.lt_slope_of_hasDerivWithinAt_Iio hx hy hxy hfd.hasDerivWithinAt

@[deprecated (since := "2025-01-26")]
alias left_deriv_lt_slope := leftDeriv_lt_slope

lemma lt_slope_of_hasDerivWithinAt (hfc : StrictConcaveOn ℝ S f)
(hx : x ∈ S) (hy : y ∈ S) (hxy : x < y) (hf' : HasDerivWithinAt f f' S y) :
f' < slope f x y := by
Expand Down
Loading