Derivative at infinity of a real function

Main definitions

• derivAtTop f: the limit at +∞ of the right derivative of f : ℝ → ℝ, as an EReal. It is defined as a limsup, so that it is always defined.

Main statements

• MonotoneOn.tendsto_derivAtTop, ConvexOn.tendsto_derivAtTop: for a function with monotone right derivative (in particular a convex function), the right derivative tends to derivAtTop f.
• slope_le_derivAtTop, le_add_derivAtTop: for a convex function, slopes are bounded by derivAtTop f, hence f y ≤ f x + derivAtTop f * (y - x).

theorem MonotoneOn.exists_tendsto_atTop {ι : Type u_1} {α : Type u_2} [SemilatticeSup ι] [CompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] {x : ι} {f : ι → α} (hf : MonotoneOn f (Set.Ici x)) : ∃ (y : α), Filter.Tendsto f Filter.atTop (nhds y)

A function to a complete linear order which is monotone on [x, ∞) has a limit at atTop.

noncomputable def derivAtTop (f : ℝ → ℝ) : EReal

Limsup of the right derivative at infinity.

Equations

• derivAtTop f = Filter.limsup (fun (x : ℝ) => ↑(rightDeriv f x)) Filter.atTop

theorem derivAtTop_congr {f g : ℝ → ℝ} (h : f =ᶠ[Filter.atTop] g) : derivAtTop f = derivAtTop g

theorem derivAtTop_of_tendsto {f : ℝ → ℝ} {y : EReal} (h : Filter.Tendsto (fun (x : ℝ) => ↑(rightDeriv f x)) Filter.atTop (nhds y)) : derivAtTop f = y

theorem derivAtTop_of_tendsto_nhds {f : ℝ → ℝ} {y : ℝ} (h : Filter.Tendsto (rightDeriv f) Filter.atTop (nhds y)) : derivAtTop f = ↑y

theorem derivAtTop_of_tendsto_atTop {f : ℝ → ℝ} (h : Filter.Tendsto (rightDeriv f) Filter.atTop Filter.atTop) : derivAtTop f = ⊤

@[simp]

theorem derivAtTop_zero : derivAtTop 0 = 0

@[simp]

theorem derivAtTop_const (c : ℝ) : (derivAtTop fun (x : ℝ) => c) = 0

@[simp]

theorem derivAtTop_id : derivAtTop id = 1

@[simp]

theorem derivAtTop_id' : (derivAtTop fun (x : ℝ) => x) = 1

theorem MonotoneOn.tendsto_derivAtTop {f : ℝ → ℝ} (hf : MonotoneOn (rightDeriv f) (Set.Ioi 0)) : Filter.Tendsto (fun (x : ℝ) => ↑(rightDeriv f x)) Filter.atTop (nhds (derivAtTop f))

theorem ConvexOn.tendsto_derivAtTop {f : ℝ → ℝ} (hf : ConvexOn ℝ (Set.Ici 0) f) : Filter.Tendsto (fun (x : ℝ) => ↑(rightDeriv f x)) Filter.atTop (nhds (derivAtTop f))

theorem MonotoneOn.derivAtTop_eq_iff {f : ℝ → ℝ} {y : EReal} (hf : MonotoneOn (rightDeriv f) (Set.Ioi 0)) : derivAtTop f = y ↔ Filter.Tendsto (fun (x : ℝ) => ↑(rightDeriv f x)) Filter.atTop (nhds y)

theorem ConvexOn.derivAtTop_eq_iff {f : ℝ → ℝ} {y : EReal} (hf : ConvexOn ℝ (Set.Ici 0) f) : derivAtTop f = y ↔ Filter.Tendsto (fun (x : ℝ) => ↑(rightDeriv f x)) Filter.atTop (nhds y)

theorem MonotoneOn.derivAtTop_eq_top_iff {f : ℝ → ℝ} (hf : MonotoneOn (rightDeriv f) (Set.Ioi 0)) : derivAtTop f = ⊤ ↔ Filter.Tendsto (rightDeriv f) Filter.atTop Filter.atTop

theorem ConvexOn.derivAtTop_eq_top_iff {f : ℝ → ℝ} (hf : ConvexOn ℝ (Set.Ici 0) f) : derivAtTop f = ⊤ ↔ Filter.Tendsto (rightDeriv f) Filter.atTop Filter.atTop

theorem MonotoneOn.derivAtTop_ne_bot {f : ℝ → ℝ} (hf : MonotoneOn (rightDeriv f) (Set.Ioi 0)) : derivAtTop f ≠ ⊥

theorem ConvexOn.derivAtTop_ne_bot {f : ℝ → ℝ} (hf : ConvexOn ℝ (Set.Ici 0) f) : derivAtTop f ≠ ⊥

theorem MonotoneOn.tendsto_toReal_derivAtTop {f : ℝ → ℝ} (hf : MonotoneOn (rightDeriv f) (Set.Ioi 0)) (h_top : derivAtTop f ≠ ⊤) : Filter.Tendsto (rightDeriv f) Filter.atTop (nhds (derivAtTop f).toReal)

theorem ConvexOn.tendsto_toReal_derivAtTop {f : ℝ → ℝ} (hf : ConvexOn ℝ (Set.Ici 0) f) (h_top : derivAtTop f ≠ ⊤) : Filter.Tendsto (rightDeriv f) Filter.atTop (nhds (derivAtTop f).toReal)

theorem derivAtTop_add' {f g : ℝ → ℝ} (hf_cvx : ConvexOn ℝ (Set.Ici 0) f) (hg_cvx : ConvexOn ℝ (Set.Ici 0) g) : derivAtTop (f + g) = derivAtTop f + derivAtTop g

theorem derivAtTop_add {f g : ℝ → ℝ} (hf_cvx : ConvexOn ℝ (Set.Ici 0) f) (hg_cvx : ConvexOn ℝ (Set.Ici 0) g) : (derivAtTop fun (x : ℝ) => f x + g x) = derivAtTop f + derivAtTop g

theorem derivAtTop_add_const {f : ℝ → ℝ} (hf_cvx : ConvexOn ℝ (Set.Ici 0) f) (c : ℝ) : (derivAtTop fun (x : ℝ) => f x + c) = derivAtTop f

theorem derivAtTop_const_add {f : ℝ → ℝ} (hf_cvx : ConvexOn ℝ (Set.Ici 0) f) (c : ℝ) : (derivAtTop fun (x : ℝ) => c + f x) = derivAtTop f

theorem derivAtTop_sub_const {f : ℝ → ℝ} (hf_cvx : ConvexOn ℝ (Set.Ici 0) f) (c : ℝ) : (derivAtTop fun (x : ℝ) => f x - c) = derivAtTop f

theorem derivAtTop_const_mul {f : ℝ → ℝ} (hf_cvx : ConvexOn ℝ (Set.Ici 0) f) {c : ℝ} (hc : c ≠ 0) : (derivAtTop fun (x : ℝ) => c * f x) = ↑c * derivAtTop f

theorem slope_le_rightDeriv {f : ℝ → ℝ} (h_cvx : ConvexOn ℝ (Set.Ici 0) f) {x y : ℝ} (hx : 0 ≤ x) (hxy : x < y) : (f y - f x) / (y - x) ≤ rightDeriv f y

theorem rightDeriv_le_toReal_derivAtTop {f : ℝ → ℝ} {x : ℝ} (h_cvx : ConvexOn ℝ (Set.Ici 0) f) (h : derivAtTop f ≠ ⊤) (hx : 0 < x) : rightDeriv f x ≤ (derivAtTop f).toReal

theorem rightDeriv_le_derivAtTop {f : ℝ → ℝ} {x : ℝ} (h_cvx : ConvexOn ℝ (Set.Ici 0) f) (hx : 0 < x) : ↑(rightDeriv f x) ≤ derivAtTop f

theorem slope_le_derivAtTop {f : ℝ → ℝ} (h_cvx : ConvexOn ℝ (Set.Ici 0) f) (h : derivAtTop f ≠ ⊤) {x y : ℝ} (hx : 0 ≤ x) (hxy : x < y) : (f y - f x) / (y - x) ≤ (derivAtTop f).toReal

theorem le_add_derivAtTop {f : ℝ → ℝ} (h_cvx : ConvexOn ℝ (Set.Ici 0) f) (h : derivAtTop f ≠ ⊤) {x y : ℝ} (hy : 0 ≤ y) (hyx : y ≤ x) : f x ≤ f y + (derivAtTop f).toReal * (x - y)

theorem le_add_derivAtTop'' {f : ℝ → ℝ} (h_cvx : ConvexOn ℝ (Set.Ici 0) f) (h : derivAtTop f ≠ ⊤) {x y : ℝ} (hx : 0 ≤ x) (hy : 0 ≤ y) : f (x + y) ≤ f x + (derivAtTop f).toReal * y

theorem le_add_derivAtTop' {f : ℝ → ℝ} (h_cvx : ConvexOn ℝ (Set.Ici 0) f) (h : derivAtTop f ≠ ⊤) {x u : ℝ} (hx : 0 ≤ x) (hu : 0 ≤ u) (hu' : u ≤ 1) : f x ≤ f (x * u) + (derivAtTop f).toReal * x * (1 - u)