Convex functions are continuous

This file proves that a convex function from a finite-dimensional real normed space to ℝ is continuous.

theorem ConvexOn.lipschitzOnWith_of_abs_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {x₀ : E} {ε r M : ℝ} (hf : ConvexOn ℝ (Metric.ball x₀ r) f) (hε : 0 < ε) (hM : ∀ (a : E), dist a x₀ < r → |f a| ≤ M) : LipschitzOnWith (2 * M / ε).toNNReal f (Metric.ball x₀ (r - ε))

theorem ConcaveOn.lipschitzOnWith_of_abs_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {x₀ : E} {ε r M : ℝ} (hf : ConcaveOn ℝ (Metric.ball x₀ r) f) (hε : 0 < ε) (hM : ∀ (a : E), dist a x₀ < r → |f a| ≤ M) : LipschitzOnWith (2 * M / ε).toNNReal f (Metric.ball x₀ (r - ε))

theorem ConvexOn.exists_lipschitzOnWith_of_isBounded {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {x₀ : E} {r r' : ℝ} (hf : ConvexOn ℝ (Metric.ball x₀ r) f) (hr : r' < r) (hf' : Bornology.IsBounded (f '' Metric.ball x₀ r)) : ∃ (K : NNReal), LipschitzOnWith K f (Metric.ball x₀ r')

theorem ConcaveOn.exists_lipschitzOnWith_of_isBounded {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {x₀ : E} {r r' : ℝ} (hf : ConcaveOn ℝ (Metric.ball x₀ r) f) (hr : r' < r) (hf' : Bornology.IsBounded (f '' Metric.ball x₀ r)) : ∃ (K : NNReal), LipschitzOnWith K f (Metric.ball x₀ r')

theorem ConvexOn.isBoundedUnder_abs {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {C : Set E} {f : E → ℝ} (hf : ConvexOn ℝ C f) {x₀ : E} (hC : C ∈ nhds x₀) : Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) (nhds x₀) |f| ↔ Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) (nhds x₀) f

theorem ConcaveOn.isBoundedUnder_abs {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {C : Set E} {f : E → ℝ} (hf : ConcaveOn ℝ C f) {x₀ : E} (hC : C ∈ nhds x₀) : Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) (nhds x₀) |f| ↔ Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≥ x2) (nhds x₀) f

theorem ConvexOn.continuousOn_tfae {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {C : Set E} {f : E → ℝ} (hC : IsOpen C) (hC' : C.Nonempty) (hf : ConvexOn ℝ C f) : [LocallyLipschitzOn C f, ContinuousOn f C, ∃ x₀ ∈ C, ContinuousAt f x₀, ∃ x₀ ∈ C, Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) (nhds x₀) f, ∀ ⦃x₀ : E⦄, x₀ ∈ C → Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) (nhds x₀) f, ∀ ⦃x₀ : E⦄, x₀ ∈ C → Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) (nhds x₀) |f|].TFAE

theorem ConcaveOn.continuousOn_tfae {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {C : Set E} {f : E → ℝ} (hC : IsOpen C) (hC' : C.Nonempty) (hf : ConcaveOn ℝ C f) : [LocallyLipschitzOn C f, ContinuousOn f C, ∃ x₀ ∈ C, ContinuousAt f x₀, ∃ x₀ ∈ C, Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≥ x2) (nhds x₀) f, ∀ ⦃x₀ : E⦄, x₀ ∈ C → Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≥ x2) (nhds x₀) f, ∀ ⦃x₀ : E⦄, x₀ ∈ C → Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) (nhds x₀) |f|].TFAE

theorem ConvexOn.locallyLipschitzOn_iff_continuousOn {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {C : Set E} {f : E → ℝ} (hC : IsOpen C) (hf : ConvexOn ℝ C f) : LocallyLipschitzOn C f ↔ ContinuousOn f C

theorem ConcaveOn.locallyLipschitzOn_iff_continuousOn {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {C : Set E} {f : E → ℝ} (hC : IsOpen C) (hf : ConcaveOn ℝ C f) : LocallyLipschitzOn C f ↔ ContinuousOn f C

theorem ConvexOn.locallyLipschitzOn {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {C : Set E} {f : E → ℝ} [FiniteDimensional ℝ E] (hC : IsOpen C) (hf : ConvexOn ℝ C f) : LocallyLipschitzOn C f

theorem ConcaveOn.locallyLipschitzOn {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {C : Set E} {f : E → ℝ} [FiniteDimensional ℝ E] (hC : IsOpen C) (hf : ConcaveOn ℝ C f) : LocallyLipschitzOn C f

theorem ConvexOn.continuousOn {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {C : Set E} {f : E → ℝ} [FiniteDimensional ℝ E] (hC : IsOpen C) (hf : ConvexOn ℝ C f) : ContinuousOn f C

theorem ConcaveOn.continuousOn {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {C : Set E} {f : E → ℝ} [FiniteDimensional ℝ E] (hC : IsOpen C) (hf : ConcaveOn ℝ C f) : ContinuousOn f C

theorem ConvexOn.locallyLipschitzOn_interior {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {C : Set E} {f : E → ℝ} [FiniteDimensional ℝ E] (hf : ConvexOn ℝ C f) : LocallyLipschitzOn (interior C) f

theorem ConcaveOn.locallyLipschitzOn_interior {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {C : Set E} {f : E → ℝ} [FiniteDimensional ℝ E] (hf : ConcaveOn ℝ C f) : LocallyLipschitzOn (interior C) f

theorem ConvexOn.continuousOn_interior {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {C : Set E} {f : E → ℝ} [FiniteDimensional ℝ E] (hf : ConvexOn ℝ C f) : ContinuousOn f (interior C)

theorem ConcaveOn.continuousOn_interior {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {C : Set E} {f : E → ℝ} [FiniteDimensional ℝ E] (hf : ConcaveOn ℝ C f) : ContinuousOn f (interior C)

theorem ConvexOn.locallyLipschitz {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} [FiniteDimensional ℝ E] (hf : ConvexOn ℝ Set.univ f) : LocallyLipschitz f

theorem ConcaveOn.locallyLipschitz {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} [FiniteDimensional ℝ E] (hf : ConcaveOn ℝ Set.univ f) : LocallyLipschitz f

theorem ConvexOn.continuousOn_Ici {f : ℝ → ℝ} {y : ℝ} (hf_cvx : ConvexOn ℝ (Set.Ici y) f) (hf_cont : ContinuousWithinAt f (Set.Ici y) y) : ContinuousOn f (Set.Ici y)

theorem ConcaveOn.continuousOn_Ici {f : ℝ → ℝ} {y : ℝ} (hf_cnv : ConcaveOn ℝ (Set.Ici y) f) (hf_cont : ContinuousWithinAt f (Set.Ici y) y) : ContinuousOn f (Set.Ici y)

theorem ConvexOn.continuousOn_Iic {f : ℝ → ℝ} {y : ℝ} (hf_cvx : ConvexOn ℝ (Set.Iic y) f) (hf_cont : ContinuousWithinAt f (Set.Iic y) y) : ContinuousOn f (Set.Iic y)

theorem ConcaveOn.continuousOn_Iic {f : ℝ → ℝ} {y : ℝ} (hf_cnv : ConcaveOn ℝ (Set.Iic y) f) (hf_cont : ContinuousWithinAt f (Set.Iic y) y) : ContinuousOn f (Set.Iic y)

theorem ConvexOn.continuousOn_Ioc {f : ℝ → ℝ} {y z : ℝ} (hf_cvx : ConvexOn ℝ (Set.Ioc y z) f) (hf_cont : ContinuousWithinAt f (Set.Iic z) z) : ContinuousOn f (Set.Ioc y z)

theorem ConcaveOn.continuousOn_Ioc {f : ℝ → ℝ} {y z : ℝ} (hf_cnv : ConcaveOn ℝ (Set.Ioc y z) f) (hf_cont : ContinuousWithinAt f (Set.Iic z) z) : ContinuousOn f (Set.Ioc y z)

theorem ConvexOn.continuousOn_Ico {f : ℝ → ℝ} {y z : ℝ} (hf_cvx : ConvexOn ℝ (Set.Ico y z) f) (hf_cont : ContinuousWithinAt f (Set.Ici y) y) : ContinuousOn f (Set.Ico y z)

theorem ConcaveOn.continuousOn_Ico {f : ℝ → ℝ} {y z : ℝ} (hf_cnv : ConcaveOn ℝ (Set.Ico y z) f) (hf_cont : ContinuousWithinAt f (Set.Ici y) y) : ContinuousOn f (Set.Ico y z)

theorem ConvexOn.continuousOn_Icc {f : ℝ → ℝ} {y z : ℝ} (hf_cvx : ConvexOn ℝ (Set.Icc y z) f) (hyz : y < z) (hfy : ContinuousWithinAt f (Set.Ici y) y) (hfz : ContinuousWithinAt f (Set.Iic z) z) : ContinuousOn f (Set.Icc y z)

theorem ConcaveOn.continuousOn_Icc {f : ℝ → ℝ} {y z : ℝ} (hf_cnv : ConcaveOn ℝ (Set.Icc y z) f) (hyz : y < z) (hfy : ContinuousWithinAt f (Set.Ici y) y) (hfz : ContinuousWithinAt f (Set.Iic z) z) : ContinuousOn f (Set.Icc y z)