-
Notifications
You must be signed in to change notification settings - Fork 307
/
AddTorsorBases.lean
159 lines (134 loc) · 7.85 KB
/
AddTorsorBases.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
/-
Copyright (c) 2021 Oliver Nash. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Oliver Nash
-/
import Mathlib.Analysis.NormedSpace.FiniteDimension
import Mathlib.Analysis.Calculus.AffineMap
import Mathlib.Analysis.Convex.Combination
import Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
#align_import analysis.normed_space.add_torsor_bases from "leanprover-community/mathlib"@"2f4cdce0c2f2f3b8cd58f05d556d03b468e1eb2e"
/-!
# Bases in normed affine spaces.
This file contains results about bases in normed affine spaces.
## Main definitions:
* `continuous_barycentric_coord`
* `isOpenMap_barycentric_coord`
* `AffineBasis.interior_convexHull`
* `IsOpen.exists_subset_affineIndependent_span_eq_top`
* `interior_convexHull_nonempty_iff_affineSpan_eq_top`
-/
section Barycentric
variable {ι 𝕜 E P : Type*} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜]
variable [NormedAddCommGroup E] [NormedSpace 𝕜 E]
variable [MetricSpace P] [NormedAddTorsor E P]
theorem isOpenMap_barycentric_coord [Nontrivial ι] (b : AffineBasis ι 𝕜 P) (i : ι) :
IsOpenMap (b.coord i) :=
AffineMap.isOpenMap_linear_iff.mp <|
(b.coord i).linear.isOpenMap_of_finiteDimensional <|
(b.coord i).linear_surjective_iff.mpr (b.surjective_coord i)
#align is_open_map_barycentric_coord isOpenMap_barycentric_coord
variable [FiniteDimensional 𝕜 E] (b : AffineBasis ι 𝕜 P)
@[continuity]
theorem continuous_barycentric_coord (i : ι) : Continuous (b.coord i) :=
(b.coord i).continuous_of_finiteDimensional
#align continuous_barycentric_coord continuous_barycentric_coord
theorem smooth_barycentric_coord (b : AffineBasis ι 𝕜 E) (i : ι) : ContDiff 𝕜 ⊤ (b.coord i) :=
(⟨b.coord i, continuous_barycentric_coord b i⟩ : E →A[𝕜] 𝕜).contDiff
#align smooth_barycentric_coord smooth_barycentric_coord
end Barycentric
open Set
/-- 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 AffineBasis.interior_convexHull {ι E : Type*} [Finite ι] [NormedAddCommGroup E]
[NormedSpace ℝ E] (b : AffineBasis ι ℝ E) :
interior (convexHull ℝ (range b)) = {x | ∀ i, 0 < b.coord i x} := by
cases subsingleton_or_nontrivial ι
· -- The zero-dimensional case.
have : range b = univ :=
AffineSubspace.eq_univ_of_subsingleton_span_eq_top (subsingleton_range _) b.tot
simp [this]
· -- The positive-dimensional case.
haveI : FiniteDimensional ℝ E := b.finiteDimensional
have : convexHull ℝ (range b) = ⋂ i, b.coord i ⁻¹' Ici 0 := by
rw [b.convexHull_eq_nonneg_coord, setOf_forall]; rfl
ext
simp only [this, interior_iInter_of_finite, ←
IsOpenMap.preimage_interior_eq_interior_preimage (isOpenMap_barycentric_coord b _)
(continuous_barycentric_coord b _),
interior_Ici, mem_iInter, mem_setOf_eq, mem_Ioi, mem_preimage]
#align affine_basis.interior_convex_hull AffineBasis.interior_convexHull
variable {V P : Type*} [NormedAddCommGroup V] [NormedSpace ℝ V] [MetricSpace P]
[NormedAddTorsor V P]
open AffineMap
/-- 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_between_affineIndependent_span_eq_top {s u : Set P} (hu : IsOpen u)
(hsu : s ⊆ u) (hne : s.Nonempty) (h : AffineIndependent ℝ ((↑) : s → P)) :
∃ t : Set P, s ⊆ t ∧ t ⊆ u ∧ AffineIndependent ℝ ((↑) : t → P) ∧ affineSpan ℝ t = ⊤ := by
obtain ⟨q, hq⟩ := hne
obtain ⟨ε, ε0, hεu⟩ := Metric.nhds_basis_closedBall.mem_iff.1 (hu.mem_nhds <| hsu hq)
obtain ⟨t, ht₁, ht₂, ht₃⟩ := exists_subset_affineIndependent_affineSpan_eq_top h
let f : P → P := fun y => lineMap q y (ε / dist y q)
have hf : ∀ y, f y ∈ u := by
refine' fun y => hεu _
simp only [f]
rw [Metric.mem_closedBall, lineMap_apply, dist_vadd_left, norm_smul, Real.norm_eq_abs,
dist_eq_norm_vsub V y q, abs_div, abs_of_pos ε0, abs_of_nonneg (norm_nonneg _), div_mul_comm]
exact mul_le_of_le_one_left ε0.le (div_self_le_one _)
have hεyq : ∀ y ∉ s, ε / dist y q ≠ 0 := fun y hy =>
div_ne_zero ε0.ne' (dist_ne_zero.2 (ne_of_mem_of_not_mem hq hy).symm)
classical
let w : t → ℝˣ := fun p => if hp : (p : P) ∈ s then 1 else Units.mk0 _ (hεyq (↑p) hp)
refine' ⟨Set.range fun p : t => lineMap q p (w p : ℝ), _, _, _, _⟩
· intro p hp; use ⟨p, ht₁ hp⟩; simp [w, hp]
· rintro y ⟨⟨p, hp⟩, rfl⟩
by_cases hps : p ∈ s <;>
simp only [w, hps, lineMap_apply_one, Units.val_mk0, dif_neg, dif_pos, not_false_iff,
Units.val_one, Subtype.coe_mk] <;>
[exact hsu hps; exact hf p]
· exact (ht₂.units_lineMap ⟨q, ht₁ hq⟩ w).range
· rw [affineSpan_eq_affineSpan_lineMap_units (ht₁ hq) w, ht₃]
#align is_open.exists_between_affine_independent_span_eq_top IsOpen.exists_between_affineIndependent_span_eq_top
theorem IsOpen.exists_subset_affineIndependent_span_eq_top {u : Set P} (hu : IsOpen u)
(hne : u.Nonempty) : ∃ s ⊆ u, AffineIndependent ℝ ((↑) : s → P) ∧ affineSpan ℝ s = ⊤ := by
rcases hne with ⟨x, hx⟩
rcases hu.exists_between_affineIndependent_span_eq_top (singleton_subset_iff.mpr hx)
(singleton_nonempty _) (affineIndependent_of_subsingleton _ _) with ⟨s, -, hsu, hs⟩
exact ⟨s, hsu, hs⟩
#align is_open.exists_subset_affine_independent_span_eq_top IsOpen.exists_subset_affineIndependent_span_eq_top
/-- The affine span of a nonempty open set is `⊤`. -/
theorem IsOpen.affineSpan_eq_top {u : Set P} (hu : IsOpen u) (hne : u.Nonempty) :
affineSpan ℝ u = ⊤ :=
let ⟨_, hsu, _, hs'⟩ := hu.exists_subset_affineIndependent_span_eq_top hne
top_unique <| hs' ▸ affineSpan_mono _ hsu
#align is_open.affine_span_eq_top IsOpen.affineSpan_eq_top
theorem affineSpan_eq_top_of_nonempty_interior {s : Set V}
(hs : (interior <| convexHull ℝ s).Nonempty) : affineSpan ℝ s = ⊤ :=
top_unique <| isOpen_interior.affineSpan_eq_top hs ▸
(affineSpan_mono _ interior_subset).trans_eq (affineSpan_convexHull _)
#align affine_span_eq_top_of_nonempty_interior affineSpan_eq_top_of_nonempty_interior
theorem AffineBasis.centroid_mem_interior_convexHull {ι} [Fintype ι] (b : AffineBasis ι ℝ V) :
Finset.univ.centroid ℝ b ∈ interior (convexHull ℝ (range b)) := by
haveI := b.nonempty
simp only [b.interior_convexHull, mem_setOf_eq, b.coord_apply_centroid (Finset.mem_univ _),
inv_pos, Nat.cast_pos, Finset.card_pos, Finset.univ_nonempty, forall_true_iff]
#align affine_basis.centroid_mem_interior_convex_hull AffineBasis.centroid_mem_interior_convexHull
theorem interior_convexHull_nonempty_iff_affineSpan_eq_top [FiniteDimensional ℝ V] {s : Set V} :
(interior (convexHull ℝ s)).Nonempty ↔ affineSpan ℝ s = ⊤ := by
refine' ⟨affineSpan_eq_top_of_nonempty_interior, fun h => _⟩
obtain ⟨t, hts, b, hb⟩ := AffineBasis.exists_affine_subbasis h
suffices (interior (convexHull ℝ (range b))).Nonempty by
rw [hb, Subtype.range_coe_subtype, setOf_mem_eq] at this
refine' this.mono _
mono*
lift t to Finset V using b.finite_set
exact ⟨_, b.centroid_mem_interior_convexHull⟩
#align interior_convex_hull_nonempty_iff_affine_span_eq_top interior_convexHull_nonempty_iff_affineSpan_eq_top
theorem Convex.interior_nonempty_iff_affineSpan_eq_top [FiniteDimensional ℝ V] {s : Set V}
(hs : Convex ℝ s) : (interior s).Nonempty ↔ affineSpan ℝ s = ⊤ := by
rw [← interior_convexHull_nonempty_iff_affineSpan_eq_top, hs.convexHull_eq]
#align convex.interior_nonempty_iff_affine_span_eq_top Convex.interior_nonempty_iff_affineSpan_eq_top