mathlib documentation

analysis.normed_space.add_torsor_bases

Bases in normed affine spaces. #

This file contains results about bases in normed affine spaces.

Main definitions: #

source
theorem is_open_map_barycentric_coord {ΞΉ : Type u_1} {π•œ : Type u_2} {E : Type u_3} {P : Type u_4} [nontrivially_normed_field π•œ] [complete_space π•œ] [normed_add_comm_group E] [normed_space π•œ E] [metric_space P] [normed_add_torsor E P] [nontrivial ΞΉ] (b : affine_basis ΞΉ π•œ P) (i : ΞΉ) :
is_open_map ⇑(b.coord i)
source
@[continuity]
theorem continuous_barycentric_coord {ΞΉ : Type u_1} {π•œ : Type u_2} {E : Type u_3} {P : Type u_4} [nontrivially_normed_field π•œ] [complete_space π•œ] [normed_add_comm_group E] [normed_space π•œ E] [metric_space P] [normed_add_torsor E P] [finite_dimensional π•œ E] (b : affine_basis ΞΉ π•œ P) (i : ΞΉ) :
continuous ⇑(b.coord i)
source
theorem smooth_barycentric_coord {ΞΉ : Type u_1} {π•œ : Type u_2} {E : Type u_3} [nontrivially_normed_field π•œ] [complete_space π•œ] [normed_add_comm_group E] [normed_space π•œ E] [finite_dimensional π•œ E] (b : affine_basis ΞΉ π•œ E) (i : ΞΉ) :
cont_diff π•œ ⊀ ⇑(b.coord i)
source
theorem affine_basis.interior_convex_hull {ΞΉ : Type u_1} {E : Type u_2} [finite ΞΉ] [normed_add_comm_group E] [normed_space ℝ E] (b : affine_basis ΞΉ ℝ E) :
interior (⇑(convex_hull ℝ) (set.range ⇑b)) = {x : E | βˆ€ (i : ΞΉ), 0 < ⇑(b.coord i) x}

Given a finite-dimensional normed real vector space, the interior of the convex hull of an affine basis is the set of points whose barycentric coordinates are strictly positive with respect to this basis.

TODO Restate this result for affine spaces (instead of vector spaces) once the definition of convexity is generalised to this setting.

source
theorem is_open.exists_between_affine_independent_span_eq_top {V : Type u_1} {P : Type u_2} [normed_add_comm_group V] [normed_space ℝ V] [metric_space P] [normed_add_torsor V P] {s u : set P} (hu : is_open u) (hsu : s βŠ† u) (hne : s.nonempty) (h : affine_independent ℝ coe) :
βˆƒ (t : set P), s βŠ† t ∧ t βŠ† u ∧ affine_independent ℝ coe ∧ affine_span ℝ t = ⊀

Given a set s of affine-independent points belonging to an open set u, we may extend s to an affine basis, all of whose elements belong to u.

source
theorem is_open.exists_subset_affine_independent_span_eq_top {V : Type u_1} {P : Type u_2} [normed_add_comm_group V] [normed_space ℝ V] [metric_space P] [normed_add_torsor V P] {u : set P} (hu : is_open u) (hne : u.nonempty) :
βˆƒ (s : set P) (H : s βŠ† u), affine_independent ℝ coe ∧ affine_span ℝ s = ⊀
source
theorem is_open.affine_span_eq_top {V : Type u_1} {P : Type u_2} [normed_add_comm_group V] [normed_space ℝ V] [metric_space P] [normed_add_torsor V P] {u : set P} (hu : is_open u) (hne : u.nonempty) :
affine_span ℝ u = ⊀

The affine span of a nonempty open set is ⊀.

source
theorem affine_span_eq_top_of_nonempty_interior {V : Type u_1} [normed_add_comm_group V] [normed_space ℝ V] {s : set V} (hs : (interior (⇑(convex_hull ℝ) s)).nonempty) :
affine_span ℝ s = ⊀
source
theorem affine_basis.centroid_mem_interior_convex_hull {V : Type u_1} [normed_add_comm_group V] [normed_space ℝ V] {ΞΉ : Type u_2} [fintype ΞΉ] (b : affine_basis ΞΉ ℝ V) :
finset.centroid ℝ finset.univ ⇑b ∈ interior (⇑(convex_hull ℝ) (set.range ⇑b))
source
theorem interior_convex_hull_nonempty_iff_affine_span_eq_top {V : Type u_1} [normed_add_comm_group V] [normed_space ℝ V] [finite_dimensional ℝ V] {s : set V} :
(interior (⇑(convex_hull ℝ) s)).nonempty ↔ affine_span ℝ s = ⊀
source
theorem convex.interior_nonempty_iff_affine_span_eq_top {V : Type u_1} [normed_add_comm_group V] [normed_space ℝ V] [finite_dimensional ℝ V] {s : set V} (hs : convex ℝ s) :
(interior s).nonempty ↔ affine_span ℝ s = ⊀