theorem lowerSemicontinuousAt_quadraticOverLinearEReal_zero : LowerSemicontinuousAt quadraticOverLinearEReal 0

Theorem 10.1.4 (lower semicontinuity at (0,0)).

theorem tendsto_quadraticOverLinearEReal_along_parabola_aux {α : ℝ} (hα : 0 < α) : Filter.Tendsto (fun (t : ℝ) => quadraticOverLinearEReal ![t ^ 2 / (2 * α), t]) (nhdsWithin 0 {0}ᶜ) (nhds ↑α)

Theorem 10.1.4 (path limit, auxiliary): for α > 0, along the parabola and excluding t = 0, the values tend to α.

theorem not_continuousAt_quadraticOverLinearEReal_zero : ¬ContinuousAt quadraticOverLinearEReal 0

Theorem 10.1.4 (failure of continuity at (0,0)).

theorem tendsto_quadraticOverLinearEReal_along_parabola {α : ℝ} (hα : 0 < α) : Filter.Tendsto (fun (t : ℝ) => quadraticOverLinearEReal ![t ^ 2 / (2 * α), t]) (nhdsWithin 0 {0}ᶜ) (nhds ↑α)

Theorem 10.1.4 (path limit): for any α > 0, lim_{t → 0} f(t^2/(2α), t) = α.

theorem tendsto_quadraticOverLinearEReal_smul_of_pos {x : Fin 2 → ℝ} (hx : x 0 > 0) : Filter.Tendsto (fun (t : ℝ) => quadraticOverLinearEReal (t • x)) (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)

Theorem 10.1.4 (path limit): for x₁ > 0, lim_{t ↓ 0} f(t • x) = 0.

def Set.LocallySimplicial (n : ℕ) (S : Set (Fin n → ℝ)) : Prop

Definition 10.1.5. A subset S ⊆ ℝ^n is locally simplicial if for each x ∈ S there exist finitely many simplices S₁, …, Sₘ ⊆ S and a neighborhood U of x such that U ∩ (S₁ ∪ ⋯ ∪ Sₘ) = U ∩ S.

Equations

• Set.LocallySimplicial n S = ∀ x ∈ S, ∃ (𝒮 : Set (Set (Fin n → ℝ))) (U : Set (Fin n → ℝ)), 𝒮.Finite ∧ U ∈ nhds x ∧ (∀ P ∈ 𝒮, ∃ (m : ℕ), IsSimplex n m P ∧ P ⊆ S) ∧ U ∩ ⋃₀ 𝒮 = U ∩ S

theorem range_update_eq_insert_range_succAbove {n m : ℕ} (b : Fin (m + 1) → Fin n → ℝ) (j : Fin (m + 1)) (x : Fin n → ℝ) : Set.range (Function.update b j x) = Set.insert x (Set.range fun (i : Fin m) => b (j.succAbove i))

Replacing b j by x produces exactly the vertex set {x} ∪ {b (succAbove j i) | i : Fin m}.

theorem exists_index_min_ratio_barycentric {m : ℕ} {μ ν : Fin (m + 1) → ℝ} (hμ0 : ∀ (i : Fin (m + 1)), 0 ≤ μ i) (hμ1 : ∑ i : Fin (m + 1), μ i = 1) (hν0 : ∀ (i : Fin (m + 1)), 0 ≤ ν i) : ∃ (j : Fin (m + 1)), 0 < μ j ∧ ∀ (i : Fin (m + 1)), ν j * μ i ≤ ν i * μ j

Given two barycentric weight functions μ and ν with μ ≥ 0 and ∑ μ = 1, choose an index j with μ j > 0 minimizing ν i / μ i among μ i > 0. The resulting j satisfies the cross-multiplied inequalities ν j * μ i ≤ ν i * μ j.

theorem not_mem_affineSpan_facet_of_barycentric_weight_pos {n m : ℕ} {b : Fin (m + 1) → Fin n → ℝ} (hb : AffineIndependent ℝ b) {x : Fin n → ℝ} {μ : Fin (m + 1) → ℝ} (hμ1 : ∑ i : Fin (m + 1), μ i = 1) (hx : x = ∑ i : Fin (m + 1), μ i • b i) {j : Fin (m + 1)} (hμj : 0 < μ j) : x ∉ affineSpan ℝ (b '' {i : Fin (m + 1) | i ≠ j})

If x is an affine combination of an affinely independent family b with a positive weight at j, then x does not lie in the affine span of the other vertices.

theorem mem_cone_facet_of_min_ratio {n m : ℕ} {b : Fin (m + 1) → Fin n → ℝ} {x y : Fin n → ℝ} {μ ν : Fin (m + 1) → ℝ} (hμ1 : ∑ i : Fin (m + 1), μ i = 1) (hν0 : ∀ (i : Fin (m + 1)), 0 ≤ ν i) (hν1 : ∑ i : Fin (m + 1), ν i = 1) (hx : x = ∑ i : Fin (m + 1), μ i • b i) (hy : y = ∑ i : Fin (m + 1), ν i • b i) {j : Fin (m + 1)} (hμj : 0 < μ j) (hcross : ∀ (i : Fin (m + 1)), ν j * μ i ≤ ν i * μ j) : y ∈ (convexHull ℝ) (Set.insert x (Set.range fun (i : Fin m) => b (j.succAbove i)))

If x and y have barycentric coordinates μ and ν in a simplex, and j is chosen by the min-ratio condition, then y lies in the convex hull of x and the facet opposite j.

theorem isSimplex_cone_over_facet {n m : ℕ} {b : Fin (m + 1) → Fin n → ℝ} (hb : AffineIndependent ℝ b) {x : Fin n → ℝ} {μ : Fin (m + 1) → ℝ} (hμ1 : ∑ i : Fin (m + 1), μ i = 1) (hx : x = ∑ i : Fin (m + 1), μ i • b i) {j : Fin (m + 1)} (hμj : 0 < μ j) : have P := (convexHull ℝ) (Set.insert x (Set.range fun (i : Fin m) => b (j.succAbove i))); IsSimplex n m P

The convex hull of x and a facet of an m-simplex is again an m-simplex, provided x is not in the affine span of that facet.

theorem simplex_exists_subsimplex_through_point {n m : ℕ} {C : Set (Fin n → ℝ)} {x : Fin n → ℝ} (hC : IsSimplex n m C) (hx : x ∈ C) : ∃ (b : Fin (m + 1) → Fin n → ℝ), AffineIndependent ℝ b ∧ C = (convexHull ℝ) (Set.range b) ∧ ∀ y ∈ C, ∃ (j : Fin (m + 1)), have P := (convexHull ℝ) (Set.insert x (Set.range fun (i : Fin m) => b (j.succAbove i))); P ⊆ C ∧ IsSimplex n m P ∧ x ∈ P ∧ y ∈ P

Theorem 10.1.6. Let C ⊆ ℝ^n be a simplex with vertices x₀, x₁, …, x_m, and let x ∈ C. Then C can be triangulated into finitely many simplices having x as a vertex. More precisely, for every y ∈ C there exists a simplex P ⊆ C whose vertices consist of x together with m of the m+1 vertices of C, and such that y ∈ P.

theorem upperSemicontinuousWithinAt_union {α : Type u_1} [TopologicalSpace α] {β : Type u_2} [Preorder β] {f : α → β} {s t : Set α} {x : α} : UpperSemicontinuousWithinAt f s x → UpperSemicontinuousWithinAt f t x → UpperSemicontinuousWithinAt f (s ∪ t) x

Upper semicontinuity within a finite union (binary case).

theorem upperSemicontinuousWithinAt_sUnion_of_finite {α : Type u_1} [TopologicalSpace α] {β : Type u_2} [Preorder β] {f : α → β} {x : α} {𝒮 : Set (Set α)} (h𝒮 : 𝒮.Finite) (husc : ∀ s ∈ 𝒮, UpperSemicontinuousWithinAt f s x) : UpperSemicontinuousWithinAt f (⋃₀ 𝒮) x

Upper semicontinuity within a sUnion of finitely many sets.

theorem upperSemicontinuousWithinAt_congr_of_local_eq {α : Type u_1} [TopologicalSpace α] {β : Type u_2} [Preorder β] {f : α → β} {s t U : Set α} {x : α} (hU : U ∈ nhds x) (hEq : U ∩ s = U ∩ t) : UpperSemicontinuousWithinAt f s x ↔ UpperSemicontinuousWithinAt f t x

Upper semicontinuity withinAt is invariant under local equality of the underlying set.

theorem Section10.convexFunctionOn_le_affineCombination_real {n : ℕ} {ι : Type u_1} {f : (Fin n → ℝ) → EReal} (hf : ConvexFunctionOn Set.univ f) (s : Finset ι) (x : ι → Fin n → ℝ) (μ w : ι → ℝ) (hμ : ∀ i ∈ s, f (x i) ≤ ↑(μ i)) (hw0 : ∀ i ∈ s, 0 ≤ w i) (hw1 : s.sum w = 1) : f ((Finset.affineCombination ℝ s x) w) ≤ ↑(∑ i ∈ s, w i * μ i)

A finite affine-combination inequality from epigraph convexity: if f (x i) ≤ μ i for i ∈ s, then f at the affine combination is bounded above by the real affine combination of the μ i.

theorem Section10.simplex_real_upper_bound_of_dom {n m : ℕ} {f : (Fin n → ℝ) → EReal} (hf : ConvexFunctionOn Set.univ f) {P : Set (Fin n → ℝ)} (hP : IsSimplex n m P) (hPdom : P ⊆ effectiveDomain Set.univ f) : ∃ (M : ℝ), ∀ z ∈ P, f z ≤ ↑M

A simplex contained in the effective domain admits a uniform real upper bound.

noncomputable def Section10.simplex_affineBasis_on_affineSpan {n m : ℕ} {b : Fin (m + 1) → Fin n → ℝ} (hb : AffineIndependent ℝ b) : AffineBasis (Fin (m + 1)) ℝ ↥(affineSpan ℝ (Set.range b))

Given an affinely independent family of vertices, build an AffineBasis for their affine span.

Equations

• Section10.simplex_affineBasis_on_affineSpan hb = { toFun := fun (i : Fin (m + 1)) => ⟨b i, ⋯⟩, ind' := ⋯, tot' := ⋯ }

theorem Section10.vertex_coord_eventually_gt {n m : ℕ} {b : Fin (m + 1) → Fin n → ℝ} (hb : AffineIndependent ℝ b) (j : Fin (m + 1)) {δ : ℝ} (hδ : 0 < δ) : ∀ᶠ (z : { z : Fin n → ℝ // z ∈ (convexHull ℝ) (Set.range b) }) in nhds ⟨b j, ⋯⟩, 1 - δ < ((simplex_affineBasis_on_affineSpan hb).coord j) ⟨↑z, ⋯⟩

In the relative topology of a simplex, the barycentric coordinate at a vertex tends to 1.