Cylinders and graphs of analytic submanifolds

In cylinder coordinates Fin.cons t x, adjoining a free scalar coordinate increases the dimension of an analytic submanifold by one. The graph of a scalar function analytic on the submanifold has the same dimension as its base. These constructions provide analytic charts for sections and open sectors between analytic root functions.

The graph construction only requires analyticity on the submanifold: it uses a local extension in a base chart, rather than requiring the given ambient function to be analytic.

References

• S. G. Krantz and H. R. Parks, A Primer of Real Analytic Functions, second edition, Birkhäuser, 2002, Chapter 2.

theorem TauCeti.IsAnalyticSubmanifold.cylinder {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n d : ℕ} {S : Set (Fin n → 𝕜)} (hS : IsAnalyticSubmanifold d S) : IsAnalyticSubmanifold (d + 1) {v : Fin (n + 1) → 𝕜 | Fin.tail v ∈ S}

Adjoining a free scalar coordinate to an analytic submanifold increases its dimension by one. The new coordinate is coordinate zero, as in Fin.cons.

theorem TauCeti.IsAnalyticSubmanifold.graph {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n d : ℕ} {S : Set (Fin n → 𝕜)} (hS : IsAnalyticSubmanifold d S) {f : (Fin n → 𝕜) → 𝕜} (hf : AnalyticOnSubmanifold d f S) : IsAnalyticSubmanifold d {v : Fin (n + 1) → 𝕜 | Fin.tail v ∈ S ∧ v 0 = f (Fin.tail v)}

The graph of a scalar function analytic on a submanifold is an analytic submanifold of the same dimension. Only the values of the function on the base matter.

theorem TauCeti.IsAnalyticSubmanifold.below {n d : ℕ} {S : Set (Fin n → ℝ)} (hS : IsAnalyticSubmanifold d S) {f : (Fin n → ℝ) → ℝ} (hf : ContinuousOn f S) : IsAnalyticSubmanifold (d + 1) {v : Fin (n + 1) → ℝ | Fin.tail v ∈ S ∧ v 0 < f (Fin.tail v)}

The nonempty sector below a continuous real function is an analytic submanifold of dimension one more than its base.

theorem TauCeti.IsAnalyticSubmanifold.above {n d : ℕ} {S : Set (Fin n → ℝ)} (hS : IsAnalyticSubmanifold d S) {f : (Fin n → ℝ) → ℝ} (hf : ContinuousOn f S) : IsAnalyticSubmanifold (d + 1) {v : Fin (n + 1) → ℝ | Fin.tail v ∈ S ∧ f (Fin.tail v) < v 0}

The nonempty sector above a continuous real function is an analytic submanifold of dimension one more than its base.

theorem TauCeti.IsAnalyticSubmanifold.between {n d : ℕ} {S : Set (Fin n → ℝ)} (hS : IsAnalyticSubmanifold d S) {f g : (Fin n → ℝ) → ℝ} (hf : ContinuousOn f S) (hg : ContinuousOn g S) (hne : {v : Fin (n + 1) → ℝ | Fin.tail v ∈ S ∧ f (Fin.tail v) < v 0 ∧ v 0 < g (Fin.tail v)}.Nonempty) : IsAnalyticSubmanifold (d + 1) {v : Fin (n + 1) → ℝ | Fin.tail v ∈ S ∧ f (Fin.tail v) < v 0 ∧ v 0 < g (Fin.tail v)}

The nonempty open sector between two continuous real functions is an analytic submanifold of dimension one more than its base.