Convexity of extension from intervals #

This file proves that constantly extending monotone/antitone functions preserves their convexity.

TODO #

We could deduplicate the proofs if we had a typeclass stating that segment 𝕜 x y = [x -[𝕜] y] as 𝕜ᵒᵈ respects it if 𝕜 does, while 𝕜ᵒᵈ isn't a linear_ordered_field if 𝕜 is.

source

@[protected]

theorem convex.Ici_extend {𝕜 : Type u_1} [linear_ordered_field 𝕜] {s : set 𝕜} {z : 𝕜} (hf : convex 𝕜 s) :

convex 𝕜 {x : 𝕜 | set.Ici_extend ((set.Ici z).restrict (λ (_x : 𝕜), _x ∈ s)) x}

A convex set extended towards minus infinity is convex.

source

@[protected]

theorem convex.Iic_extend {𝕜 : Type u_1} [linear_ordered_field 𝕜] {s : set 𝕜} {z : 𝕜} (hf : convex 𝕜 s) :

convex 𝕜 {x : 𝕜 | set.Iic_extend ((set.Iic z).restrict (λ (_x : 𝕜), _x ∈ s)) x}

A convex set extended towards infinity is convex.

source

@[protected]

theorem convex_on.Ici_extend {𝕜 : Type u_1} {β : Type u_2} [linear_ordered_field 𝕜] [linear_ordered_add_comm_monoid β] [has_smul 𝕜 β] {s : set 𝕜} {f : 𝕜 → β} {z : 𝕜} (hf : convex_on 𝕜 s f) (hf' : monotone_on f s) :

convex_on 𝕜 {x : 𝕜 | set.Ici_extend ((set.Ici z).restrict (λ (_x : 𝕜), _x ∈ s)) x} (set.Ici_extend ((set.Ici z).restrict f))

A convex monotone function extended constantly towards minus infinity is convex.

source

@[protected]

theorem convex_on.Iic_extend {𝕜 : Type u_1} {β : Type u_2} [linear_ordered_field 𝕜] [linear_ordered_add_comm_monoid β] [has_smul 𝕜 β] {s : set 𝕜} {f : 𝕜 → β} {z : 𝕜} (hf : convex_on 𝕜 s f) (hf' : antitone_on f s) :

convex_on 𝕜 {x : 𝕜 | set.Iic_extend ((set.Iic z).restrict (λ (_x : 𝕜), _x ∈ s)) x} (set.Iic_extend ((set.Iic z).restrict f))

A convex antitone function extended constantly towards infinity is convex.

source

@[protected]

theorem concave_on.Ici_extend {𝕜 : Type u_1} {β : Type u_2} [linear_ordered_field 𝕜] [linear_ordered_add_comm_monoid β] [has_smul 𝕜 β] {s : set 𝕜} {f : 𝕜 → β} {z : 𝕜} (hf : concave_on 𝕜 s f) (hf' : antitone_on f s) :

concave_on 𝕜 {x : 𝕜 | set.Ici_extend ((set.Ici z).restrict (λ (_x : 𝕜), _x ∈ s)) x} (set.Ici_extend ((set.Ici z).restrict f))

A concave antitone function extended constantly minus towards infinity is concave.

source

@[protected]

theorem concave_on.Iic_extend {𝕜 : Type u_1} {β : Type u_2} [linear_ordered_field 𝕜] [linear_ordered_add_comm_monoid β] [has_smul 𝕜 β] {s : set 𝕜} {f : 𝕜 → β} {z : 𝕜} (hf : concave_on 𝕜 s f) (hf' : monotone_on f s) :

concave_on 𝕜 {x : 𝕜 | set.Iic_extend ((set.Iic z).restrict (λ (_x : 𝕜), _x ∈ s)) x} (set.Iic_extend ((set.Iic z).restrict f))

A concave monotone function extended constantly towards infinity is concave.

source

@[protected]

theorem convex_on.Ici_extend_of_monotone {𝕜 : Type u_1} {β : Type u_2} [linear_ordered_field 𝕜] [linear_ordered_add_comm_monoid β] [has_smul 𝕜 β] {f : 𝕜 → β} {z : 𝕜} (hf : convex_on 𝕜 set.univ f) (hf' : monotone f) :

convex_on 𝕜 set.univ (set.Ici_extend ((set.Ici z).restrict f))

A convex monotone function extended constantly towards minus infinity is convex.

source

@[protected]

theorem convex_on.Iic_extend_of_antitone {𝕜 : Type u_1} {β : Type u_2} [linear_ordered_field 𝕜] [linear_ordered_add_comm_monoid β] [has_smul 𝕜 β] {f : 𝕜 → β} {z : 𝕜} (hf : convex_on 𝕜 set.univ f) (hf' : antitone f) :

convex_on 𝕜 set.univ (set.Iic_extend ((set.Iic z).restrict f))

A convex antitone function extended constantly towards infinity is convex.

source

@[protected]

theorem concave_on.Ici_extend_of_antitone {𝕜 : Type u_1} {β : Type u_2} [linear_ordered_field 𝕜] [linear_ordered_add_comm_monoid β] [has_smul 𝕜 β] {f : 𝕜 → β} {z : 𝕜} (hf : concave_on 𝕜 set.univ f) (hf' : antitone f) :

concave_on 𝕜 set.univ (set.Ici_extend ((set.Ici z).restrict f))

A concave antitone function extended constantly minus towards infinity is concave.

source

@[protected]

theorem concave_on.Iic_extend_of_monotone {𝕜 : Type u_1} {β : Type u_2} [linear_ordered_field 𝕜] [linear_ordered_add_comm_monoid β] [has_smul 𝕜 β] {f : 𝕜 → β} {z : 𝕜} (hf : concave_on 𝕜 set.univ f) (hf' : monotone f) :

concave_on 𝕜 set.univ (set.Iic_extend ((set.Iic z).restrict f))

A concave monotone function extended constantly towards infinity is concave.