def Function.ContinuousRelativeTo {n : ℕ} (f : EuclideanSpace ℝ (Fin n) → ℝ) (S : Set (EuclideanSpace ℝ (Fin n))) : Prop

Definition 10.0.1. Let f : ℝ^n → ℝ be a function and let S ⊆ ℝ^n. The function f is continuous relative to S if the restriction of f to S (denoted f|_S) is continuous on S.

Equations

• Function.ContinuousRelativeTo f S = ContinuousOn f S

theorem Function.tendsto_nhdsWithin_of_forall_mem {n : ℕ} {S : Set (EuclideanSpace ℝ (Fin n))} {x : EuclideanSpace ℝ (Fin n)} {y : ℕ → EuclideanSpace ℝ (Fin n)} (hyS : ∀ (k : ℕ), y k ∈ S) (hy : Filter.Tendsto y Filter.atTop (nhds x)) : Filter.Tendsto y Filter.atTop (nhdsWithin x S)

If a sequence in a subset S converges in the ambient space, then it also converges in the topology nhdsWithin _ S.

theorem Function.continuousRelativeTo_imp_seq_tendsto {n : ℕ} {f : EuclideanSpace ℝ (Fin n) → ℝ} {S : Set (EuclideanSpace ℝ (Fin n))} : ContinuousRelativeTo f S → ∀ x ∈ S, ∀ (y : ℕ → EuclideanSpace ℝ (Fin n)), (∀ (k : ℕ), y k ∈ S) → Filter.Tendsto y Filter.atTop (nhds x) → Filter.Tendsto (fun (k : ℕ) => f (y k)) Filter.atTop (nhds (f x))

From ContinuousRelativeTo f S (i.e. ContinuousOn f S), every sequence in S converging to x ∈ S has f (y k) → f x.

theorem Function.seq_in_subtype_to_seq_in_ambient {n : ℕ} {S : Set (EuclideanSpace ℝ (Fin n))} {u : ℕ → ↑S} {x : ↑S} (hu : Filter.Tendsto u Filter.atTop (nhds x)) : Filter.Tendsto (fun (k : ℕ) => ↑(u k)) Filter.atTop (nhds ↑x)

A sequence in a subtype S converging to x yields an ambient sequence converging to x.

theorem Function.seq_tendsto_imp_continuousRelativeTo_via_restrict {n : ℕ} {f : EuclideanSpace ℝ (Fin n) → ℝ} {S : Set (EuclideanSpace ℝ (Fin n))} (hseq : ∀ x ∈ S, ∀ (y : ℕ → EuclideanSpace ℝ (Fin n)), (∀ (k : ℕ), y k ∈ S) → Filter.Tendsto y Filter.atTop (nhds x) → Filter.Tendsto (fun (k : ℕ) => f (y k)) Filter.atTop (nhds (f x))) : ContinuousRelativeTo f S

If every ambient sequence in S converging to x ∈ S satisfies f (y k) → f x, then f is continuous relative to S.

theorem Function.continuousRelativeTo_iff_seq_tendsto {n : ℕ} (f : EuclideanSpace ℝ (Fin n) → ℝ) (S : Set (EuclideanSpace ℝ (Fin n))) : ContinuousRelativeTo f S ↔ ∀ x ∈ S, ∀ (y : ℕ → EuclideanSpace ℝ (Fin n)), (∀ (k : ℕ), y k ∈ S) → Filter.Tendsto y Filter.atTop (nhds x) → Filter.Tendsto (fun (k : ℕ) => f (y k)) Filter.atTop (nhds (f x))

Theorem 10.0.2. Let f : ℝ^n → ℝ and S ⊆ ℝ^n. Then f is continuous relative to S if and only if for every x ∈ S and every sequence (y_k) ⊆ S with y_k → x, one has f(y_k) → f(x).

theorem convexFunctionOn_continuousOn_of_relOpen_effectiveDomain {n : ℕ} {f : (Fin n → ℝ) → EReal} (hf : ConvexFunctionOn Set.univ f) {C : Set (Fin n → ℝ)} (hCconv : Convex ℝ C) (hCsub : C ⊆ effectiveDomain Set.univ f) (hCrelOpen : euclideanRelativelyOpen n ((fun (x : EuclideanSpace ℝ (Fin n)) => x.ofLp) ⁻¹' C)) : ContinuousOn f C

Theorem 10.1. A convex function f on ℝ^n is continuous relative to any relatively open convex set C in its effective domain, in particular relative to ri (dom f).

theorem convexFunctionOn_continuousOn_relativeInterior_effectiveDomain {n : ℕ} {f : (Fin n → ℝ) → EReal} (hf : ConvexFunctionOn Set.univ f) : ContinuousOn (fun (x : EuclideanSpace ℝ (Fin n)) => f x.ofLp) (euclideanRelativeInterior n ((fun (x : EuclideanSpace ℝ (Fin n)) => x.ofLp) ⁻¹' effectiveDomain Set.univ f))

Theorem 10.1 (in particular). A convex function f on ℝ^n is continuous relative to ri (dom f), where dom f is the effective domain.

theorem effectiveDomain_univ_coe_real {n : ℕ} (f : (Fin n → ℝ) → ℝ) : (effectiveDomain Set.univ fun (x : Fin n → ℝ) => ↑(f x)) = Set.univ

For a real-valued function, coercion to EReal is finite everywhere, hence its effective domain over univ is univ.

theorem euclideanRelativelyOpen_univ (n : ℕ) : euclideanRelativelyOpen n Set.univ

The whole Euclidean space is relatively open in itself (ri univ = univ).

theorem continuous_coe_ereal_iff_continuous {α : Type u_1} [TopologicalSpace α] {f : α → ℝ} : (Continuous fun (a : α) => ↑(f a)) ↔ Continuous f

A real-valued map is continuous iff its coercion to EReal is continuous.

theorem convexFunctionOn_continuous_of_real {n : ℕ} {f : (Fin n → ℝ) → ℝ} (hf : ConvexFunctionOn Set.univ fun (x : Fin n → ℝ) => ↑(f x)) : Continuous f

Corollary 10.1.1. A convex function finite on all of ℝ^n is necessarily continuous.

theorem le_csSup_range_apply {n : ℕ} {T : Type u_1} [Nonempty T] (f : (Fin n → ℝ) → T → ℝ) (hbdd : ∀ (x : Fin n → ℝ), BddAbove (Set.range fun (t : T) => f x t)) (x : Fin n → ℝ) (t : T) : f x t ≤ sSup (Set.range fun (t : T) => f x t)

Any element of a bounded-above range is bounded above by its sSup.

theorem convexOn_sSup_range_of_convexOn {n : ℕ} {T : Type u_1} [Nonempty T] (f : (Fin n → ℝ) → T → ℝ) (hconv : ∀ (t : T), ConvexOn ℝ Set.univ fun (x : Fin n → ℝ) => f x t) (hbdd : ∀ (x : Fin n → ℝ), BddAbove (Set.range fun (t : T) => f x t)) : ConvexOn ℝ Set.univ fun (x : Fin n → ℝ) => sSup (Set.range fun (t : T) => f x t)

The pointwise supremum of a family of convex functions is convex.

theorem continuous_of_convexOn_univ {n : ℕ} {h : (Fin n → ℝ) → ℝ} (hh : ConvexOn ℝ Set.univ h) : Continuous h

A convex real-valued function on all of ℝ^n is continuous.

theorem convexOn_continuous_sSup_range {n : ℕ} {T : Type u_1} [Nonempty T] (f : (Fin n → ℝ) → T → ℝ) (hconv : ∀ (t : T), ConvexOn ℝ Set.univ fun (x : Fin n → ℝ) => f x t) (hbdd : ∀ (x : Fin n → ℝ), BddAbove (Set.range fun (t : T) => f x t)) : have h := fun (x : Fin n → ℝ) => sSup (Set.range fun (t : T) => f x t); ConvexOn ℝ Set.univ h ∧ Continuous h

Theorem 10.1.2. Let T be an arbitrary index set and let f : ℝ^n × T → ℝ be a function such that:

• for each t ∈ T, the function x ↦ f(x,t) is convex on ℝ^n;
• for each x ∈ ℝ^n, the function t ↦ f(x,t) is bounded above on T.

Define h(x) := sup { f(x,t) | t ∈ T }. Then h is a finite convex function on ℝ^n, and h(x) depends continuously on x.

theorem sInf_image_add_nonempty {n : ℕ} {f : (Fin n → ℝ) → ℝ} {C : Set (Fin n → ℝ)} (hCne : C.Nonempty) (x : Fin n → ℝ) : (f '' ((fun (y : Fin n → ℝ) => y + x) '' C)).Nonempty

The inf-set in Theorem 10.1.3 is nonempty.

theorem exists_mem_C_lt_sInf_add {n : ℕ} {f : (Fin n → ℝ) → ℝ} {C : Set (Fin n → ℝ)} (hCne : C.Nonempty) (x : Fin n → ℝ) {ε : ℝ} (hε : 0 < ε) : ∃ y ∈ C, f (y + x) < sInf (f '' ((fun (y : Fin n → ℝ) => y + x) '' C)) + ε

For ε > 0, there is a point in C whose translate is ε-close above the infimum.

theorem convexOn_sInf_image_add_of_bddBelow {n : ℕ} {f : (Fin n → ℝ) → ℝ} (hf : ConvexOn ℝ Set.univ f) {C : Set (Fin n → ℝ)} (hCne : C.Nonempty) (hCconv : Convex ℝ C) (hbdd : ∀ (x : Fin n → ℝ), BddBelow (f '' ((fun (y : Fin n → ℝ) => y + x) '' C))) : ConvexOn ℝ Set.univ fun (x : Fin n → ℝ) => sInf (f '' ((fun (y : Fin n → ℝ) => y + x) '' C))

If all the inf-sets are bounded below, the pointwise infimum of translates of a convex function is convex.

theorem convexOn_continuous_sInf_image_add {n : ℕ} {f : (Fin n → ℝ) → ℝ} (hf : ConvexOn ℝ Set.univ f) {C : Set (Fin n → ℝ)} (hCne : C.Nonempty) (hCconv : Convex ℝ C) (hbdd : ∀ (x : Fin n → ℝ), BddBelow (f '' ((fun (y : Fin n → ℝ) => y + x) '' C))) : have h := fun (x : Fin n → ℝ) => sInf (f '' ((fun (y : Fin n → ℝ) => y + x) '' C)); ConvexOn ℝ Set.univ h ∧ Continuous h

Theorem 10.1.3. Let f : ℝ^n → ℝ be a convex function finite on all of ℝ^n, and let C ⊆ ℝ^n be a nonempty convex set. For each x ∈ ℝ^n, define h(x) := inf {f(y) | y ∈ C + x}.

Then h is convex on ℝ^n, and h depends continuously on x.

noncomputable def quadraticOverLinearEReal (ξ : Fin 2 → ℝ) : EReal

Theorem 10.1.4. Define f : ℝ^2 → (-∞, +∞] by

• f(ξ₁, ξ₂) = ξ₂^2 / (2 ξ₁) if ξ₁ > 0,
• f(0, 0) = 0,
• f(ξ₁, ξ₂) = +∞ otherwise.

Then f is convex with effective domain {(ξ₁, ξ₂) | ξ₁ > 0} ∪ {(0,0)}. Moreover, f is the support function of the convex set C = {(η₁, η₂) | η₁ + η₂^2 / 2 ≤ 0} (i.e. the supremum of ⟪ξ, η⟫ over η ∈ C).

The function is continuous at every point of its effective domain except at (0,0), where it is only lower semicontinuous. In particular, for any α > 0, lim_{t → 0} f(t^2/(2α), t) = α, while lim_{t ↓ 0} f(t • x) = 0 for every x with x₁ > 0.

Equations

• quadraticOverLinearEReal ξ = if ξ 0 > 0 then ↑(ξ 1 ^ 2 / (2 * ξ 0)) else if ξ 0 = 0 ∧ ξ 1 = 0 then 0 else ⊤

def quadraticOverLinearSupportSet : Set (Fin 2 → ℝ)

The convex set C = {(η₁, η₂) | η₁ + η₂^2/2 ≤ 0} appearing in Theorem 10.1.4.

Equations

• quadraticOverLinearSupportSet = {η : Fin 2 → ℝ | η 0 + η 1 ^ 2 / 2 ≤ 0}

theorem dotProduct_fin2 (ξ η : Fin 2 → ℝ) : ξ ⬝ᵥ η = ξ 0 * η 0 + ξ 1 * η 1

Expand dotProduct on Fin 2 as a two-term sum.

def quadraticOverLinearSupportValues (ξ : Fin 2 → ℝ) : Set EReal

The set of dot products ⟪ξ,η⟫ with η ∈ quadraticOverLinearSupportSet, seen in EReal.

Equations

• quadraticOverLinearSupportValues ξ = {z : EReal | ∃ η ∈ quadraticOverLinearSupportSet, z = ↑(ξ ⬝ᵥ η)}

theorem zero_le_quadraticOverLinearEReal (ξ : Fin 2 → ℝ) : 0 ≤ quadraticOverLinearEReal ξ

The quadratic-over-linear function is nonnegative everywhere (as an EReal-valued map).

theorem concave_quadratic_bound {a b t : ℝ} (ha : 0 < a) : -(a / 2) * t ^ 2 + b * t ≤ b ^ 2 / (2 * a)

A completing-the-square bound for a concave quadratic.

theorem quadraticOverLinear_supportSet_dotProduct_le_quadraticBound {ξ η : Fin 2 → ℝ} (hξ : 0 < ξ 0) (hη : η ∈ quadraticOverLinearSupportSet) : ξ ⬝ᵥ η ≤ ξ 1 ^ 2 / (2 * ξ 0)

Upper bound on ⟪ξ,η⟫ when η ∈ quadraticOverLinearSupportSet and ξ₁ > 0.

theorem exists_supportSet_attains_quadraticBound {ξ : Fin 2 → ℝ} (hξ : 0 < ξ 0) : ∃ η ∈ quadraticOverLinearSupportSet, ξ ⬝ᵥ η = ξ 1 ^ 2 / (2 * ξ 0)

For ξ₁ > 0, there is η ∈ quadraticOverLinearSupportSet attaining the quadratic bound.

theorem fin2_eq_zero_iff (ξ : Fin 2 → ℝ) : ξ = 0 ↔ ξ 0 = 0 ∧ ξ 1 = 0

ξ = 0 in Fin 2 → ℝ iff both coordinates are zero.

theorem exists_lt_coe_of_lt_top {b : EReal} (hb : b < ⊤) : ∃ (r : ℝ), b < ↑r

If b < ⊤ in EReal, it is below some real coercion.

theorem sSup_quadraticOverLinearSupportValues_of_pos {ξ : Fin 2 → ℝ} (hξ : 0 < ξ 0) : sSup (quadraticOverLinearSupportValues ξ) = ↑(ξ 1 ^ 2 / (2 * ξ 0))

If ξ₁ > 0, the support supremum equals the quadratic bound.

theorem sSup_quadraticOverLinearSupportValues_zero : sSup (quadraticOverLinearSupportValues 0) = 0

For ξ = 0, the support supremum equals 0.

theorem sSup_quadraticOverLinearSupportValues_eq_top_of_neg {ξ : Fin 2 → ℝ} (hξ : ξ 0 < 0) : sSup (quadraticOverLinearSupportValues ξ) = ⊤

If ξ₁ < 0, the support supremum is ⊤ (unbounded above).

theorem sSup_quadraticOverLinearSupportValues_eq_top_of_zero_ne {ξ : Fin 2 → ℝ} (hξ0 : ξ 0 = 0) (hξ1 : ξ 1 ≠ 0) : sSup (quadraticOverLinearSupportValues ξ) = ⊤

If ξ₁ = 0 and ξ₂ ≠ 0, the support supremum is ⊤ (unbounded above).

theorem sSup_quadraticOverLinearSupportValues (ξ : Fin 2 → ℝ) : sSup (quadraticOverLinearSupportValues ξ) = if ξ 0 > 0 then ↑(ξ 1 ^ 2 / (2 * ξ 0)) else if ξ 0 = 0 ∧ ξ 1 = 0 then 0 else ⊤

Compute the support supremum in closed form.

theorem quadraticOverLinearEReal_eq_supportFunction_aux : quadraticOverLinearEReal = fun (ξ : Fin 2 → ℝ) => sSup (quadraticOverLinearSupportValues ξ)

Support function representation for quadraticOverLinearEReal (as a pointwise equality).

theorem convexFunctionOn_ereal_dotProduct_fixed (η : Fin 2 → ℝ) : ConvexFunctionOn Set.univ fun (ξ : Fin 2 → ℝ) => ↑(ξ ⬝ᵥ η)

For fixed η, the map ξ ↦ ⟪ξ,η⟫ (coerced to EReal) is convex on ℝ^2.

theorem convexFunctionOn_supportFunctionEReal (C : Set (Fin 2 → ℝ)) : ConvexFunctionOn Set.univ fun (ξ : Fin 2 → ℝ) => sSup {z : EReal | ∃ η ∈ C, z = ↑(ξ ⬝ᵥ η)}

The EReal support function ξ ↦ sSup {⟪ξ,η⟫ | η ∈ C} is convex.

theorem convexFunctionOn_quadraticOverLinearEReal : ConvexFunctionOn Set.univ quadraticOverLinearEReal

Theorem 10.1.4 (convexity): the quadratic-over-linear extended-valued function is convex.

theorem effectiveDomain_quadraticOverLinearEReal : effectiveDomain Set.univ quadraticOverLinearEReal = {ξ : Fin 2 → ℝ | ξ 0 > 0} ∪ {0}

Theorem 10.1.4 (effective domain): dom f = {ξ | ξ₁ > 0} ∪ {(0,0)}.

theorem convex_quadraticOverLinearSupportSet : Convex ℝ quadraticOverLinearSupportSet

Theorem 10.1.4 (convex set): C = {(η₁, η₂) | η₁ + η₂^2/2 ≤ 0} is convex.

theorem quadraticOverLinearEReal_eq_supportFunction : quadraticOverLinearEReal = fun (ξ : Fin 2 → ℝ) => sSup {z : EReal | ∃ η ∈ quadraticOverLinearSupportSet, z = ↑(ξ ⬝ᵥ η)}

Theorem 10.1.4 (support function): f is the support function of C.

theorem continuousAt_quadraticOverLinearEReal_of_mem_effectiveDomain {x : Fin 2 → ℝ} (hx : x ∈ effectiveDomain Set.univ quadraticOverLinearEReal) (hx0 : x ≠ 0) : ContinuousAt quadraticOverLinearEReal x

Theorem 10.1.4 (continuity away from (0,0)): f is continuous at every nonzero point of its effective domain.