theorem ConvexOn.comp_neg {𝕜 : Type u_1} {F : Type u_2} {β : Type u_3} [LinearOrderedField 𝕜] [AddCommGroup F] [OrderedAddCommMonoid β] [Module 𝕜 F] [SMul 𝕜 β] {f : F → β} {s : Set F} (hf : ConvexOn 𝕜 s f) : ConvexOn 𝕜 (-s) fun (x : F) => f (-x)

theorem ConvexOn.comp_neg_iff {𝕜 : Type u_1} {F : Type u_2} {β : Type u_3} [LinearOrderedField 𝕜] [AddCommGroup F] [OrderedAddCommMonoid β] [Module 𝕜 F] [SMul 𝕜 β] {f : F → β} {s : Set F} : (ConvexOn 𝕜 (-s) fun (x : F) => f (-x)) ↔ ConvexOn 𝕜 s f

theorem ConvexOn.const_mul_id (c : ℝ) : ConvexOn ℝ Set.univ fun (x : ℝ) => c * x

noncomputable def rightDeriv (f : ℝ → ℝ) : ℝ → ℝ

The right derivative of a real function.

Equations

• rightDeriv f x = derivWithin f (Set.Ioi x) x

theorem rightDeriv_def (f : ℝ → ℝ) (x : ℝ) : rightDeriv f x = derivWithin f (Set.Ioi x) x

noncomputable def leftDeriv (f : ℝ → ℝ) : ℝ → ℝ

The left derivative of a real function.

Equations

• leftDeriv f x = derivWithin f (Set.Iio x) x

theorem leftDeriv_def (f : ℝ → ℝ) (x : ℝ) : leftDeriv f x = derivWithin f (Set.Iio x) x

theorem rightDeriv_of_not_differentiableWithinAt {f : ℝ → ℝ} {x : ℝ} (hf : ¬DifferentiableWithinAt ℝ f (Set.Ioi x) x) : rightDeriv f x = 0

theorem leftDeriv_of_not_differentiableWithinAt {f : ℝ → ℝ} {x : ℝ} (hf : ¬DifferentiableWithinAt ℝ f (Set.Iio x) x) : leftDeriv f x = 0

theorem rightDeriv_eq_leftDeriv_apply (f : ℝ → ℝ) (x : ℝ) : rightDeriv f x = -leftDeriv (fun (x : ℝ) => f (-x)) (-x)

theorem rightDeriv_eq_leftDeriv (f : ℝ → ℝ) : rightDeriv f = fun (x : ℝ) => -leftDeriv (fun (y : ℝ) => f (-y)) (-x)

theorem leftDeriv_eq_rightDeriv_apply (f : ℝ → ℝ) (x : ℝ) : leftDeriv f x = -rightDeriv (fun (y : ℝ) => f (-y)) (-x)

theorem leftDeriv_eq_rightDeriv (f : ℝ → ℝ) : leftDeriv f = fun (x : ℝ) => -rightDeriv (fun (y : ℝ) => f (-y)) (-x)

theorem Filter.EventuallyEq.derivWithin_eq_nhds {𝕜 : Type u_1} {F : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f₁ : 𝕜 → F} {f : 𝕜 → F} {x : 𝕜} {s : Set 𝕜} (h : f₁ =ᶠ[nhds x] f) : derivWithin f₁ s x = derivWithin f s x

theorem Filter.EventuallyEq.rightDeriv_eq_nhds {f : ℝ → ℝ} {x : ℝ} {g : ℝ → ℝ} (h : f =ᶠ[nhds x] g) : rightDeriv f x = rightDeriv g x

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

theorem rightDeriv_of_hasDerivAt {f : ℝ → ℝ} {f' : ℝ} {x : ℝ} (h : HasDerivAt f f' x) : rightDeriv f x = f'

theorem leftDeriv_of_hasDerivAt {f : ℝ → ℝ} {f' : ℝ} {x : ℝ} (h : HasDerivAt f f' x) : leftDeriv f x = f'

@[simp]

theorem rightDeriv_zero : rightDeriv 0 = 0

@[simp]

theorem rightDeriv_const (c : ℝ) : (rightDeriv fun (x : ℝ) => c) = 0

@[simp]

theorem leftDeriv_const (c : ℝ) : (leftDeriv fun (x : ℝ) => c) = 0

@[simp]

theorem rightDeriv_const_mul (a : ℝ) {f : ℝ → ℝ} : (rightDeriv fun (x : ℝ) => a * f x) = fun (x : ℝ) => a * rightDeriv f x

@[simp]

theorem leftDeriv_const_mul (a : ℝ) {f : ℝ → ℝ} : (leftDeriv fun (x : ℝ) => a * f x) = fun (x : ℝ) => a * leftDeriv f x

@[simp]

theorem rightDeriv_neg {f : ℝ → ℝ} : (rightDeriv fun (x : ℝ) => -f x) = fun (x : ℝ) => -rightDeriv f x

@[simp]

theorem leftDeriv_neg {f : ℝ → ℝ} : (leftDeriv fun (x : ℝ) => -f x) = fun (x : ℝ) => -leftDeriv f x

@[simp]

theorem rightDeriv_id : rightDeriv id = fun (x : ℝ) => 1

@[simp]

theorem rightDeriv_id' : (rightDeriv fun (x : ℝ) => x) = fun (x : ℝ) => 1

@[simp]

theorem leftDeriv_id : leftDeriv id = fun (x : ℝ) => 1

@[simp]

theorem leftDeriv_id' : (leftDeriv fun (x : ℝ) => x) = fun (x : ℝ) => 1

theorem rightDeriv_add_apply {f : ℝ → ℝ} {g : ℝ → ℝ} {x : ℝ} (hf : DifferentiableWithinAt ℝ f (Set.Ioi x) x) (hg : DifferentiableWithinAt ℝ g (Set.Ioi x) x) : rightDeriv (f + g) x = rightDeriv f x + rightDeriv g x

theorem rightDeriv_add_apply' {f : ℝ → ℝ} {g : ℝ → ℝ} {x : ℝ} (hf : DifferentiableWithinAt ℝ f (Set.Ioi x) x) (hg : DifferentiableWithinAt ℝ g (Set.Ioi x) x) : rightDeriv (fun (x : ℝ) => f x + g x) x = rightDeriv f x + rightDeriv g x

theorem rightDeriv_add {f : ℝ → ℝ} {g : ℝ → ℝ} (hf : ∀ (x : ℝ), DifferentiableWithinAt ℝ f (Set.Ioi x) x) (hg : ∀ (x : ℝ), DifferentiableWithinAt ℝ g (Set.Ioi x) x) : rightDeriv (f + g) = fun (x : ℝ) => rightDeriv f x + rightDeriv g x

theorem rightDeriv_add' {f : ℝ → ℝ} {g : ℝ → ℝ} (hf : ∀ (x : ℝ), DifferentiableWithinAt ℝ f (Set.Ioi x) x) (hg : ∀ (x : ℝ), DifferentiableWithinAt ℝ g (Set.Ioi x) x) : (rightDeriv fun (x : ℝ) => f x + g x) = fun (x : ℝ) => rightDeriv f x + rightDeriv g x

theorem leftDeriv_add_apply {f : ℝ → ℝ} {g : ℝ → ℝ} {x : ℝ} (hf : DifferentiableWithinAt ℝ f (Set.Iio x) x) (hg : DifferentiableWithinAt ℝ g (Set.Iio x) x) : leftDeriv (f + g) x = leftDeriv f x + leftDeriv g x

theorem leftDeriv_add_apply' {f : ℝ → ℝ} {g : ℝ → ℝ} {x : ℝ} (hf : DifferentiableWithinAt ℝ f (Set.Iio x) x) (hg : DifferentiableWithinAt ℝ g (Set.Iio x) x) : leftDeriv (fun (x : ℝ) => f x + g x) x = leftDeriv f x + leftDeriv g x

theorem leftDeriv_add {f : ℝ → ℝ} {g : ℝ → ℝ} (hf : ∀ (x : ℝ), DifferentiableWithinAt ℝ f (Set.Iio x) x) (hg : ∀ (x : ℝ), DifferentiableWithinAt ℝ g (Set.Iio x) x) : leftDeriv (f + g) = fun (x : ℝ) => leftDeriv f x + leftDeriv g x

theorem leftDeriv_add' {f : ℝ → ℝ} {g : ℝ → ℝ} (hf : ∀ (x : ℝ), DifferentiableWithinAt ℝ f (Set.Iio x) x) (hg : ∀ (x : ℝ), DifferentiableWithinAt ℝ g (Set.Iio x) x) : (leftDeriv fun (x : ℝ) => f x + g x) = fun (x : ℝ) => leftDeriv f x + leftDeriv g x

theorem rightDeriv_add_const_apply {f : ℝ → ℝ} {x : ℝ} (hf : DifferentiableWithinAt ℝ f (Set.Ioi x) x) (c : ℝ) : rightDeriv (fun (x : ℝ) => f x + c) x = rightDeriv f x

theorem rightDeriv_add_const {f : ℝ → ℝ} (hf : ∀ (x : ℝ), DifferentiableWithinAt ℝ f (Set.Ioi x) x) (c : ℝ) : (rightDeriv fun (x : ℝ) => f x + c) = rightDeriv f

theorem leftDeriv_add_const_apply {f : ℝ → ℝ} {x : ℝ} (hf : DifferentiableWithinAt ℝ f (Set.Iio x) x) (c : ℝ) : leftDeriv (fun (x : ℝ) => f x + c) x = leftDeriv f x

theorem leftDeriv_add_const {f : ℝ → ℝ} (hf : ∀ (x : ℝ), DifferentiableWithinAt ℝ f (Set.Iio x) x) (c : ℝ) : (leftDeriv fun (x : ℝ) => f x + c) = leftDeriv f

theorem rightDeriv_add_linear_apply {f : ℝ → ℝ} {x : ℝ} (hf : DifferentiableWithinAt ℝ f (Set.Ioi x) x) (a : ℝ) : rightDeriv (fun (x : ℝ) => f x + a * x) x = rightDeriv f x + a

theorem rightDeriv_add_linear {f : ℝ → ℝ} (hf : ∀ (x : ℝ), DifferentiableWithinAt ℝ f (Set.Ioi x) x) (a : ℝ) : (rightDeriv fun (x : ℝ) => f x + a * x) = rightDeriv f + fun (x : ℝ) => a

theorem leftDeriv_add_linear_apply {f : ℝ → ℝ} {x : ℝ} (hf : DifferentiableWithinAt ℝ f (Set.Iio x) x) (a : ℝ) : leftDeriv (fun (x : ℝ) => f x + a * x) x = leftDeriv f x + a

theorem leftDeriv_add_linear {f : ℝ → ℝ} (hf : ∀ (x : ℝ), DifferentiableWithinAt ℝ f (Set.Iio x) x) (a : ℝ) : (leftDeriv fun (x : ℝ) => f x + a * x) = leftDeriv f + fun (x : ℝ) => a

theorem ConvexOn.bddBelow_slope_Ioi {f : ℝ → ℝ} (hfc : ConvexOn ℝ Set.univ f) (x : ℝ) : BddBelow (slope f x '' Set.Ioi x)

theorem ConvexOn.bddBelow_slope_Ioi' {f : ℝ → ℝ} (hfc : ConvexOn ℝ (Set.Ici 0) f) (x : ℝ) (hx : 0 < x) : BddBelow (slope f x '' Set.Ioi x)

theorem ConvexOn.bddAbove_slope_Iio {f : ℝ → ℝ} (hfc : ConvexOn ℝ Set.univ f) (x : ℝ) : BddAbove (slope f x '' Set.Iio x)

theorem ConvexOn.monotoneOn_slope_gt {f : ℝ → ℝ} {s : Set ℝ} (hfc : ConvexOn ℝ s f) {x : ℝ} (hxs : x ∈ interior s) : MonotoneOn (slope f x) {y : ℝ | y ∈ s ∧ x < y}

theorem ConvexOn.monotoneOn_slope_lt {f : ℝ → ℝ} {s : Set ℝ} (hfc : ConvexOn ℝ s f) {x : ℝ} (hxs : x ∈ interior s) : MonotoneOn (slope f x) {y : ℝ | y ∈ s ∧ y < x}

theorem ConvexOn.bddBelow_slope_Ioi_of_mem_interior {f : ℝ → ℝ} {s : Set ℝ} (hfc : ConvexOn ℝ s f) {x : ℝ} (hxs : x ∈ interior s) : BddBelow (slope f x '' {y : ℝ | y ∈ s ∧ x < y})

theorem ConvexOn.bddAbove_slope_Iio_of_mem_interior {f : ℝ → ℝ} {s : Set ℝ} (hfc : ConvexOn ℝ s f) {x : ℝ} (hxs : x ∈ interior s) : BddAbove (slope f x '' {y : ℝ | y ∈ s ∧ y < x})

theorem ConvexOn.hasRightDerivAt_of_mem_interior {f : ℝ → ℝ} {s : Set ℝ} {x : ℝ} (hfc : ConvexOn ℝ s f) (hxs : x ∈ interior s) : HasDerivWithinAt f (sInf (slope f x '' {y : ℝ | y ∈ s ∧ x < y})) (Set.Ioi x) x

theorem ConvexOn.differentiableWithinAt_Ioi_of_mem_interior {f : ℝ → ℝ} {s : Set ℝ} {x : ℝ} (hfc : ConvexOn ℝ s f) (hxs : x ∈ interior s) : DifferentiableWithinAt ℝ f (Set.Ioi x) x

theorem ConvexOn.hadDerivWithinAt_rightDeriv_of_mem_interior {f : ℝ → ℝ} {s : Set ℝ} {x : ℝ} (hfc : ConvexOn ℝ s f) (hxs : x ∈ interior s) : HasDerivWithinAt f (rightDeriv f x) (Set.Ioi x) x

theorem ConvexOn.rightDeriv_eq_sInf_slope_of_mem_interior {f : ℝ → ℝ} {s : Set ℝ} {x : ℝ} (hfc : ConvexOn ℝ s f) (hxs : x ∈ interior s) : rightDeriv f x = sInf (slope f x '' {y : ℝ | y ∈ s ∧ x < y})

theorem ConvexOn.rightDeriv_le_slope {f : ℝ → ℝ} {s : Set ℝ} {x : ℝ} (hfc : ConvexOn ℝ s f) {y : ℝ} (hxs : x ∈ interior s) (hys : y ∈ s) (hxy : x < y) : rightDeriv f x ≤ slope f x y

theorem ConvexOn.hasLeftDerivAt_of_mem_interior {f : ℝ → ℝ} {s : Set ℝ} {x : ℝ} (hfc : ConvexOn ℝ s f) (hxs : x ∈ interior s) : HasDerivWithinAt f (sSup (slope f x '' {y : ℝ | y ∈ s ∧ y < x})) (Set.Iio x) x

theorem ConvexOn.differentiableWithinAt_Iio_of_mem_interior {f : ℝ → ℝ} {s : Set ℝ} {x : ℝ} (hfc : ConvexOn ℝ s f) (hxs : x ∈ interior s) : DifferentiableWithinAt ℝ f (Set.Iio x) x

theorem ConvexOn.hadDerivWithinAt_leftDeriv_of_mem_interior {f : ℝ → ℝ} {s : Set ℝ} {x : ℝ} (hfc : ConvexOn ℝ s f) (hxs : x ∈ interior s) : HasDerivWithinAt f (leftDeriv f x) (Set.Iio x) x

theorem ConvexOn.leftDeriv_eq_sSup_slope_of_mem_interior {f : ℝ → ℝ} {s : Set ℝ} {x : ℝ} (hfc : ConvexOn ℝ s f) (hxs : x ∈ interior s) : leftDeriv f x = sSup (slope f x '' {y : ℝ | y ∈ s ∧ y < x})

theorem ConvexOn.slope_le_leftDeriv {f : ℝ → ℝ} {s : Set ℝ} {x : ℝ} (hfc : ConvexOn ℝ s f) {y : ℝ} (hxs : x ∈ interior s) (hys : y ∈ s) (hxy : y < x) : slope f x y ≤ leftDeriv f x

theorem ConvexOn.leftDeriv_le_rightDeriv_of_mem_interior {f : ℝ → ℝ} {s : Set ℝ} {x : ℝ} (hfc : ConvexOn ℝ s f) (hxs : x ∈ interior s) : leftDeriv f x ≤ rightDeriv f x

theorem ConvexOn.hasRightDerivAt {f : ℝ → ℝ} (hfc : ConvexOn ℝ Set.univ f) (x : ℝ) : HasDerivWithinAt f (sInf (slope f x '' Set.Ioi x)) (Set.Ioi x) x

theorem ConvexOn.hasRightDerivAt' {f : ℝ → ℝ} {x : ℝ} (hfc : ConvexOn ℝ (Set.Ici 0) f) (hx : 0 < x) : HasDerivWithinAt f (sInf (slope f x '' Set.Ioi x)) (Set.Ioi x) x

theorem ConvexOn.differentiableWithinAt_Ioi {f : ℝ → ℝ} (hfc : ConvexOn ℝ Set.univ f) (x : ℝ) : DifferentiableWithinAt ℝ f (Set.Ioi x) x

theorem ConvexOn.differentiableWithinAt_Ioi' {f : ℝ → ℝ} {x : ℝ} (hfc : ConvexOn ℝ (Set.Ici 0) f) (hx : 0 < x) : DifferentiableWithinAt ℝ f (Set.Ioi x) x

theorem ConvexOn.hadDerivWithinAt_rightDeriv {f : ℝ → ℝ} (hfc : ConvexOn ℝ Set.univ f) (x : ℝ) : HasDerivWithinAt f (rightDeriv f x) (Set.Ioi x) x

theorem ConvexOn.hasLeftDerivAt {f : ℝ → ℝ} (hfc : ConvexOn ℝ Set.univ f) (x : ℝ) : HasDerivWithinAt f (sSup (slope f x '' Set.Iio x)) (Set.Iio x) x

theorem ConvexOn.differentiableWithinAt_Iio {f : ℝ → ℝ} (hfc : ConvexOn ℝ Set.univ f) (x : ℝ) : DifferentiableWithinAt ℝ f (Set.Iio x) x

theorem ConvexOn.hadDerivWithinAt_leftDeriv {f : ℝ → ℝ} (hfc : ConvexOn ℝ Set.univ f) (x : ℝ) : HasDerivWithinAt f (leftDeriv f x) (Set.Iio x) x

theorem ConvexOn.rightDeriv_eq_sInf_slope {f : ℝ → ℝ} (hfc : ConvexOn ℝ Set.univ f) (x : ℝ) : rightDeriv f x = sInf (slope f x '' Set.Ioi x)

theorem ConvexOn.rightDeriv_eq_sInf_slope' {f : ℝ → ℝ} {x : ℝ} (hfc : ConvexOn ℝ (Set.Ici 0) f) (hx : 0 < x) : rightDeriv f x = sInf (slope f x '' Set.Ioi x)

theorem ConvexOn.leftDeriv_eq_sSup_slope {f : ℝ → ℝ} (hfc : ConvexOn ℝ Set.univ f) (x : ℝ) : leftDeriv f x = sSup (slope f x '' Set.Iio x)

theorem ConvexOn.rightDeriv_mono {f : ℝ → ℝ} (hfc : ConvexOn ℝ Set.univ f) : Monotone (rightDeriv f)

theorem ConvexOn.rightDeriv_mono' {f : ℝ → ℝ} (hfc : ConvexOn ℝ (Set.Ici 0) f) : MonotoneOn (rightDeriv f) (Set.Ioi 0)

theorem ConvexOn.leftDeriv_mono {f : ℝ → ℝ} (hfc : ConvexOn ℝ Set.univ f) : Monotone (leftDeriv f)

theorem ConvexOn.leftDeriv_le_rightDeriv {f : ℝ → ℝ} (hfc : ConvexOn ℝ Set.univ f) : leftDeriv f ≤ rightDeriv f

theorem ConvexOn.rightDeriv_right_continuous {f : ℝ → ℝ} (hfc : ConvexOn ℝ Set.univ f) (w : ℝ) : ContinuousWithinAt (rightDeriv f) (Set.Ici w) w

theorem ConvexOn.leftDeriv_left_continuous {f : ℝ → ℝ} (hfc : ConvexOn ℝ Set.univ f) (w : ℝ) : ContinuousWithinAt (leftDeriv f) (Set.Iic w) w

noncomputable def ConvexOn.rightDerivStieltjes {f : ℝ → ℝ} (hf : ConvexOn ℝ Set.univ f) : StieltjesFunction

The right derivative of a convex real function is a Stieltjes function.

Equations

• hf.rightDerivStieltjes = { toFun := rightDeriv f, mono' := ⋯, right_continuous' := ⋯ }

theorem ConvexOn.rightDerivStieltjes_eq_rightDeriv {f : ℝ → ℝ} (hf : ConvexOn ℝ Set.univ f) : ↑hf.rightDerivStieltjes = rightDeriv f

theorem ConvexOn.rightDerivStieltjes_const (c : ℝ) : ⋯.rightDerivStieltjes = 0

theorem ConvexOn.rightDerivStieltjes_linear (a : ℝ) : ⋯.rightDerivStieltjes = StieltjesFunction.const a

theorem ConvexOn.rightDerivStieltjes_add {f : ℝ → ℝ} {g : ℝ → ℝ} (hf : ConvexOn ℝ Set.univ f) (hg : ConvexOn ℝ Set.univ g) : ⋯.rightDerivStieltjes = hf.rightDerivStieltjes + hg.rightDerivStieltjes

theorem ConvexOn.rightDerivStieltjes_add_const {f : ℝ → ℝ} (hf : ConvexOn ℝ Set.univ f) (c : ℝ) : ⋯.rightDerivStieltjes = hf.rightDerivStieltjes