Smoothness of coordinate insertion and of homogeneous ratios

Inserting a coordinate into a tuple, x ↦ Fin.insertNth i (f x) (g x), is as smooth as its inputs; this is the differentiable counterpart of Mathlib's Continuous.finInsertNth.

As a consequence, the homogeneous-ratio maps z ↦ (Fin.insertNth i 1 z (j.succAbove k) / Fin.insertNth i 1 z j)_k are smooth, indeed analytic, wherever the denominator is nonzero. These are the transition maps between the standard affine charts of projective space over a nontrivially normed field, so this file supplies the smoothness of every atlas of projective space built from homogeneous ratios.

theorem ContDiff.finInsertNth {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {r : WithTop ℕ∞} {F : Fin (n + 1) → Type u_3} [(j : Fin (n + 1)) → NormedAddCommGroup (F j)] [(j : Fin (n + 1)) → NormedSpace 𝕜 (F j)] (i : Fin (n + 1)) {f : E → F i} {g : E → (j : Fin n) → F (i.succAbove j)} (hf : ContDiff 𝕜 r f) (hg : ContDiff 𝕜 r g) : ContDiff 𝕜 r fun (x : E) => i.insertNth (f x) (g x)

Inserting a coordinate into a tuple preserves smoothness: if f and g are C^r, then so is x ↦ Fin.insertNth i (f x) (g x).

theorem Fin.contDiffOn_insertNth_one_div {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n : ℕ} {r : WithTop ℕ∞} (i j : Fin (n + 1)) : ContDiffOn 𝕜 r (fun (z : Fin n → 𝕜) (k : Fin n) => i.insertNth 1 z (j.succAbove k) / i.insertNth 1 z j) {z : Fin n → 𝕜 | i.insertNth 1 z j ≠ 0}

The homogeneous-ratio map z ↦ (w (j.succAbove k) / w j)_k, where w = Fin.insertNth i 1 z inserts the coordinate 1 in position i, is C^r on the set where w j ≠ 0. These maps are the transition maps between the standard affine charts of projective space.