# mathlib3documentation

analysis.convex.proj_Icc

# 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.

@[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.

@[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.

@[protected]
theorem convex_on.Ici_extend {π : Type u_1} {Ξ² : Type u_2} [linear_ordered_field π] [has_smul π Ξ²] {s : set π} {f : π β Ξ²} {z : π} (hf : convex_on π s f) (hf' : 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.

@[protected]
theorem convex_on.Iic_extend {π : Type u_1} {Ξ² : Type u_2} [linear_ordered_field π] [has_smul π Ξ²] {s : set π} {f : π β Ξ²} {z : π} (hf : convex_on π s f) (hf' : 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.

@[protected]
theorem concave_on.Ici_extend {π : Type u_1} {Ξ² : Type u_2} [linear_ordered_field π] [has_smul π Ξ²] {s : set π} {f : π β Ξ²} {z : π} (hf : concave_on π s f) (hf' : 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.

@[protected]
theorem concave_on.Iic_extend {π : Type u_1} {Ξ² : Type u_2} [linear_ordered_field π] [has_smul π Ξ²] {s : set π} {f : π β Ξ²} {z : π} (hf : concave_on π s f) (hf' : 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.

@[protected]
theorem convex_on.Ici_extend_of_monotone {π : Type u_1} {Ξ² : Type u_2} [linear_ordered_field π] [has_smul π Ξ²] {f : π β Ξ²} {z : π} (hf : convex_on π set.univ f) (hf' : monotone f) :

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

@[protected]
theorem convex_on.Iic_extend_of_antitone {π : Type u_1} {Ξ² : Type u_2} [linear_ordered_field π] [has_smul π Ξ²] {f : π β Ξ²} {z : π} (hf : convex_on π set.univ f) (hf' : antitone f) :

A convex antitone function extended constantly towards infinity is convex.

@[protected]
theorem concave_on.Ici_extend_of_antitone {π : Type u_1} {Ξ² : Type u_2} [linear_ordered_field π] [has_smul π Ξ²] {f : π β Ξ²} {z : π} (hf : concave_on π set.univ f) (hf' : antitone f) :

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

@[protected]
theorem concave_on.Iic_extend_of_monotone {π : Type u_1} {Ξ² : Type u_2} [linear_ordered_field π] [has_smul π Ξ²] {f : π β Ξ²} {z : π} (hf : concave_on π set.univ f) (hf' : monotone f) :

A concave monotone function extended constantly towards infinity is concave.