Add proof of lem:smooth_surrounding

blueprint/src/loops.tex

@@ -271,55 +271,41 @@ \section{Preliminaries}
 \end{lemma}
 
 \begin{proof}
-  If $d = 0$ then there is nothing to prove.
-  Hence we will assume $d ≥ 1$.
-  Components of elements of $E^{d+1}$ or $ℝ^{d+1}$ will always be
-  numbered from $0$ to $d$.
-  By assumption, the family of points $p_i$ is affinely independent and
-  there are weights $w_0, \dots, w_d$ such that $x = \sum_i w_i p_i$
-  where each $w_i$ is in $(0, 1)$ and their sum is one.
-  In particular
+  \leanok
+  Let:
+  \begin{align*}
+    A = E \times \{ q \in E^{d+1} ~|~ \mbox{$q$ is an affine basis for $E$} \},
+  \end{align*}
+  and define:
+  \begin{align*}
+    w : A &\to ℝ^{d+1}\\
+    (y, q) &\mapsto \mbox{barycentric coordinates of $y$ with respect to $q$}.
+  \end{align*}
 
+  If we fix an affine basis $b$ of $E$, we may express $w$ as a
+  ratio of determinants in terms of coordinates relative to $b$. More precisely,
+  by Cramer's rule, if $0 \le i \le d$ and $w_i$ is the $i^{\rm th}$ component of $w$,
+  then:
   \begin{align*}
-    x - p_0 &= \sum_{i=0}^d w_i p_i - \sum_{i=0}^d w_i p_0 \\
-            & = \sum_{i=0}^d w_i (p_i - p_0) \\
-            & = \sum_{i=1}^d w_i (p_i - p_0).
+    w_i (y, q) = \det M_i (y, q) / \det N (q)
   \end{align*}
+  where $N(q)$ is the $(d+1)\times (d+1)$ matrix whose columns are the barycentric
+  coordinates of the components of $q$ relative to $b$, and $M_i (y, q)$ is $N(q)$
+  except with column $i$ replaced by the barycentric coordinates of $y$ relative
+  to $b$.
 
-  For $q$ in $E^{d+1}$ and $i ∈ \{1, \dots, d\}$, we set
-  $e_i(q) = q_i - q_0$.
-  Since $p$ is a collection of $d+1$ affinely independent points,
-  the family $e_i(p)$ is a basis of $e$.
-  By continuity of the determinant, this stays true
-  for $q$ in $Π_i B_δ(p_i)$ for some positive $δ$.
-  Let $e^*_i(q)$ denote the elements of the dual basis.
-  In order to prove continuity of these maps and define them
-  for every $q$, we fix a basis $B$ of $E$ and the corresponding
-  determinant $\det_B : E^d → ℝ$.
-  We set $δ(q) = \det_B(e(q))$ and define
-  \[
-    e^*_i(q) = v ↦
-    \det_B(e_1(q), \dots, e_{i-1}(q), v, e_{i+1}(q), \dots, e_d(q))/δ(q).
-  \]
-  which should be interpreted as the zero linear form if $δ(q) = 0$
-  (this interpretation is automatic if division by zero in $ℝ$
-  is defined as zero, as it should be).
-  The map $q ↦ e^*_i(q)$ is smooth on $Π_i B_δ(p_i)$
-  where $δ$ does not vanish since the determinant is polynomial.
-  We set $w_i(y, q) = e^*_i(q)(y - q_0)$.
-  The computation of $x - p_0$ above proves that
-  $w_i(x, p) = w_i$.
-  We have $y - q_0 = \sum_{i = 1}^d w_i(y, q)(q_i - q_0)$.
-  Hence
-  \[
-    y = \left(1 - \sum_{i = 1}^d w_i(y, q)\right)q_0 +
-        \sum_{i = 1}^d w_i(y, q)q_i.
-  \]
-  We denote by $w_0(y, q)$ the coefficient in front of $q_0$ in the
-  above formula.
-  Hence we have $y = \sum_{i=0}^d w_i(y, q)q_i$ with
-  $w_i(x, p) = w_i$ hence $\sum_{i=0}^d w_i(y, q) = 1$ and each $w_i(y, q) > 0$
-  if $(y, q)$ is sufficiently close to $(x, p)$.
+  Since determinants are smooth functions and $(y, q) \mapsto \det N(q)$ is
+  non-vanishing on $A$, $w$ is smooth on $A$.
+
+  Finally define:
+  \begin{align*}
+    U = w^{-1}((0, \infty)^{d+1}),
+  \end{align*}
+  and note that $U$ is open in $A$, since it is the preimage of an open set under the
+  continuous map $w$. In fact since $A$ is open, $U$ is open as a subset of $E \times E^{d+1}$.
+  Note that $(x, p) \in U$ since $p$ surrounds $x$.
+
+  We may extend $w$ to $E \times E^{d+1}$ by giving it any values at all outside $A$.
 \end{proof}
 
 \section{Constructing loops}

src/loops/basic.lean

@@ -8,8 +8,9 @@ import topology.path_connected
 import linear_algebra.affine_space.independent
 
 import loops.homotheties
+import loops.smooth_barycentric
 import to_mathlib.topology.misc
-
+import to_mathlib.linear_algebra.affine_space.basis
 
 /-!
 # Basic definitions and properties of loops
@@ -26,6 +27,7 @@ variables {E : Type*} [normed_group E] [normed_space ℝ E]
           {F' : Type*} [normed_group F'] [normed_space ℝ F'] --[finite_dimensional ℝ F']
 
 local notation `d` := finrank ℝ F
+local notation `ι` := fin (d + 1)
 
 local notation `smooth_on` := times_cont_diff_on ℝ ⊤
 
@@ -66,12 +68,27 @@ section surrounding_points
 /-- `p` is a collection of points surrounding `f` with weights `w` (that are positive and sum to 1)
 if the weighted average of the points `p` is `f` and the points `p` form an affine basis of the
 space. -/
-structure surrounding_pts (f : F) (p : fin (d + 1) → F) (w : fin (d + 1) → ℝ) : Prop :=
+structure surrounding_pts (f : F) (p : ι → F) (w : ι → ℝ) : Prop :=
 (indep : affine_independent ℝ p)
 (w_pos : ∀ i, 0 < w i)
 (w_sum : ∑ i, w i = 1)
 (avg : ∑ i, w i • p i = f)
 
+lemma surrounding_pts.tot [finite_dimensional ℝ F]
+  {f : F} {p : ι → F} {w : ι → ℝ} (h : surrounding_pts f p w) :
+  affine_span ℝ (range p) = ⊤ :=
+h.indep.affine_span_eq_top_iff_card_eq_finrank_add_one.mpr (fintype.card_fin _)
+
+lemma surrounding_pts.coord_eq_w [finite_dimensional ℝ F]
+  {f : F} {p : ι → F} {w : ι → ℝ} (h : surrounding_pts f p w) :
+  (⟨p, h.indep, h.tot⟩ : affine_basis ι ℝ F).coords f = w :=
+begin
+  ext i,
+  conv_lhs { congr, skip, rw ← h.avg, },
+  rw [← finset.univ.affine_combination_eq_linear_combination _ w h.w_sum, affine_basis.coords_apply],
+  exact affine_basis.coord_apply_combination_of_mem _ (finset.mem_univ i) h.w_sum,
+end
+
 /-- `f` is surrounded by a set `s` if there is an affine basis `p` in `s` with weighted average `f`.
 -/
 def surrounded (f : F) (s : set F) : Prop :=
@@ -90,7 +107,7 @@ begin
     have h_tot : affine_span ℝ (range p) = ⊤ :=
       indep.affine_span_eq_top_iff_card_eq_finrank_add_one.mpr (fintype.card_fin _),
     refine ⟨range p, range_subset_iff.mpr h_mem, indep.range, h_tot, _⟩,
-    let basis : affine_basis (fin (finrank ℝ F + 1)) ℝ F := ⟨p, indep, h_tot⟩,
+    let basis : affine_basis ι ℝ F := ⟨p, indep, h_tot⟩,
     rw interior_convex_hull_aff_basis basis,
     intros i,
     rw [← finset.affine_combination_eq_linear_combination _ _ _ w_sum,
@@ -109,7 +126,7 @@ begin
     rw hp at h₀ h₂ h₃,
     replace h₁ : affine_independent ℝ p :=
       h₁.comp_embedding (fintype.equiv_fin_of_card_eq hb).symm.to_embedding,
-    let basis : affine_basis (fin (finrank ℝ F + 1)) ℝ F := ⟨_, h₁, h₂⟩,
+    let basis : affine_basis ι ℝ F := ⟨_, h₁, h₂⟩,
     rw [interior_convex_hull_aff_basis basis, mem_set_of_eq] at h₃,
     refine ⟨p, λ i, basis.coord i f, ⟨h₁, h₃, _, _⟩, λ i, h₀ (mem_range_self i)⟩,
     { exact basis.sum_coord_apply_eq_one f, },
@@ -144,19 +161,46 @@ begin
 end
 
 -- lem:smooth_barycentric_coord
-lemma smooth_surrounding {x : F} {p : fin (d + 1) → F} {w : fin (d + 1) → ℝ}
+lemma smooth_surrounding [finite_dimensional ℝ F] {x : F} {p : ι → F} {w : ι → ℝ}
   (h : surrounding_pts x p w) :
-  ∃ W : F → (fin (d+1) → F) → (fin (d+1) → ℝ),
-  ∀ᶠ (yq : F × (fin (d + 1) → F)) in 𝓝 (x, p), smooth_at (uncurry W) (yq.1, yq.2) ∧
+  ∃ W : F → (ι → F) → (ι → ℝ),
+  ∀ᶠ (yq : F × (ι → F)) in 𝓝 (x, p), smooth_at (uncurry W) yq ∧
                              (∀ i, 0 < W yq.1 yq.2 i) ∧
                              ∑ i, W yq.1 yq.2 i = 1 ∧
                              ∑ i, W yq.1 yq.2 i • yq.2 i = yq.1 :=
-sorry
+begin
+  classical,
+  use eval_barycentric_coords ι ℝ F,
+  let V : set (ι → ℝ) := set.pi set.univ (λ i, Ioi (0 : ℝ)),
+  let W' : F × (ι → F) → (ι → ℝ) := uncurry (eval_barycentric_coords ι ℝ F),
+  let A : set (F × (ι → F)) := set.prod univ (affine_bases ι ℝ F),
+  let U : set (F × (ι → F)) := A ∩ (W' ⁻¹' V),
+  have hι : fintype.card ι = d + 1 := fintype.card_fin _,
+  have hp : p ∈ affine_bases ι ℝ F := ⟨h.indep, h.tot⟩,
+  have hV : is_open V := is_open_set_pi finite_univ (λ _ _, is_open_Ioi),
+  have hW' : continuous_on W' A := (smooth_barycentric ι ℝ F hι).continuous_on,
+  have hxp : W' (x, p) ∈ V, { simp [W', hp, h.coord_eq_w, h.w_pos], },
+  have hA : is_open A,
+  { simp only [A, affine_bases_findim ι ℝ F hι],
+    exact is_open_univ.prod (is_open_set_of_affine_independent ℝ F), },
+  have hU₁ : U ⊆ A := set.inter_subset_left _ _,
+  have hU₂ : is_open U := hW'.preimage_open_of_open hA hV,
+  have hU₃ : U ∈ 𝓝 (x, p) :=
+    mem_nhds_iff.mpr ⟨U, le_refl U, hU₂, set.mem_inter (by simp [hp]) (mem_preimage.mpr hxp)⟩,
+  apply filter.eventually_of_mem hU₃,
+  rintros ⟨y, q⟩ hyq,
+  have hq : q ∈ affine_bases ι ℝ F, { simpa using hU₁ hyq, },
+  have hyq' : (y, q) ∈ W' ⁻¹' V := (set.inter_subset_right _ _) hyq,
+  refine ⟨⟨U, mem_nhds_iff.mpr ⟨U, le_refl U, hU₂, hyq⟩, (smooth_barycentric ι ℝ F hι).mono hU₁⟩, _, _, _⟩,
+  { simpa using hyq', },
+  { simp [hq], },
+  { simp [hq, affine_basis.linear_combination_coord_eq_self _ y], },
+end
 
-lemma smooth_surrounding_pts {x : F} {p : fin (d + 1) → F} {w : fin (d + 1) → ℝ}
+lemma smooth_surrounding_pts [finite_dimensional ℝ F] {x : F} {p : ι → F} {w : ι → ℝ}
   (h : surrounding_pts x p w) :
-  ∃ W : F → (fin (d+1) → F) → (fin (d+1) → ℝ),
-  ∀ᶠ (yq : F × (fin (d + 1) → F)) in 𝓝 (x, p), smooth_at (uncurry W) yq ∧
+  ∃ W : F → (ι → F) → (ι → ℝ),
+  ∀ᶠ (yq : F × (ι → F)) in 𝓝 (x, p), smooth_at (uncurry W) yq ∧
     surrounding_pts yq.1 yq.2 (W yq.1 yq.2) :=
 begin
   refine exists_imp_exists (λ W hW, _) (smooth_surrounding h),

src/loops/smooth_barycentric.lean

@@ -0,0 +1,149 @@
+import to_mathlib.analysis.normed_space.add_torsor_bases
+import to_mathlib.analysis.calculus.times_cont_diff
+
+noncomputable theory
+open set function
+open_locale affine matrix big_operators
+
+section barycentric_det
+
+variables (ι R k P : Type*) {M : Type*} [ring R] [add_comm_group M] [module R M] [affine_space M P]
+include M
+
+-- On reflection, it might be better to drop this definition and just write
+-- `affine_independent R v ∧ affine_span R (range v) = ⊤` everywhere instead of
+-- `v ∈ affine_bases ι R P`.
+def affine_bases : set (ι → P) :=
+{ v | affine_independent R v ∧ affine_span R (range v) = ⊤ }
+
+variables [fintype ι] [decidable_eq ι]
+
+lemma affine_bases_findim [field k] [module k M] [finite_dimensional k M]
+  (h : fintype.card ι = finite_dimensional.finrank k M + 1) :
+  affine_bases ι k P = { v | affine_independent k v } :=
+begin
+  ext v,
+  simp only [affine_bases, mem_set_of_eq, and_iff_left_iff_imp],
+  exact λ h_ind, h_ind.affine_span_eq_top_iff_card_eq_finrank_add_one.mpr h,
+end
+
+lemma mem_affine_bases_iff [nontrivial R] (b : affine_basis ι R P) (v : ι → P) :
+  v ∈ affine_bases ι R P ↔ is_unit (b.to_matrix v) :=
+(b.is_unit_to_matrix_iff v).symm
+
+def eval_barycentric_coords [∀ v, decidable (v ∈ affine_bases ι R P)] (p : P) (v : ι → P) : ι → R :=
+if h : v ∈ affine_bases ι R P then ((affine_basis.mk v h.1 h.2).coords p : ι → R) else 0
+
+@[simp] lemma eval_barycentric_coords_apply_of_mem_bases [∀ v, decidable (v ∈ affine_bases ι R P)]
+  (p : P) {v : ι → P} (h : v ∈ affine_bases ι R P) :
+  eval_barycentric_coords ι R P p v = (affine_basis.mk v h.1 h.2).coords p :=
+by simp only [eval_barycentric_coords, h, dif_pos]
+
+variables {ι R P}
+
+-- This could be stated and proved without having to assume a choice of affine basis if we
+-- had a sufficiently-developed theory of exterior algebras. Two key results which are missing
+-- are that the top exterior power is one-dimensional (and thus its non-zero elements are a
+-- multiplicative torsor for the scalar units) and that linear independence corresponds to
+-- exterior product being non-zero.
+lemma eval_barycentric_coords_eq_det
+  (S : Type*) [field S] [module S M] [∀ v, decidable (v ∈ affine_bases ι S P)]
+  (b : affine_basis ι S P) (p : P) (v : ι → P) :
+  eval_barycentric_coords ι S P p v = (b.to_matrix v).det⁻¹ • (b.to_matrix v)ᵀ.cramer (b.coords p) :=
+begin
+  ext i,
+  by_cases h : v ∈ affine_bases ι S P,
+  { simp only [eval_barycentric_coords, h, dif_pos, algebra.id.smul_eq_mul, pi.smul_apply,
+      affine_basis.coords_apply, ← b.det_smul_coords_eq_cramer_coords ⟨v, h.1, h.2⟩, smul_smul],
+    convert (one_mul _).symm,
+    have hu := b.is_unit_to_matrix ⟨v, h.1, h.2⟩,
+    rw matrix.is_unit_iff_is_unit_det at hu,
+    rw ← ring.inverse_eq_inv,
+    exact ring.inverse_mul_cancel _ hu, },
+  { -- Both sides are "junk values". It's only slightly evil to take advantage of this.
+    simp only [eval_barycentric_coords, h, algebra.id.smul_eq_mul, pi.zero_apply, inv_eq_zero,
+      dif_neg, not_false_iff, zero_eq_mul, pi.smul_apply],
+    left,
+    rwa [mem_affine_bases_iff ι S P b v, matrix.is_unit_iff_is_unit_det,
+      is_unit_iff_ne_zero, not_not] at h, },
+end
+
+end barycentric_det
+
+namespace matrix
+
+-- This lemma already exists in Mathlib but we need a bump to pick it up.
+@[simp] lemma coe_det_is_empty {n R : Type*} [comm_ring R] [is_empty n] [decidable_eq n] :
+  (det : matrix n n R → R) = function.const _ 1 :=
+by { ext, exact det_is_empty, }
+
+variables (ι k : Type*) [fintype ι] [decidable_eq ι] [nondiscrete_normed_field k]
+
+attribute [instance] normed_group normed_space
+
+-- This should really be deduced from general results about continuous multilinear maps.
+lemma smooth_det (m : with_top ℕ) :
+  times_cont_diff k m (det : matrix ι ι k → k) :=
+begin
+  suffices : ∀ (n : ℕ), times_cont_diff k m (det : matrix (fin n) (fin n) k → k),
+  { have h : (det : matrix ι ι k → k) = det ∘ reindex (fintype.equiv_fin ι) (fintype.equiv_fin ι),
+    { ext, simp, },
+    rw h,
+    apply (this (fintype.card ι)).comp,
+    exact times_cont_diff_pi.mpr (λ i, times_cont_diff_pi.mpr (λ j, times_cont_diff_apply_apply _ _)), },
+  intros n,
+  induction n with n ih,
+  { rw coe_det_is_empty,
+    exact times_cont_diff_const, },
+  change times_cont_diff k m (λ (A : matrix (fin n.succ) (fin n.succ) k), A.det),
+  simp_rw det_succ_column_zero,
+  apply times_cont_diff.sum (λ l _, _),
+  apply times_cont_diff.mul,
+  { refine times_cont_diff_const.mul _,
+    apply times_cont_diff_apply_apply, },
+  { apply ih.comp,
+    refine times_cont_diff_pi.mpr (λ i, times_cont_diff_pi.mpr (λ j, _)),
+    simp only [minor_apply],
+    apply times_cont_diff_apply_apply, },
+end
+
+end matrix
+
+section smooth_barycentric
+
+variables (ι 𝕜 F : Type*)
+variables [fintype ι] [decidable_eq ι] [nondiscrete_normed_field 𝕜] [complete_space 𝕜]
+variables [normed_group F] [normed_space 𝕜 F]
+
+-- An alternative approach would be to prove the affine version of `times_cont_diff_at_map_inverse`
+-- and prove that barycentric coordinates give a continuous affine equivalence to
+-- `{ f : ι →₀ 𝕜 | f.sum = 1 }`. This should obviate the need for the finite-dimensionality assumption.
+lemma smooth_barycentric [∀ v, decidable (v ∈ affine_bases ι 𝕜 F)] [finite_dimensional 𝕜 F]
+  (h : fintype.card ι = finite_dimensional.finrank 𝕜 F + 1) :
+  times_cont_diff_on 𝕜 ⊤ (uncurry (eval_barycentric_coords ι 𝕜 F)) (set.prod univ (affine_bases ι 𝕜 F)) :=
+begin
+  obtain ⟨b : affine_basis ι 𝕜 F⟩ := affine_basis.exists_affine_basis_of_finite_dimensional h,
+  simp_rw [uncurry_def, times_cont_diff_on_pi, eval_barycentric_coords_eq_det 𝕜 b],
+  intros i,
+  simp only [algebra.id.smul_eq_mul, pi.smul_apply, matrix.cramer_transpose_apply],
+  have h_snd : times_cont_diff 𝕜 ⊤ (λ (x : F × (ι → F)), b.to_matrix x.snd),
+  { refine times_cont_diff.comp _ times_cont_diff_snd,
+    refine times_cont_diff_pi.mpr (λ j, times_cont_diff_pi.mpr (λ j', _)),
+    exact (smooth_barycentric_coord b j').comp (times_cont_diff_apply j), },
+  apply times_cont_diff_on.mul,
+  { apply ((matrix.smooth_det ι 𝕜 ⊤).comp h_snd).times_cont_diff_on.inv,
+    rintros ⟨p, v⟩ hpv,
+    have hv : is_unit (b.to_matrix v), { simpa [mem_affine_bases_iff ι 𝕜 F b v] using hpv, },
+    rw [← is_unit_iff_ne_zero, ← matrix.is_unit_iff_is_unit_det],
+    exact hv, },
+  { refine ((matrix.smooth_det ι 𝕜 ⊤).comp _).times_cont_diff_on,
+    refine times_cont_diff_pi.mpr (λ j, times_cont_diff_pi.mpr (λ j', _)),
+    simp only [matrix.update_row_apply, affine_basis.to_matrix_apply, affine_basis.coords_apply],
+    by_cases hij : j = i,
+    { simp only [hij, if_true, eq_self_iff_true],
+      exact (smooth_barycentric_coord b j').comp times_cont_diff_fst, },
+    { simp only [hij, if_false],
+      exact (smooth_barycentric_coord b j').comp (times_cont_diff_pi.mp times_cont_diff_snd j), }, },
+end
+
+end smooth_barycentric

src/to_mathlib/analysis/calculus/times_cont_diff.lean

@@ -0,0 +1,13 @@
+import analysis.calculus.times_cont_diff
+
+variables {ι k : Type*} [fintype ι]
+variables [nondiscrete_normed_field k] {Z : Type*} [normed_group Z] [normed_space k Z]
+variables {m : with_top ℕ}
+
+lemma times_cont_diff_apply (i : ι) :
+  times_cont_diff k m (λ (f : ι → Z), f i) :=
+(continuous_linear_map.proj i : (ι → Z) →L[k] Z).times_cont_diff
+
+lemma times_cont_diff_apply_apply (i j : ι) :
+  times_cont_diff k m (λ (f : ι → ι → Z), f j i) :=
+(@times_cont_diff_apply _ _ _ _ Z _ _ m i).comp (@times_cont_diff_apply _ _ _ _ (ι → Z) _ _ m j)

src/to_mathlib/analysis/normed_space/add_torsor_bases.lean

@@ -0,0 +1,9 @@
+import analysis.calculus.affine_map
+import analysis.normed_space.add_torsor_bases
+
+variables {ι 𝕜 E : Type*} [nondiscrete_normed_field 𝕜] [complete_space 𝕜]
+variables [normed_group E] [normed_space 𝕜 E] [finite_dimensional 𝕜 E]
+variables (b : affine_basis ι 𝕜 E)
+
+lemma smooth_barycentric_coord (i : ι) : times_cont_diff 𝕜 ⊤ (b.coord i) :=
+(⟨b.coord i, continuous_barycentric_coord b i⟩ : E →A[𝕜] 𝕜).times_cont_diff