Bases in normed affine spaces. #
This file contains results about bases in normed affine spaces.
Main definitions: #
theorem
isOpenMap_barycentric_coord
{ι : Type u_1}
{𝕜 : Type u_2}
{E : Type u_3}
{P : Type u_4}
[NontriviallyNormedField 𝕜]
[CompleteSpace 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[MetricSpace P]
[NormedAddTorsor E P]
[Nontrivial ι]
(b : AffineBasis ι 𝕜 P)
(i : ι)
:
IsOpenMap ⇑(AffineBasis.coord b i)
theorem
continuous_barycentric_coord
{ι : Type u_1}
{𝕜 : Type u_2}
{E : Type u_3}
{P : Type u_4}
[NontriviallyNormedField 𝕜]
[CompleteSpace 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[MetricSpace P]
[NormedAddTorsor E P]
[FiniteDimensional 𝕜 E]
(b : AffineBasis ι 𝕜 P)
(i : ι)
:
Continuous ⇑(AffineBasis.coord b i)
theorem
smooth_barycentric_coord
{ι : Type u_1}
{𝕜 : Type u_2}
{E : Type u_3}
[NontriviallyNormedField 𝕜]
[CompleteSpace 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[FiniteDimensional 𝕜 E]
(b : AffineBasis ι 𝕜 E)
(i : ι)
:
ContDiff 𝕜 ⊤ ⇑(AffineBasis.coord b i)
theorem
AffineBasis.interior_convexHull
{ι : Type u_1}
{E : Type u_2}
[Finite ι]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
(b : AffineBasis ι ℝ E)
:
interior ((convexHull ℝ) (Set.range ⇑b)) = {x : E | ∀ (i : ι), 0 < (AffineBasis.coord b 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.
theorem
IsOpen.exists_between_affineIndependent_span_eq_top
{V : Type u_1}
{P : Type u_2}
[NormedAddCommGroup V]
[NormedSpace ℝ V]
[MetricSpace P]
[NormedAddTorsor V P]
{s : Set P}
{u : Set P}
(hu : IsOpen u)
(hsu : s ⊆ u)
(hne : Set.Nonempty s)
(h : AffineIndependent ℝ Subtype.val)
:
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.
theorem
IsOpen.exists_subset_affineIndependent_span_eq_top
{V : Type u_1}
{P : Type u_2}
[NormedAddCommGroup V]
[NormedSpace ℝ V]
[MetricSpace P]
[NormedAddTorsor V P]
{u : Set P}
(hu : IsOpen u)
(hne : Set.Nonempty u)
:
∃ s ⊆ u, AffineIndependent ℝ Subtype.val ∧ affineSpan ℝ s = ⊤
theorem
IsOpen.affineSpan_eq_top
{V : Type u_1}
{P : Type u_2}
[NormedAddCommGroup V]
[NormedSpace ℝ V]
[MetricSpace P]
[NormedAddTorsor V P]
{u : Set P}
(hu : IsOpen u)
(hne : Set.Nonempty u)
:
affineSpan ℝ u = ⊤
The affine span of a nonempty open set is ⊤.
theorem
affineSpan_eq_top_of_nonempty_interior
{V : Type u_1}
[NormedAddCommGroup V]
[NormedSpace ℝ V]
{s : Set V}
(hs : Set.Nonempty (interior ((convexHull ℝ) s)))
:
affineSpan ℝ s = ⊤
theorem
AffineBasis.centroid_mem_interior_convexHull
{V : Type u_1}
[NormedAddCommGroup V]
[NormedSpace ℝ V]
{ι : Type u_3}
[Fintype ι]
(b : AffineBasis ι ℝ V)
:
Finset.centroid ℝ Finset.univ ⇑b ∈ interior ((convexHull ℝ) (Set.range ⇑b))
theorem
interior_convexHull_nonempty_iff_affineSpan_eq_top
{V : Type u_1}
[NormedAddCommGroup V]
[NormedSpace ℝ V]
[FiniteDimensional ℝ V]
{s : Set V}
:
Set.Nonempty (interior ((convexHull ℝ) s)) ↔ affineSpan ℝ s = ⊤
theorem
Convex.interior_nonempty_iff_affineSpan_eq_top
{V : Type u_1}
[NormedAddCommGroup V]
[NormedSpace ℝ V]
[FiniteDimensional ℝ V]
{s : Set V}
(hs : Convex ℝ s)
:
Set.Nonempty (interior s) ↔ affineSpan ℝ s = ⊤