analysis.convex.function

source

def convex_on (𝕜 : Type u_1) {E : Type u_2} {β : Type u_5} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_monoid β] [has_smul 𝕜 E] [has_smul 𝕜 β] (s : set E) (f : E → β) :

Prop

Convexity of functions

Equations

convex_on 𝕜 s f = (convex 𝕜 s ∧ ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → f (a • x + b • y) ≤ a • f x + b • f y)

source

def concave_on (𝕜 : Type u_1) {E : Type u_2} {β : Type u_5} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_monoid β] [has_smul 𝕜 E] [has_smul 𝕜 β] (s : set E) (f : E → β) :

Prop

Concavity of functions

Equations

concave_on 𝕜 s f = (convex 𝕜 s ∧ ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → a • f x + b • f y ≤ f (a • x + b • y))

source

def strict_convex_on (𝕜 : Type u_1) {E : Type u_2} {β : Type u_5} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_monoid β] [has_smul 𝕜 E] [has_smul 𝕜 β] (s : set E) (f : E → β) :

Prop

Strict convexity of functions

Equations

strict_convex_on 𝕜 s f = (convex 𝕜 s ∧ ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → x ≠ y → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → f (a • x + b • y) < a • f x + b • f y)

source

def strict_concave_on (𝕜 : Type u_1) {E : Type u_2} {β : Type u_5} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_monoid β] [has_smul 𝕜 E] [has_smul 𝕜 β] (s : set E) (f : E → β) :

Prop

Strict concavity of functions

Equations

strict_concave_on 𝕜 s f = (convex 𝕜 s ∧ ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → x ≠ y → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • f x + b • f y < f (a • x + b • y))

source

theorem convex_on.dual {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_monoid β] [has_smul 𝕜 E] [has_smul 𝕜 β] {s : set E} {f : E → β} (hf : convex_on 𝕜 s f) :

concave_on 𝕜 s (⇑order_dual.to_dual ∘ f)

source

theorem concave_on.dual {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_monoid β] [has_smul 𝕜 E] [has_smul 𝕜 β] {s : set E} {f : E → β} (hf : concave_on 𝕜 s f) :

convex_on 𝕜 s (⇑order_dual.to_dual ∘ f)

source

theorem strict_convex_on.dual {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_monoid β] [has_smul 𝕜 E] [has_smul 𝕜 β] {s : set E} {f : E → β} (hf : strict_convex_on 𝕜 s f) :

strict_concave_on 𝕜 s (⇑order_dual.to_dual ∘ f)

source

theorem strict_concave_on.dual {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_monoid β] [has_smul 𝕜 E] [has_smul 𝕜 β] {s : set E} {f : E → β} (hf : strict_concave_on 𝕜 s f) :

strict_convex_on 𝕜 s (⇑order_dual.to_dual ∘ f)

source

theorem convex_on_id {𝕜 : Type u_1} {β : Type u_5} [ordered_semiring 𝕜] [ordered_add_comm_monoid β] [has_smul 𝕜 β] {s : set β} (hs : convex 𝕜 s) :

convex_on 𝕜 s id

source

theorem concave_on_id {𝕜 : Type u_1} {β : Type u_5} [ordered_semiring 𝕜] [ordered_add_comm_monoid β] [has_smul 𝕜 β] {s : set β} (hs : convex 𝕜 s) :

concave_on 𝕜 s id

source

theorem convex_on.subset {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_monoid β] [has_smul 𝕜 E] [has_smul 𝕜 β] {s : set E} {f : E → β} {t : set E} (hf : convex_on 𝕜 t f) (hst : s ⊆ t) (hs : convex 𝕜 s) :

convex_on 𝕜 s f

source

theorem concave_on.subset {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_monoid β] [has_smul 𝕜 E] [has_smul 𝕜 β] {s : set E} {f : E → β} {t : set E} (hf : concave_on 𝕜 t f) (hst : s ⊆ t) (hs : convex 𝕜 s) :

concave_on 𝕜 s f

source

theorem strict_convex_on.subset {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_monoid β] [has_smul 𝕜 E] [has_smul 𝕜 β] {s : set E} {f : E → β} {t : set E} (hf : strict_convex_on 𝕜 t f) (hst : s ⊆ t) (hs : convex 𝕜 s) :

strict_convex_on 𝕜 s f

source

theorem strict_concave_on.subset {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_monoid β] [has_smul 𝕜 E] [has_smul 𝕜 β] {s : set E} {f : E → β} {t : set E} (hf : strict_concave_on 𝕜 t f) (hst : s ⊆ t) (hs : convex 𝕜 s) :

strict_concave_on 𝕜 s f

source

theorem convex_on.comp {𝕜 : Type u_1} {E : Type u_2} {α : Type u_4} {β : Type u_5} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_monoid α] [ordered_add_comm_monoid β] [has_smul 𝕜 E] [has_smul 𝕜 α] [has_smul 𝕜 β] {s : set E} {f : E → β} {g : β → α} (hg : convex_on 𝕜 (f '' s) g) (hf : convex_on 𝕜 s f) (hg' : monotone_on g (f '' s)) :

convex_on 𝕜 s (g ∘ f)

source

theorem concave_on.comp {𝕜 : Type u_1} {E : Type u_2} {α : Type u_4} {β : Type u_5} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_monoid α] [ordered_add_comm_monoid β] [has_smul 𝕜 E] [has_smul 𝕜 α] [has_smul 𝕜 β] {s : set E} {f : E → β} {g : β → α} (hg : concave_on 𝕜 (f '' s) g) (hf : concave_on 𝕜 s f) (hg' : monotone_on g (f '' s)) :

concave_on 𝕜 s (g ∘ f)

source

theorem convex_on.comp_concave_on {𝕜 : Type u_1} {E : Type u_2} {α : Type u_4} {β : Type u_5} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_monoid α] [ordered_add_comm_monoid β] [has_smul 𝕜 E] [has_smul 𝕜 α] [has_smul 𝕜 β] {s : set E} {f : E → β} {g : β → α} (hg : convex_on 𝕜 (f '' s) g) (hf : concave_on 𝕜 s f) (hg' : antitone_on g (f '' s)) :

convex_on 𝕜 s (g ∘ f)

source

theorem concave_on.comp_convex_on {𝕜 : Type u_1} {E : Type u_2} {α : Type u_4} {β : Type u_5} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_monoid α] [ordered_add_comm_monoid β] [has_smul 𝕜 E] [has_smul 𝕜 α] [has_smul 𝕜 β] {s : set E} {f : E → β} {g : β → α} (hg : concave_on 𝕜 (f '' s) g) (hf : convex_on 𝕜 s f) (hg' : antitone_on g (f '' s)) :

concave_on 𝕜 s (g ∘ f)

source

theorem strict_convex_on.comp {𝕜 : Type u_1} {E : Type u_2} {α : Type u_4} {β : Type u_5} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_monoid α] [ordered_add_comm_monoid β] [has_smul 𝕜 E] [has_smul 𝕜 α] [has_smul 𝕜 β] {s : set E} {f : E → β} {g : β → α} (hg : strict_convex_on 𝕜 (f '' s) g) (hf : strict_convex_on 𝕜 s f) (hg' : strict_mono_on g (f '' s)) (hf' : set.inj_on f s) :

strict_convex_on 𝕜 s (g ∘ f)

source

theorem strict_concave_on.comp {𝕜 : Type u_1} {E : Type u_2} {α : Type u_4} {β : Type u_5} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_monoid α] [ordered_add_comm_monoid β] [has_smul 𝕜 E] [has_smul 𝕜 α] [has_smul 𝕜 β] {s : set E} {f : E → β} {g : β → α} (hg : strict_concave_on 𝕜 (f '' s) g) (hf : strict_concave_on 𝕜 s f) (hg' : strict_mono_on g (f '' s)) (hf' : set.inj_on f s) :

strict_concave_on 𝕜 s (g ∘ f)

source

theorem strict_convex_on.comp_strict_concave_on {𝕜 : Type u_1} {E : Type u_2} {α : Type u_4} {β : Type u_5} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_monoid α] [ordered_add_comm_monoid β] [has_smul 𝕜 E] [has_smul 𝕜 α] [has_smul 𝕜 β] {s : set E} {f : E → β} {g : β → α} (hg : strict_convex_on 𝕜 (f '' s) g) (hf : strict_concave_on 𝕜 s f) (hg' : strict_anti_on g (f '' s)) (hf' : set.inj_on f s) :

strict_convex_on 𝕜 s (g ∘ f)

source

theorem strict_concave_on.comp_strict_convex_on {𝕜 : Type u_1} {E : Type u_2} {α : Type u_4} {β : Type u_5} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_monoid α] [ordered_add_comm_monoid β] [has_smul 𝕜 E] [has_smul 𝕜 α] [has_smul 𝕜 β] {s : set E} {f : E → β} {g : β → α} (hg : strict_concave_on 𝕜 (f '' s) g) (hf : strict_convex_on 𝕜 s f) (hg' : strict_anti_on g (f '' s)) (hf' : set.inj_on f s) :

strict_concave_on 𝕜 s (g ∘ f)

source

theorem convex_on.add {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_monoid β] [has_smul 𝕜 E] [distrib_mul_action 𝕜 β] {s : set E} {f g : E → β} (hf : convex_on 𝕜 s f) (hg : convex_on 𝕜 s g) :

convex_on 𝕜 s (f + g)

source

theorem concave_on.add {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_monoid β] [has_smul 𝕜 E] [distrib_mul_action 𝕜 β] {s : set E} {f g : E → β} (hf : concave_on 𝕜 s f) (hg : concave_on 𝕜 s g) :

concave_on 𝕜 s (f + g)

source

theorem convex_on_const {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_monoid β] [has_smul 𝕜 E] [module 𝕜 β] {s : set E} (c : β) (hs : convex 𝕜 s) :

convex_on 𝕜 s (λ (x : E), c)

source

theorem concave_on_const {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_monoid β] [has_smul 𝕜 E] [module 𝕜 β] {s : set E} (c : β) (hs : convex 𝕜 s) :

concave_on 𝕜 s (λ (x : E), c)

source

theorem convex_on_of_convex_epigraph {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_monoid β] [has_smul 𝕜 E] [module 𝕜 β] {s : set E} {f : E → β} (h : convex 𝕜 {p : E × β | p.fst ∈ s ∧ f p.fst ≤ p.snd}) :

convex_on 𝕜 s f

source

theorem concave_on_of_convex_hypograph {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_monoid β] [has_smul 𝕜 E] [module 𝕜 β] {s : set E} {f : E → β} (h : convex 𝕜 {p : E × β | p.fst ∈ s ∧ p.snd ≤ f p.fst}) :

concave_on 𝕜 s f

source

theorem convex_on.convex_le {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_monoid β] [has_smul 𝕜 E] [module 𝕜 β] [ordered_smul 𝕜 β] {s : set E} {f : E → β} (hf : convex_on 𝕜 s f) (r : β) :

convex 𝕜 {x ∈ s | f x ≤ r}

source

theorem concave_on.convex_ge {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_monoid β] [has_smul 𝕜 E] [module 𝕜 β] [ordered_smul 𝕜 β] {s : set E} {f : E → β} (hf : concave_on 𝕜 s f) (r : β) :

convex 𝕜 {x ∈ s | r ≤ f x}

source

theorem convex_on.convex_epigraph {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_monoid β] [has_smul 𝕜 E] [module 𝕜 β] [ordered_smul 𝕜 β] {s : set E} {f : E → β} (hf : convex_on 𝕜 s f) :

convex 𝕜 {p : E × β | p.fst ∈ s ∧ f p.fst ≤ p.snd}

source

theorem concave_on.convex_hypograph {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_monoid β] [has_smul 𝕜 E] [module 𝕜 β] [ordered_smul 𝕜 β] {s : set E} {f : E → β} (hf : concave_on 𝕜 s f) :

convex 𝕜 {p : E × β | p.fst ∈ s ∧ p.snd ≤ f p.fst}

source

theorem convex_on_iff_convex_epigraph {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_monoid β] [has_smul 𝕜 E] [module 𝕜 β] [ordered_smul 𝕜 β] {s : set E} {f : E → β} :

convex_on 𝕜 s f ↔ convex 𝕜 {p : E × β | p.fst ∈ s ∧ f p.fst ≤ p.snd}

source

theorem concave_on_iff_convex_hypograph {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_monoid β] [has_smul 𝕜 E] [module 𝕜 β] [ordered_smul 𝕜 β] {s : set E} {f : E → β} :

concave_on 𝕜 s f ↔ convex 𝕜 {p : E × β | p.fst ∈ s ∧ p.snd ≤ f p.fst}

source

theorem convex_on.translate_right {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_monoid β] [module 𝕜 E] [has_smul 𝕜 β] {s : set E} {f : E → β} (hf : convex_on 𝕜 s f) (c : E) :

convex_on 𝕜 ((λ (z : E), c + z) ⁻¹' s) (f ∘ λ (z : E), c + z)

Right translation preserves convexity.

source

theorem concave_on.translate_right {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_monoid β] [module 𝕜 E] [has_smul 𝕜 β] {s : set E} {f : E → β} (hf : concave_on 𝕜 s f) (c : E) :

concave_on 𝕜 ((λ (z : E), c + z) ⁻¹' s) (f ∘ λ (z : E), c + z)

Right translation preserves concavity.

source

theorem convex_on.translate_left {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_monoid β] [module 𝕜 E] [has_smul 𝕜 β] {s : set E} {f : E → β} (hf : convex_on 𝕜 s f) (c : E) :

convex_on 𝕜 ((λ (z : E), c + z) ⁻¹' s) (f ∘ λ (z : E), z + c)

Left translation preserves convexity.

source

theorem concave_on.translate_left {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_monoid β] [module 𝕜 E] [has_smul 𝕜 β] {s : set E} {f : E → β} (hf : concave_on 𝕜 s f) (c : E) :

concave_on 𝕜 ((λ (z : E), c + z) ⁻¹' s) (f ∘ λ (z : E), z + c)

Left translation preserves concavity.

source

theorem convex_on_iff_forall_pos {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_monoid β] [module 𝕜 E] [module 𝕜 β] {s : set E} {f : E → β} :

convex_on 𝕜 s f ↔ convex 𝕜 s ∧ ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → f (a • x + b • y) ≤ a • f x + b • f y

source

theorem concave_on_iff_forall_pos {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_monoid β] [module 𝕜 E] [module 𝕜 β] {s : set E} {f : E → β} :

concave_on 𝕜 s f ↔ convex 𝕜 s ∧ ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • f x + b • f y ≤ f (a • x + b • y)

source

theorem convex_on_iff_pairwise_pos {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_monoid β] [module 𝕜 E] [module 𝕜 β] {s : set E} {f : E → β} :

convex_on 𝕜 s f ↔ convex 𝕜 s ∧ s.pairwise (λ (x y : E), ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → f (a • x + b • y) ≤ a • f x + b • f y)

source

theorem concave_on_iff_pairwise_pos {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_monoid β] [module 𝕜 E] [module 𝕜 β] {s : set E} {f : E → β} :

concave_on 𝕜 s f ↔ convex 𝕜 s ∧ s.pairwise (λ (x y : E), ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • f x + b • f y ≤ f (a • x + b • y))

source

theorem linear_map.convex_on {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_monoid β] [module 𝕜 E] [module 𝕜 β] (f : E →ₗ[𝕜] β) {s : set E} (hs : convex 𝕜 s) :

convex_on 𝕜 s ⇑f

A linear map is convex.

source

theorem linear_map.concave_on {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_monoid β] [module 𝕜 E] [module 𝕜 β] (f : E →ₗ[𝕜] β) {s : set E} (hs : convex 𝕜 s) :

concave_on 𝕜 s ⇑f

A linear map is concave.

source

theorem strict_convex_on.convex_on {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_monoid β] [module 𝕜 E] [module 𝕜 β] {s : set E} {f : E → β} (hf : strict_convex_on 𝕜 s f) :

convex_on 𝕜 s f

source

theorem strict_concave_on.concave_on {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_monoid β] [module 𝕜 E] [module 𝕜 β] {s : set E} {f : E → β} (hf : strict_concave_on 𝕜 s f) :

concave_on 𝕜 s f

source

theorem strict_convex_on.convex_lt {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_monoid β] [module 𝕜 E] [module 𝕜 β] [ordered_smul 𝕜 β] {s : set E} {f : E → β} (hf : strict_convex_on 𝕜 s f) (r : β) :

convex 𝕜 {x ∈ s | f x < r}

source

theorem strict_concave_on.convex_gt {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_monoid β] [module 𝕜 E] [module 𝕜 β] [ordered_smul 𝕜 β] {s : set E} {f : E → β} (hf : strict_concave_on 𝕜 s f) (r : β) :

convex 𝕜 {x ∈ s | r < f x}

source

theorem linear_order.convex_on_of_lt {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_monoid β] [module 𝕜 E] [module 𝕜 β] [linear_order E] {s : set E} {f : E → β} (hs : convex 𝕜 s) (hf : ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → x < y → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → f (a • x + b • y) ≤ a • f x + b • f y) :

convex_on 𝕜 s f

For a function on a convex set in a linearly ordered space (where the order and the algebraic structures aren't necessarily compatible), in order to prove that it is convex, it suffices to verify the inequality f (a • x + b • y) ≤ a • f x + b • f y only for x < y and positive a, b. The main use case is E = 𝕜 however one can apply it, e.g., to 𝕜^n with lexicographic order.

source

theorem linear_order.concave_on_of_lt {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_monoid β] [module 𝕜 E] [module 𝕜 β] [linear_order E] {s : set E} {f : E → β} (hs : convex 𝕜 s) (hf : ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → x < y → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • f x + b • f y ≤ f (a • x + b • y)) :

concave_on 𝕜 s f

For a function on a convex set in a linearly ordered space (where the order and the algebraic structures aren't necessarily compatible), in order to prove that it is concave it suffices to verify the inequality a • f x + b • f y ≤ f (a • x + b • y) for x < y and positive a, b. The main use case is E = ℝ however one can apply it, e.g., to ℝ^n with lexicographic order.

source

theorem linear_order.strict_convex_on_of_lt {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_monoid β] [module 𝕜 E] [module 𝕜 β] [linear_order E] {s : set E} {f : E → β} (hs : convex 𝕜 s) (hf : ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → x < y → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → f (a • x + b • y) < a • f x + b • f y) :

strict_convex_on 𝕜 s f

For a function on a convex set in a linearly ordered space (where the order and the algebraic structures aren't necessarily compatible), in order to prove that it is strictly convex, it suffices to verify the inequality f (a • x + b • y) < a • f x + b • f y for x < y and positive a, b. The main use case is E = 𝕜 however one can apply it, e.g., to 𝕜^n with lexicographic order.

source

theorem linear_order.strict_concave_on_of_lt {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_monoid β] [module 𝕜 E] [module 𝕜 β] [linear_order E] {s : set E} {f : E → β} (hs : convex 𝕜 s) (hf : ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → x < y → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • f x + b • f y < f (a • x + b • y)) :

strict_concave_on 𝕜 s f

For a function on a convex set in a linearly ordered space (where the order and the algebraic structures aren't necessarily compatible), in order to prove that it is strictly concave it suffices to verify the inequality a • f x + b • f y < f (a • x + b • y) for x < y and positive a, b. The main use case is E = 𝕜 however one can apply it, e.g., to 𝕜^n with lexicographic order.

source

theorem convex_on.comp_linear_map {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {β : Type u_5} [ordered_semiring 𝕜] [add_comm_monoid E] [add_comm_monoid F] [ordered_add_comm_monoid β] [module 𝕜 E] [module 𝕜 F] [has_smul 𝕜 β] {f : F → β} {s : set F} (hf : convex_on 𝕜 s f) (g : E →ₗ[𝕜] F) :

convex_on 𝕜 (⇑g ⁻¹' s) (f ∘ ⇑g)

If g is convex on s, so is (f ∘ g) on f ⁻¹' s for a linear f.

source

theorem concave_on.comp_linear_map {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {β : Type u_5} [ordered_semiring 𝕜] [add_comm_monoid E] [add_comm_monoid F] [ordered_add_comm_monoid β] [module 𝕜 E] [module 𝕜 F] [has_smul 𝕜 β] {f : F → β} {s : set F} (hf : concave_on 𝕜 s f) (g : E →ₗ[𝕜] F) :

concave_on 𝕜 (⇑g ⁻¹' s) (f ∘ ⇑g)

If g is concave on s, so is (g ∘ f) on f ⁻¹' s for a linear f.

source

theorem strict_convex_on.add_convex_on {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_cancel_add_comm_monoid β] [has_smul 𝕜 E] [distrib_mul_action 𝕜 β] {s : set E} {f g : E → β} (hf : strict_convex_on 𝕜 s f) (hg : convex_on 𝕜 s g) :

strict_convex_on 𝕜 s (f + g)

source

theorem convex_on.add_strict_convex_on {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_cancel_add_comm_monoid β] [has_smul 𝕜 E] [distrib_mul_action 𝕜 β] {s : set E} {f g : E → β} (hf : convex_on 𝕜 s f) (hg : strict_convex_on 𝕜 s g) :

strict_convex_on 𝕜 s (f + g)

source

theorem strict_convex_on.add {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_cancel_add_comm_monoid β] [has_smul 𝕜 E] [distrib_mul_action 𝕜 β] {s : set E} {f g : E → β} (hf : strict_convex_on 𝕜 s f) (hg : strict_convex_on 𝕜 s g) :

strict_convex_on 𝕜 s (f + g)

source

theorem strict_concave_on.add_concave_on {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_cancel_add_comm_monoid β] [has_smul 𝕜 E] [distrib_mul_action 𝕜 β] {s : set E} {f g : E → β} (hf : strict_concave_on 𝕜 s f) (hg : concave_on 𝕜 s g) :

strict_concave_on 𝕜 s (f + g)

source

theorem concave_on.add_strict_concave_on {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_cancel_add_comm_monoid β] [has_smul 𝕜 E] [distrib_mul_action 𝕜 β] {s : set E} {f g : E → β} (hf : concave_on 𝕜 s f) (hg : strict_concave_on 𝕜 s g) :

strict_concave_on 𝕜 s (f + g)

source

theorem strict_concave_on.add {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_cancel_add_comm_monoid β] [has_smul 𝕜 E] [distrib_mul_action 𝕜 β] {s : set E} {f g : E → β} (hf : strict_concave_on 𝕜 s f) (hg : strict_concave_on 𝕜 s g) :

strict_concave_on 𝕜 s (f + g)

source

theorem convex_on.convex_lt {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_cancel_add_comm_monoid β] [module 𝕜 E] [module 𝕜 β] [ordered_smul 𝕜 β] {s : set E} {f : E → β} (hf : convex_on 𝕜 s f) (r : β) :

convex 𝕜 {x ∈ s | f x < r}

source

theorem concave_on.convex_gt {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_cancel_add_comm_monoid β] [module 𝕜 E] [module 𝕜 β] [ordered_smul 𝕜 β] {s : set E} {f : E → β} (hf : concave_on 𝕜 s f) (r : β) :

convex 𝕜 {x ∈ s | r < f x}

source

theorem convex_on.open_segment_subset_strict_epigraph {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_cancel_add_comm_monoid β] [module 𝕜 E] [module 𝕜 β] [ordered_smul 𝕜 β] {s : set E} {f : E → β} (hf : convex_on 𝕜 s f) (p q : E × β) (hp : p.fst ∈ s ∧ f p.fst < p.snd) (hq : q.fst ∈ s ∧ f q.fst ≤ q.snd) :

open_segment 𝕜 p q ⊆ {p : E × β | p.fst ∈ s ∧ f p.fst < p.snd}

source

theorem concave_on.open_segment_subset_strict_hypograph {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_cancel_add_comm_monoid β] [module 𝕜 E] [module 𝕜 β] [ordered_smul 𝕜 β] {s : set E} {f : E → β} (hf : concave_on 𝕜 s f) (p q : E × β) (hp : p.fst ∈ s ∧ p.snd < f p.fst) (hq : q.fst ∈ s ∧ q.snd ≤ f q.fst) :

open_segment 𝕜 p q ⊆ {p : E × β | p.fst ∈ s ∧ p.snd < f p.fst}

source

theorem convex_on.convex_strict_epigraph {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_cancel_add_comm_monoid β] [module 𝕜 E] [module 𝕜 β] [ordered_smul 𝕜 β] {s : set E} {f : E → β} (hf : convex_on 𝕜 s f) :

convex 𝕜 {p : E × β | p.fst ∈ s ∧ f p.fst < p.snd}

source

theorem concave_on.convex_strict_hypograph {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_cancel_add_comm_monoid β] [module 𝕜 E] [module 𝕜 β] [ordered_smul 𝕜 β] {s : set E} {f : E → β} (hf : concave_on 𝕜 s f) :

convex 𝕜 {p : E × β | p.fst ∈ s ∧ p.snd < f p.fst}

source

theorem convex_on.sup {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ordered_semiring 𝕜] [add_comm_monoid E] [linear_ordered_add_comm_monoid β] [has_smul 𝕜 E] [module 𝕜 β] [ordered_smul 𝕜 β] {s : set E} {f g : E → β} (hf : convex_on 𝕜 s f) (hg : convex_on 𝕜 s g) :

convex_on 𝕜 s (f ⊔ g)

The pointwise maximum of convex functions is convex.

source

theorem concave_on.inf {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ordered_semiring 𝕜] [add_comm_monoid E] [linear_ordered_add_comm_monoid β] [has_smul 𝕜 E] [module 𝕜 β] [ordered_smul 𝕜 β] {s : set E} {f g : E → β} (hf : concave_on 𝕜 s f) (hg : concave_on 𝕜 s g) :

concave_on 𝕜 s (f ⊓ g)

The pointwise minimum of concave functions is concave.

source

theorem strict_convex_on.sup {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ordered_semiring 𝕜] [add_comm_monoid E] [linear_ordered_add_comm_monoid β] [has_smul 𝕜 E] [module 𝕜 β] [ordered_smul 𝕜 β] {s : set E} {f g : E → β} (hf : strict_convex_on 𝕜 s f) (hg : strict_convex_on 𝕜 s g) :

strict_convex_on 𝕜 s (f ⊔ g)

The pointwise maximum of strictly convex functions is strictly convex.

source

theorem strict_concave_on.inf {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ordered_semiring 𝕜] [add_comm_monoid E] [linear_ordered_add_comm_monoid β] [has_smul 𝕜 E] [module 𝕜 β] [ordered_smul 𝕜 β] {s : set E} {f g : E → β} (hf : strict_concave_on 𝕜 s f) (hg : strict_concave_on 𝕜 s g) :

strict_concave_on 𝕜 s (f ⊓ g)

The pointwise minimum of strictly concave functions is strictly concave.

source

theorem convex_on.le_on_segment' {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ordered_semiring 𝕜] [add_comm_monoid E] [linear_ordered_add_comm_monoid β] [has_smul 𝕜 E] [module 𝕜 β] [ordered_smul 𝕜 β] {s : set E} {f : E → β} (hf : convex_on 𝕜 s f) {x y : E} (hx : x ∈ s) (hy : y ∈ s) {a b : 𝕜} (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1) :

f (a • x + b • y) ≤ linear_order.max (f x) (f y)

A convex function on a segment is upper-bounded by the max of its endpoints.

source

theorem concave_on.ge_on_segment' {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ordered_semiring 𝕜] [add_comm_monoid E] [linear_ordered_add_comm_monoid β] [has_smul 𝕜 E] [module 𝕜 β] [ordered_smul 𝕜 β] {s : set E} {f : E → β} (hf : concave_on 𝕜 s f) {x y : E} (hx : x ∈ s) (hy : y ∈ s) {a b : 𝕜} (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1) :

linear_order.min (f x) (f y) ≤ f (a • x + b • y)

A concave function on a segment is lower-bounded by the min of its endpoints.

source

theorem convex_on.le_on_segment {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ordered_semiring 𝕜] [add_comm_monoid E] [linear_ordered_add_comm_monoid β] [has_smul 𝕜 E] [module 𝕜 β] [ordered_smul 𝕜 β] {s : set E} {f : E → β} (hf : convex_on 𝕜 s f) {x y z : E} (hx : x ∈ s) (hy : y ∈ s) (hz : z ∈ segment 𝕜 x y) :

f z ≤ linear_order.max (f x) (f y)

A convex function on a segment is upper-bounded by the max of its endpoints.

source

theorem concave_on.ge_on_segment {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ordered_semiring 𝕜] [add_comm_monoid E] [linear_ordered_add_comm_monoid β] [has_smul 𝕜 E] [module 𝕜 β] [ordered_smul 𝕜 β] {s : set E} {f : E → β} (hf : concave_on 𝕜 s f) {x y z : E} (hx : x ∈ s) (hy : y ∈ s) (hz : z ∈ segment 𝕜 x y) :

linear_order.min (f x) (f y) ≤ f z

A concave function on a segment is lower-bounded by the min of its endpoints.

source

theorem strict_convex_on.lt_on_open_segment' {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ordered_semiring 𝕜] [add_comm_monoid E] [linear_ordered_add_comm_monoid β] [has_smul 𝕜 E] [module 𝕜 β] [ordered_smul 𝕜 β] {s : set E} {f : E → β} (hf : strict_convex_on 𝕜 s f) {x y : E} (hx : x ∈ s) (hy : y ∈ s) (hxy : x ≠ y) {a b : 𝕜} (ha : 0 < a) (hb : 0 < b) (hab : a + b = 1) :

f (a • x + b • y) < linear_order.max (f x) (f y)

A strictly convex function on an open segment is strictly upper-bounded by the max of its endpoints.

source

theorem strict_concave_on.lt_on_open_segment' {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ordered_semiring 𝕜] [add_comm_monoid E] [linear_ordered_add_comm_monoid β] [has_smul 𝕜 E] [module 𝕜 β] [ordered_smul 𝕜 β] {s : set E} {f : E → β} (hf : strict_concave_on 𝕜 s f) {x y : E} (hx : x ∈ s) (hy : y ∈ s) (hxy : x ≠ y) {a b : 𝕜} (ha : 0 < a) (hb : 0 < b) (hab : a + b = 1) :

linear_order.min (f x) (f y) < f (a • x + b • y)

A strictly concave function on an open segment is strictly lower-bounded by the min of its endpoints.

source

theorem strict_convex_on.lt_on_open_segment {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ordered_semiring 𝕜] [add_comm_monoid E] [linear_ordered_add_comm_monoid β] [has_smul 𝕜 E] [module 𝕜 β] [ordered_smul 𝕜 β] {s : set E} {f : E → β} (hf : strict_convex_on 𝕜 s f) {x y z : E} (hx : x ∈ s) (hy : y ∈ s) (hxy : x ≠ y) (hz : z ∈ open_segment 𝕜 x y) :

f z < linear_order.max (f x) (f y)

A strictly convex function on an open segment is strictly upper-bounded by the max of its endpoints.

source

theorem strict_concave_on.lt_on_open_segment {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ordered_semiring 𝕜] [add_comm_monoid E] [linear_ordered_add_comm_monoid β] [has_smul 𝕜 E] [module 𝕜 β] [ordered_smul 𝕜 β] {s : set E} {f : E → β} (hf : strict_concave_on 𝕜 s f) {x y z : E} (hx : x ∈ s) (hy : y ∈ s) (hxy : x ≠ y) (hz : z ∈ open_segment 𝕜 x y) :

linear_order.min (f x) (f y) < f z

A strictly concave function on an open segment is strictly lower-bounded by the min of its endpoints.

source

theorem convex_on.le_left_of_right_le' {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ordered_semiring 𝕜] [add_comm_monoid E] [linear_ordered_cancel_add_comm_monoid β] [has_smul 𝕜 E] [module 𝕜 β] [ordered_smul 𝕜 β] {s : set E} {f : E → β} (hf : convex_on 𝕜 s f) {x y : E} (hx : x ∈ s) (hy : y ∈ s) {a b : 𝕜} (ha : 0 < a) (hb : 0 ≤ b) (hab : a + b = 1) (hfy : f y ≤ f (a • x + b • y)) :

f (a • x + b • y) ≤ f x

source

theorem concave_on.left_le_of_le_right' {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ordered_semiring 𝕜] [add_comm_monoid E] [linear_ordered_cancel_add_comm_monoid β] [has_smul 𝕜 E] [module 𝕜 β] [ordered_smul 𝕜 β] {s : set E} {f : E → β} (hf : concave_on 𝕜 s f) {x y : E} (hx : x ∈ s) (hy : y ∈ s) {a b : 𝕜} (ha : 0 < a) (hb : 0 ≤ b) (hab : a + b = 1) (hfy : f (a • x + b • y) ≤ f y) :

f x ≤ f (a • x + b • y)

source

theorem convex_on.le_right_of_left_le' {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ordered_semiring 𝕜] [add_comm_monoid E] [linear_ordered_cancel_add_comm_monoid β] [has_smul 𝕜 E] [module 𝕜 β] [ordered_smul 𝕜 β] {s : set E} {f : E → β} (hf : convex_on 𝕜 s f) {x y : E} {a b : 𝕜} (hx : x ∈ s) (hy : y ∈ s) (ha : 0 ≤ a) (hb : 0 < b) (hab : a + b = 1) (hfx : f x ≤ f (a • x + b • y)) :

f (a • x + b • y) ≤ f y

source

theorem concave_on.right_le_of_le_left' {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ordered_semiring 𝕜] [add_comm_monoid E] [linear_ordered_cancel_add_comm_monoid β] [has_smul 𝕜 E] [module 𝕜 β] [ordered_smul 𝕜 β] {s : set E} {f : E → β} (hf : concave_on 𝕜 s f) {x y : E} {a b : 𝕜} (hx : x ∈ s) (hy : y ∈ s) (ha : 0 ≤ a) (hb : 0 < b) (hab : a + b = 1) (hfx : f (a • x + b • y) ≤ f x) :

f y ≤ f (a • x + b • y)

source

theorem convex_on.le_left_of_right_le {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ordered_semiring 𝕜] [add_comm_monoid E] [linear_ordered_cancel_add_comm_monoid β] [has_smul 𝕜 E] [module 𝕜 β] [ordered_smul 𝕜 β] {s : set E} {f : E → β} (hf : convex_on 𝕜 s f) {x y z : E} (hx : x ∈ s) (hy : y ∈ s) (hz : z ∈ open_segment 𝕜 x y) (hyz : f y ≤ f z) :

f z ≤ f x

source

theorem concave_on.left_le_of_le_right {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ordered_semiring 𝕜] [add_comm_monoid E] [linear_ordered_cancel_add_comm_monoid β] [has_smul 𝕜 E] [module 𝕜 β] [ordered_smul 𝕜 β] {s : set E} {f : E → β} (hf : concave_on 𝕜 s f) {x y z : E} (hx : x ∈ s) (hy : y ∈ s) (hz : z ∈ open_segment 𝕜 x y) (hyz : f z ≤ f y) :

f x ≤ f z

source

theorem convex_on.le_right_of_left_le {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ordered_semiring 𝕜] [add_comm_monoid E] [linear_ordered_cancel_add_comm_monoid β] [has_smul 𝕜 E] [module 𝕜 β] [ordered_smul 𝕜 β] {s : set E} {f : E → β} (hf : convex_on 𝕜 s f) {x y z : E} (hx : x ∈ s) (hy : y ∈ s) (hz : z ∈ open_segment 𝕜 x y) (hxz : f x ≤ f z) :

f z ≤ f y

source

theorem concave_on.right_le_of_le_left {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ordered_semiring 𝕜] [add_comm_monoid E] [linear_ordered_cancel_add_comm_monoid β] [has_smul 𝕜 E] [module 𝕜 β] [ordered_smul 𝕜 β] {s : set E} {f : E → β} (hf : concave_on 𝕜 s f) {x y z : E} (hx : x ∈ s) (hy : y ∈ s) (hz : z ∈ open_segment 𝕜 x y) (hxz : f z ≤ f x) :

f y ≤ f z

source

theorem convex_on.lt_left_of_right_lt' {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ordered_semiring 𝕜] [add_comm_monoid E] [linear_ordered_cancel_add_comm_monoid β] [module 𝕜 E] [module 𝕜 β] [ordered_smul 𝕜 β] {s : set E} {f : E → β} (hf : convex_on 𝕜 s f) {x y : E} (hx : x ∈ s) (hy : y ∈ s) {a b : 𝕜} (ha : 0 < a) (hb : 0 < b) (hab : a + b = 1) (hfy : f y < f (a • x + b • y)) :

f (a • x + b • y) < f x

source

theorem concave_on.left_lt_of_lt_right' {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ordered_semiring 𝕜] [add_comm_monoid E] [linear_ordered_cancel_add_comm_monoid β] [module 𝕜 E] [module 𝕜 β] [ordered_smul 𝕜 β] {s : set E} {f : E → β} (hf : concave_on 𝕜 s f) {x y : E} (hx : x ∈ s) (hy : y ∈ s) {a b : 𝕜} (ha : 0 < a) (hb : 0 < b) (hab : a + b = 1) (hfy : f (a • x + b • y) < f y) :

f x < f (a • x + b • y)

source

theorem convex_on.lt_right_of_left_lt' {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ordered_semiring 𝕜] [add_comm_monoid E] [linear_ordered_cancel_add_comm_monoid β] [module 𝕜 E] [module 𝕜 β] [ordered_smul 𝕜 β] {s : set E} {f : E → β} (hf : convex_on 𝕜 s f) {x y : E} {a b : 𝕜} (hx : x ∈ s) (hy : y ∈ s) (ha : 0 < a) (hb : 0 < b) (hab : a + b = 1) (hfx : f x < f (a • x + b • y)) :

f (a • x + b • y) < f y

source

theorem concave_on.lt_right_of_left_lt' {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ordered_semiring 𝕜] [add_comm_monoid E] [linear_ordered_cancel_add_comm_monoid β] [module 𝕜 E] [module 𝕜 β] [ordered_smul 𝕜 β] {s : set E} {f : E → β} (hf : concave_on 𝕜 s f) {x y : E} {a b : 𝕜} (hx : x ∈ s) (hy : y ∈ s) (ha : 0 < a) (hb : 0 < b) (hab : a + b = 1) (hfx : f (a • x + b • y) < f x) :

f y < f (a • x + b • y)

source

theorem convex_on.lt_left_of_right_lt {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ordered_semiring 𝕜] [add_comm_monoid E] [linear_ordered_cancel_add_comm_monoid β] [module 𝕜 E] [module 𝕜 β] [ordered_smul 𝕜 β] {s : set E} {f : E → β} (hf : convex_on 𝕜 s f) {x y z : E} (hx : x ∈ s) (hy : y ∈ s) (hz : z ∈ open_segment 𝕜 x y) (hyz : f y < f z) :

f z < f x

source

theorem concave_on.left_lt_of_lt_right {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ordered_semiring 𝕜] [add_comm_monoid E] [linear_ordered_cancel_add_comm_monoid β] [module 𝕜 E] [module 𝕜 β] [ordered_smul 𝕜 β] {s : set E} {f : E → β} (hf : concave_on 𝕜 s f) {x y z : E} (hx : x ∈ s) (hy : y ∈ s) (hz : z ∈ open_segment 𝕜 x y) (hyz : f z < f y) :

f x < f z

source

theorem convex_on.lt_right_of_left_lt {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ordered_semiring 𝕜] [add_comm_monoid E] [linear_ordered_cancel_add_comm_monoid β] [module 𝕜 E] [module 𝕜 β] [ordered_smul 𝕜 β] {s : set E} {f : E → β} (hf : convex_on 𝕜 s f) {x y z : E} (hx : x ∈ s) (hy : y ∈ s) (hz : z ∈ open_segment 𝕜 x y) (hxz : f x < f z) :

f z < f y

source

theorem concave_on.lt_right_of_left_lt {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ordered_semiring 𝕜] [add_comm_monoid E] [linear_ordered_cancel_add_comm_monoid β] [module 𝕜 E] [module 𝕜 β] [ordered_smul 𝕜 β] {s : set E} {f : E → β} (hf : concave_on 𝕜 s f) {x y z : E} (hx : x ∈ s) (hy : y ∈ s) (hz : z ∈ open_segment 𝕜 x y) (hxz : f z < f x) :

f y < f z

source

@[simp]

theorem neg_convex_on_iff {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_group β] [has_smul 𝕜 E] [module 𝕜 β] {s : set E} {f : E → β} :

convex_on 𝕜 s (-f) ↔ concave_on 𝕜 s f

A function -f is convex iff f is concave.

source

@[simp]

theorem neg_concave_on_iff {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_group β] [has_smul 𝕜 E] [module 𝕜 β] {s : set E} {f : E → β} :

concave_on 𝕜 s (-f) ↔ convex_on 𝕜 s f

A function -f is concave iff f is convex.

source

@[simp]

theorem neg_strict_convex_on_iff {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_group β] [has_smul 𝕜 E] [module 𝕜 β] {s : set E} {f : E → β} :

strict_convex_on 𝕜 s (-f) ↔ strict_concave_on 𝕜 s f

A function -f is strictly convex iff f is strictly concave.

source

@[simp]

theorem neg_strict_concave_on_iff {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_group β] [has_smul 𝕜 E] [module 𝕜 β] {s : set E} {f : E → β} :

strict_concave_on 𝕜 s (-f) ↔ strict_convex_on 𝕜 s f

A function -f is strictly concave iff f is strictly convex.

source

theorem concave_on.neg {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_group β] [has_smul 𝕜 E] [module 𝕜 β] {s : set E} {f : E → β} :

concave_on 𝕜 s f → convex_on 𝕜 s (-f)

Alias of the reverse direction of neg_convex_on_iff.

source

theorem convex_on.neg {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_group β] [has_smul 𝕜 E] [module 𝕜 β] {s : set E} {f : E → β} :

convex_on 𝕜 s f → concave_on 𝕜 s (-f)

Alias of the reverse direction of neg_concave_on_iff.

source

theorem strict_concave_on.neg {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_group β] [has_smul 𝕜 E] [module 𝕜 β] {s : set E} {f : E → β} :

strict_concave_on 𝕜 s f → strict_convex_on 𝕜 s (-f)

Alias of the reverse direction of neg_strict_convex_on_iff.

source

theorem strict_convex_on.neg {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_group β] [has_smul 𝕜 E] [module 𝕜 β] {s : set E} {f : E → β} :

strict_convex_on 𝕜 s f → strict_concave_on 𝕜 s (-f)

Alias of the reverse direction of neg_strict_concave_on_iff.

source

theorem convex_on.sub {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_group β] [has_smul 𝕜 E] [module 𝕜 β] {s : set E} {f g : E → β} (hf : convex_on 𝕜 s f) (hg : concave_on 𝕜 s g) :

convex_on 𝕜 s (f - g)

source

theorem concave_on.sub {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_group β] [has_smul 𝕜 E] [module 𝕜 β] {s : set E} {f g : E → β} (hf : concave_on 𝕜 s f) (hg : convex_on 𝕜 s g) :

concave_on 𝕜 s (f - g)

source

theorem strict_convex_on.sub {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_group β] [has_smul 𝕜 E] [module 𝕜 β] {s : set E} {f g : E → β} (hf : strict_convex_on 𝕜 s f) (hg : strict_concave_on 𝕜 s g) :

strict_convex_on 𝕜 s (f - g)

source

theorem strict_concave_on.sub {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_group β] [has_smul 𝕜 E] [module 𝕜 β] {s : set E} {f g : E → β} (hf : strict_concave_on 𝕜 s f) (hg : strict_convex_on 𝕜 s g) :

strict_concave_on 𝕜 s (f - g)

source

theorem convex_on.sub_strict_concave_on {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_group β] [has_smul 𝕜 E] [module 𝕜 β] {s : set E} {f g : E → β} (hf : convex_on 𝕜 s f) (hg : strict_concave_on 𝕜 s g) :

strict_convex_on 𝕜 s (f - g)

source

theorem concave_on.sub_strict_convex_on {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_group β] [has_smul 𝕜 E] [module 𝕜 β] {s : set E} {f g : E → β} (hf : concave_on 𝕜 s f) (hg : strict_convex_on 𝕜 s g) :

strict_concave_on 𝕜 s (f - g)

source

theorem strict_convex_on.sub_concave_on {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_group β] [has_smul 𝕜 E] [module 𝕜 β] {s : set E} {f g : E → β} (hf : strict_convex_on 𝕜 s f) (hg : concave_on 𝕜 s g) :

strict_convex_on 𝕜 s (f - g)

source

theorem strict_concave_on.sub_convex_on {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ordered_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_group β] [has_smul 𝕜 E] [module 𝕜 β] {s : set E} {f g : E → β} (hf : strict_concave_on 𝕜 s f) (hg : convex_on 𝕜 s g) :

strict_concave_on 𝕜 s (f - g)

source

theorem strict_convex_on.translate_right {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ordered_semiring 𝕜] [add_cancel_comm_monoid E] [ordered_add_comm_monoid β] [module 𝕜 E] [has_smul 𝕜 β] {s : set E} {f : E → β} (hf : strict_convex_on 𝕜 s f) (c : E) :

strict_convex_on 𝕜 ((λ (z : E), c + z) ⁻¹' s) (f ∘ λ (z : E), c + z)

Right translation preserves strict convexity.

source

theorem strict_concave_on.translate_right {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ordered_semiring 𝕜] [add_cancel_comm_monoid E] [ordered_add_comm_monoid β] [module 𝕜 E] [has_smul 𝕜 β] {s : set E} {f : E → β} (hf : strict_concave_on 𝕜 s f) (c : E) :

strict_concave_on 𝕜 ((λ (z : E), c + z) ⁻¹' s) (f ∘ λ (z : E), c + z)

Right translation preserves strict concavity.

source

theorem strict_convex_on.translate_left {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ordered_semiring 𝕜] [add_cancel_comm_monoid E] [ordered_add_comm_monoid β] [module 𝕜 E] [has_smul 𝕜 β] {s : set E} {f : E → β} (hf : strict_convex_on 𝕜 s f) (c : E) :

strict_convex_on 𝕜 ((λ (z : E), c + z) ⁻¹' s) (f ∘ λ (z : E), z + c)

Left translation preserves strict convexity.

source

theorem strict_concave_on.translate_left {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ordered_semiring 𝕜] [add_cancel_comm_monoid E] [ordered_add_comm_monoid β] [module 𝕜 E] [has_smul 𝕜 β] {s : set E} {f : E → β} (hf : strict_concave_on 𝕜 s f) (c : E) :

strict_concave_on 𝕜 ((λ (z : E), c + z) ⁻¹' s) (f ∘ λ (z : E), z + c)

Left translation preserves strict concavity.

source

theorem convex_on.smul {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ordered_comm_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_monoid β] [has_smul 𝕜 E] [module 𝕜 β] [ordered_smul 𝕜 β] {s : set E} {f : E → β} {c : 𝕜} (hc : 0 ≤ c) (hf : convex_on 𝕜 s f) :

convex_on 𝕜 s (λ (x : E), c • f x)

source

theorem concave_on.smul {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [ordered_comm_semiring 𝕜] [add_comm_monoid E] [ordered_add_comm_monoid β] [has_smul 𝕜 E] [module 𝕜 β] [ordered_smul 𝕜 β] {s : set E} {f : E → β} {c : 𝕜} (hc : 0 ≤ c) (hf : concave_on 𝕜 s f) :

concave_on 𝕜 s (λ (x : E), c • f x)

source

theorem convex_on.comp_affine_map {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {β : Type u_5} [linear_ordered_field 𝕜] [add_comm_group E] [add_comm_group F] [ordered_add_comm_monoid β] [module 𝕜 E] [module 𝕜 F] [has_smul 𝕜 β] {f : F → β} (g : E →ᵃ[𝕜] F) {s : set F} (hf : convex_on 𝕜 s f) :

convex_on 𝕜 (⇑g ⁻¹' s) (f ∘ ⇑g)

If a function is convex on s, it remains convex when precomposed by an affine map.

source

theorem concave_on.comp_affine_map {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {β : Type u_5} [linear_ordered_field 𝕜] [add_comm_group E] [add_comm_group F] [ordered_add_comm_monoid β] [module 𝕜 E] [module 𝕜 F] [has_smul 𝕜 β] {f : F → β} (g : E →ᵃ[𝕜] F) {s : set F} (hf : concave_on 𝕜 s f) :

concave_on 𝕜 (⇑g ⁻¹' s) (f ∘ ⇑g)

If a function is concave on s, it remains concave when precomposed by an affine map.

source

theorem convex_on_iff_div {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [linear_ordered_field 𝕜] [add_comm_monoid E] [ordered_add_comm_monoid β] [has_smul 𝕜 E] [has_smul 𝕜 β] {s : set E} {f : E → β} :

convex_on 𝕜 s f ↔ convex 𝕜 s ∧ ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → 0 < a + b → f ((a / (a + b)) • x + (b / (a + b)) • y) ≤ (a / (a + b)) • f x + (b / (a + b)) • f y

source

theorem concave_on_iff_div {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [linear_ordered_field 𝕜] [add_comm_monoid E] [ordered_add_comm_monoid β] [has_smul 𝕜 E] [has_smul 𝕜 β] {s : set E} {f : E → β} :

concave_on 𝕜 s f ↔ convex 𝕜 s ∧ ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → 0 < a + b → (a / (a + b)) • f x + (b / (a + b)) • f y ≤ f ((a / (a + b)) • x + (b / (a + b)) • y)

source

theorem strict_convex_on_iff_div {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [linear_ordered_field 𝕜] [add_comm_monoid E] [ordered_add_comm_monoid β] [has_smul 𝕜 E] [has_smul 𝕜 β] {s : set E} {f : E → β} :

strict_convex_on 𝕜 s f ↔ convex 𝕜 s ∧ ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → x ≠ y → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → f ((a / (a + b)) • x + (b / (a + b)) • y) < (a / (a + b)) • f x + (b / (a + b)) • f y

source

theorem strict_concave_on_iff_div {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [linear_ordered_field 𝕜] [add_comm_monoid E] [ordered_add_comm_monoid β] [has_smul 𝕜 E] [has_smul 𝕜 β] {s : set E} {f : E → β} :

strict_concave_on 𝕜 s f ↔ convex 𝕜 s ∧ ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → x ≠ y → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → (a / (a + b)) • f x + (b / (a + b)) • f y < f ((a / (a + b)) • x + (b / (a + b)) • y)

source

theorem convex_on.le_right_of_left_le'' {𝕜 : Type u_1} {β : Type u_5} [linear_ordered_field 𝕜] [linear_ordered_cancel_add_comm_monoid β] [module 𝕜 β] [ordered_smul 𝕜 β] {x y z : 𝕜} {s : set 𝕜} {f : 𝕜 → β} (hf : convex_on 𝕜 s f) (hx : x ∈ s) (hz : z ∈ s) (hxy : x < y) (hyz : y ≤ z) (h : f x ≤ f y) :

f y ≤ f z

source

theorem convex_on.le_left_of_right_le'' {𝕜 : Type u_1} {β : Type u_5} [linear_ordered_field 𝕜] [linear_ordered_cancel_add_comm_monoid β] [module 𝕜 β] [ordered_smul 𝕜 β] {x y z : 𝕜} {s : set 𝕜} {f : 𝕜 → β} (hf : convex_on 𝕜 s f) (hx : x ∈ s) (hz : z ∈ s) (hxy : x ≤ y) (hyz : y < z) (h : f z ≤ f y) :

f y ≤ f x

source

theorem concave_on.right_le_of_le_left'' {𝕜 : Type u_1} {β : Type u_5} [linear_ordered_field 𝕜] [linear_ordered_cancel_add_comm_monoid β] [module 𝕜 β] [ordered_smul 𝕜 β] {x y z : 𝕜} {s : set 𝕜} {f : 𝕜 → β} (hf : concave_on 𝕜 s f) (hx : x ∈ s) (hz : z ∈ s) (hxy : x < y) (hyz : y ≤ z) (h : f y ≤ f x) :

f z ≤ f y

source

theorem concave_on.left_le_of_le_right'' {𝕜 : Type u_1} {β : Type u_5} [linear_ordered_field 𝕜] [linear_ordered_cancel_add_comm_monoid β] [module 𝕜 β] [ordered_smul 𝕜 β] {x y z : 𝕜} {s : set 𝕜} {f : 𝕜 → β} (hf : concave_on 𝕜 s f) (hx : x ∈ s) (hz : z ∈ s) (hxy : x ≤ y) (hyz : y < z) (h : f y ≤ f z) :

f x ≤ f y

mathlib3 documentation

Convex and concave functions #

Main declarations #