Documentation

TestingLowerBounds.DerivAtTop

DerivAtTop #

Main definitions #

FooBar

Main statements #

fooBar_unique

Notation #

Implementation details #

theorem EReal.tendsto_of_monotone {ι : Type u_1} [Preorder ι] {f : ι → EReal} (hf : Monotone f) :

∃ (y : EReal), Filter.Tendsto f Filter.atTop (nhds y)

theorem EReal.tendsto_of_monotoneOn {ι : Type u_1} [SemilatticeSup ι] [Nonempty ι] {x : ι} {f : ι → EReal} (hf : MonotoneOn f (Set.Ici x)) :

∃ (y : EReal), Filter.Tendsto f Filter.atTop (nhds y)

theorem Real.monotone_toEReal :

Monotone Real.toEReal

theorem ite_bot_ae_eq_atTop (f : ℝ → EReal) :

(fun (x : ℝ) => if 1 ≤ x then f x else ⊥) =ᶠ[Filter.atTop] f

theorem MonotoneOn.monotone_ite_bot {f : ℝ → ℝ} (hf : MonotoneOn (rightDeriv f) (Set.Ioi 0)) :

Monotone fun (x : ℝ) => if 1 ≤ x then ↑(rightDeriv f x) else ⊥

noncomputable def derivAtTop (f : ℝ → ℝ) :

Limsup of the right derivative at infinity.

Equations

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

Instances For

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

derivAtTop f = derivAtTop g

theorem derivAtTop_congr_nonneg {f : ℝ → ℝ} {g : ℝ → ℝ} (h : ∀ (x : ℝ), 0 ≤ x → f x = g x) :

derivAtTop f = derivAtTop g

theorem derivAtTop_eq_limsup_extendBotLtOne {f : ℝ → ℝ} :

derivAtTop f = Filter.limsup (fun (x : ℝ) => if 1 ≤ x then ↑(rightDeriv f x) else ⊥) Filter.atTop

theorem tendsto_extendBotLtOne_rightDeriv_iff {f : ℝ → ℝ} {y : EReal} :

Filter.Tendsto (fun (x : ℝ) => if 1 ≤ x then ↑(rightDeriv f x) else ⊥) Filter.atTop (nhds y) ↔ Filter.Tendsto (fun (x : ℝ) => ↑(rightDeriv f x)) Filter.atTop (nhds y)

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)

theorem toReal_le_add_derivAtTop {f : ℝ → ℝ} (hf_cvx : ConvexOn ℝ (Set.Ici 0) f) {a : ENNReal} {b : ENNReal} (ha : a ≠ ⊤) (hb : b ≠ ⊤) :

↑(f (a + b).toReal) ≤ ↑(f a.toReal) + derivAtTop f * ↑b