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