Analytic submanifolds of 𝕜ⁿ and analytic functions on them

A subset S of 𝕜ⁿ is a d-dimensional analytic submanifold if it can be straightened near each of its points by an analytic change of coordinates of the ambient space: around every x ∈ S there is an open partial homeomorphism e of 𝕜ⁿ, analytic with analytic inverse, which maps e.source ∩ S onto the points of e.target whose coordinates of index at least d vanish. Such an e is an analytic chart of S (TauCeti.IsAnalyticChart).

A function f on 𝕜ⁿ is analytic on the d-dimensional submanifold S if near each point of S its coordinate expression u ↦ f (e.symm (u, 0)) in an analytic chart, a function of the first d coordinates u ∈ 𝕜ᵈ, is analytic (TauCeti.AnalyticOnSubmanifold). Only the values of f on S matter. Analyticity does not depend on the chart: once the coordinate expression is analytic in one chart, it is analytic in every chart around the point, since the transition between two charts is analytic. This is what makes the notion usable: analytic functions on S are closed under composition with analytic maps of the values, under pairing, and under composition with analytic maps from S into another analytic submanifold. Submanifolds restrict to nonempty relatively open subsets, analytic functions restrict to arbitrary relatively open subsets, and analyticity of functions is a local property.

Over ℝ, analytic submanifolds are the cells over which McCallum's and Lazard's projection theorems lift cylindrical decompositions: the lifting theorems assert that, over such a cell, the ordered real roots of suitable polynomials are analytic functions on the cell.

Implementation notes

The coordinate maps TauCeti.firstCoords 𝕜 d n : 𝕜ᵈ → 𝕜ⁿ and TauCeti.firstCoords 𝕜 n d are defined without the hypothesis d ≤ n, so that charts and analytic functions make sense for every d; the hypothesis d ≤ n is part of TauCeti.IsAnalyticSubmanifold.

Main declarations

• TauCeti.firstCoords 𝕜 m k: the linear map 𝕜ᵐ → 𝕜ᵏ copying the first min m k coordinates. It includes 𝕜ᵈ in 𝕜ⁿ as the first d coordinates and projects back.
• TauCeti.IsAnalyticChart d S e: e is an analytic chart of S in dimension d.
• TauCeti.IsAnalyticSubmanifold d S: S is a d-dimensional analytic submanifold.
• TauCeti.AnalyticOnSubmanifold d f S: f is analytic on S in dimension d.
• TauCeti.AnalyticOnSubmanifold.analyticAt_chart: independence of the chart.
• TauCeti.AnalyticOnSubmanifold.analyticOnNhd: the coordinate expression in any chart is analytic on the open set of 𝕜ᵈ where it is defined.
• AnalyticOnNhd.analyticOnSubmanifold, AnalyticOnNhd.comp_analyticOnSubmanifold, TauCeti.AnalyticOnSubmanifold.prod, TauCeti.AnalyticOnSubmanifold.comp: ambient analytic functions, compositions and pairs.
• TauCeti.IsAnalyticSubmanifold.inter, TauCeti.AnalyticOnSubmanifold.inter, TauCeti.analyticOnSubmanifold_of_locally_analyticOnSubmanifold: restriction to relatively open subsets (nonempty ones, for submanifolds), and locality.
• TauCeti.AnalyticOnSubmanifold.exists_analyticAt_eqOn, TauCeti.AnalyticOnSubmanifold.exists_analyticOnNhd_eqOn: local ambient analytic extensions.
• TauCeti.AnalyticOnSubmanifold.continuousOn: intrinsic analytic functions are continuous.
• TauCeti.IsAnalyticSubmanifold.of_isOpen_preimage_val: nonempty relatively open subsets.
• TauCeti.isAnalyticSubmanifold_coordSubspace, IsOpen.isAnalyticSubmanifold, TauCeti.isAnalyticSubmanifold_singleton: coordinate subspaces, open sets and points.

References

• S. G. Krantz and H. R. Parks, A Primer of Real Analytic Functions, second edition, Birkhäuser, 2002, Chapter 2 (real analytic submanifolds).
• S. McCallum, An improved projection operation for cylindrical algebraic decomposition, 1998 (analytic delineability over analytic submanifolds).

Leading coordinates

def TauCeti.firstCoords (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] (m k : ℕ) : (Fin m → 𝕜) →L[𝕜] Fin k → 𝕜

TauCeti.firstCoords 𝕜 m k v is the vector of 𝕜ᵏ whose coordinate of index i is that of v ∈ 𝕜ᵐ when i < m, and zero otherwise. For d ≤ n, firstCoords 𝕜 d n includes 𝕜ᵈ in 𝕜ⁿ as the subspace of the first d coordinates, and firstCoords 𝕜 n d is the projection onto these coordinates.

Equations

• TauCeti.firstCoords 𝕜 m k = ContinuousLinearMap.pi fun (i : Fin k) => if h : ↑i < m then ContinuousLinearMap.proj ⟨↑i, h⟩ else 0

@[simp]

theorem TauCeti.firstCoords_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {m n : ℕ} (v : Fin m → 𝕜) (i : Fin n) : (firstCoords 𝕜 m n) v i = if h : ↑i < m then v ⟨↑i, h⟩ else 0

theorem TauCeti.firstCoords_apply_of_le {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {m n : ℕ} (v : Fin m → 𝕜) {i : Fin n} (hi : m ≤ ↑i) : (firstCoords 𝕜 m n) v i = 0

The coordinates of index at least m of firstCoords 𝕜 m n v vanish.

@[simp]

theorem TauCeti.firstCoords_firstCoords_of_le {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n d : ℕ} (h : d ≤ n) (u : Fin d → 𝕜) : (firstCoords 𝕜 n d) ((firstCoords 𝕜 d n) u) = u

Projecting 𝕜ᵈ ⊆ 𝕜ⁿ back to its first d coordinates is the identity.

theorem TauCeti.firstCoords_firstCoords_of_forall {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n d : ℕ} {y : Fin n → 𝕜} (hy : ∀ (i : Fin n), d ≤ ↑i → y i = 0) : (firstCoords 𝕜 d n) ((firstCoords 𝕜 n d) y) = y

A vector of 𝕜ⁿ whose coordinates of index at least d vanish is recovered from its first d coordinates.

Analytic charts

structure TauCeti.IsAnalyticChart {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n : ℕ} (d : ℕ) (S : Set (Fin n → 𝕜)) (e : OpenPartialHomeomorph (Fin n → 𝕜) (Fin n → 𝕜)) : Prop

An analytic chart of S ⊆ 𝕜ⁿ in dimension d is an open partial homeomorphism e of 𝕜ⁿ, analytic on its source with inverse analytic on its target, which straightens S: it maps e.source ∩ S onto the points of e.target whose coordinates of index at least d vanish.

• analyticOnNhd : AnalyticOnNhd 𝕜 (↑e) e.source

  The chart is analytic on its source.

• analyticOnNhd_symm : AnalyticOnNhd 𝕜 (↑e.symm) e.target

  The inverse of the chart is analytic on its target.

• isImage : e.IsImage S {y : Fin n → 𝕜 | ∀ (i : Fin n), d ≤ ↑i → y i = 0}

  The chart maps the part of S in its source onto the points of its target whose coordinates of index at least d vanish.

theorem TauCeti.IsAnalyticChart.mem_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n d : ℕ} {S : Set (Fin n → 𝕜)} {e : OpenPartialHomeomorph (Fin n → 𝕜) (Fin n → 𝕜)} {x : Fin n → 𝕜} (he : IsAnalyticChart d S e) (hx : x ∈ e.source) : x ∈ S ↔ ∀ (i : Fin n), d ≤ ↑i → ↑e x i = 0

A point of the source of an analytic chart lies in S exactly when the coordinates of index at least d of its image vanish.

theorem TauCeti.IsAnalyticChart.congr_set {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n d : ℕ} {S T : Set (Fin n → 𝕜)} {e : OpenPartialHomeomorph (Fin n → 𝕜) (Fin n → 𝕜)} (he : IsAnalyticChart d S e) (h : e.source ∩ S = e.source ∩ T) : IsAnalyticChart d T e

An analytic chart of S is an analytic chart of every set with the same points in its source.

theorem TauCeti.IsAnalyticChart.restrOpen {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n d : ℕ} {S U : Set (Fin n → 𝕜)} {e : OpenPartialHomeomorph (Fin n → 𝕜) (Fin n → 𝕜)} (he : IsAnalyticChart d S e) (hU : IsOpen U) : IsAnalyticChart d S (e.restrOpen U hU)

The restriction of an analytic chart of S to an open set is an analytic chart of S.

theorem TauCeti.IsAnalyticChart.restrOpen_inter {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n d : ℕ} {S U : Set (Fin n → 𝕜)} {e : OpenPartialHomeomorph (Fin n → 𝕜) (Fin n → 𝕜)} (he : IsAnalyticChart d S e) (hU : IsOpen U) : IsAnalyticChart d (S ∩ U) (e.restrOpen U hU)

The restriction of an analytic chart of S to an open set U is an analytic chart of S ∩ U.

theorem TauCeti.IsAnalyticChart.of_inter {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n d : ℕ} {S U : Set (Fin n → 𝕜)} {e : OpenPartialHomeomorph (Fin n → 𝕜) (Fin n → 𝕜)} (he : IsAnalyticChart d (S ∩ U) e) (hU : e.source ⊆ U) : IsAnalyticChart d S e

An analytic chart of S ∩ U whose source lies in U is an analytic chart of S.

theorem TauCeti.IsAnalyticChart.firstCoords_firstCoords_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n d : ℕ} {S : Set (Fin n → 𝕜)} {e : OpenPartialHomeomorph (Fin n → 𝕜) (Fin n → 𝕜)} {x : Fin n → 𝕜} (he : IsAnalyticChart d S e) (hx : x ∈ e.source) (hxS : x ∈ S) : (firstCoords 𝕜 d n) ((firstCoords 𝕜 n d) (↑e x)) = ↑e x

The image of a point of S by an analytic chart is determined by its first d coordinates.

theorem TauCeti.IsAnalyticChart.symm_firstCoords_firstCoords_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n d : ℕ} {S : Set (Fin n → 𝕜)} {e : OpenPartialHomeomorph (Fin n → 𝕜) (Fin n → 𝕜)} {x : Fin n → 𝕜} (he : IsAnalyticChart d S e) (hx : x ∈ e.source) (hxS : x ∈ S) : ↑e.symm ((firstCoords 𝕜 d n) ((firstCoords 𝕜 n d) (↑e x))) = x

A point of S is recovered from the first d coordinates of its image by an analytic chart.

theorem TauCeti.IsAnalyticChart.analyticAt_symm_firstCoords {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n d : ℕ} {S : Set (Fin n → 𝕜)} {e : OpenPartialHomeomorph (Fin n → 𝕜) (Fin n → 𝕜)} {x : Fin n → 𝕜} (he : IsAnalyticChart d S e) (hx : x ∈ e.source) (hxS : x ∈ S) : AnalyticAt 𝕜 (fun (u : Fin d → 𝕜) => ↑e.symm ((firstCoords 𝕜 d n) u)) ((firstCoords 𝕜 n d) (↑e x))

The local parametrization u ↦ e.symm (u, 0) of S by an analytic chart is analytic at the coordinates of each point of S in the source.

theorem TauCeti.IsAnalyticChart.eventually_symm_firstCoords_mem {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n d : ℕ} {S : Set (Fin n → 𝕜)} {e : OpenPartialHomeomorph (Fin n → 𝕜) (Fin n → 𝕜)} {x : Fin n → 𝕜} (he : IsAnalyticChart d S e) (hx : x ∈ e.source) (hxS : x ∈ S) : ∀ᶠ (u : Fin d → 𝕜) in nhds ((firstCoords 𝕜 n d) (↑e x)), ↑e.symm ((firstCoords 𝕜 d n) u) ∈ e.source ∩ S

Near the coordinates of a point of S, the local parametrization u ↦ e.symm (u, 0) by an analytic chart takes values in the part of S in the source of the chart.

theorem TauCeti.IsAnalyticChart.analyticAt_comp {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {m d' : ℕ} {T : Set (Fin m → 𝕜)} {e' : OpenPartialHomeomorph (Fin m → 𝕜) (Fin m → 𝕜)} {g : (Fin m → 𝕜) → E} {φ : F → Fin m → 𝕜} {u₀ : F} (he' : IsAnalyticChart d' T e') (hφ : AnalyticAt 𝕜 φ u₀) (h₀ : φ u₀ ∈ e'.source) (hT : ∀ᶠ (u : F) in nhds u₀, φ u ∈ T) (hg : AnalyticAt 𝕜 (fun (v : Fin d' → 𝕜) => g (↑e'.symm ((firstCoords 𝕜 d' m) v))) ((firstCoords 𝕜 m d') (↑e' (φ u₀)))) : AnalyticAt 𝕜 (g ∘ φ) u₀

Let e' be an analytic chart of T in dimension d'. If φ is analytic at u₀, takes values in T near u₀, and φ u₀ lies in the source of e', and if the coordinate expression of g in e' is analytic at the coordinates of φ u₀, then g ∘ φ is analytic at u₀.

Analytic submanifolds

structure TauCeti.IsAnalyticSubmanifold {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n : ℕ} (d : ℕ) (S : Set (Fin n → 𝕜)) : Prop

A set S ⊆ 𝕜ⁿ is a d-dimensional analytic submanifold if it is nonempty, d ≤ n, and every point of S lies in the source of an analytic chart of S in dimension d.

• nonempty : S.Nonempty

  An analytic submanifold is nonempty.

• le : d ≤ n

  The dimension of an analytic submanifold is at most that of the ambient space.

• exists_isAnalyticChart (x : Fin n → 𝕜) : x ∈ S → ∃ (e : OpenPartialHomeomorph (Fin n → 𝕜) (Fin n → 𝕜)), x ∈ e.source ∧ IsAnalyticChart d S e

  Every point of an analytic submanifold lies in the source of an analytic chart.

theorem TauCeti.isAnalyticSubmanifold_coordSubspace {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n d : ℕ} (h : d ≤ n) : IsAnalyticSubmanifold d {y : Fin n → 𝕜 | ∀ (i : Fin n), d ≤ ↑i → y i = 0}

The subspace of the first d coordinates of 𝕜ⁿ is a d-dimensional analytic submanifold.

theorem IsOpen.isAnalyticSubmanifold {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n : ℕ} {U : Set (Fin n → 𝕜)} (hU : IsOpen U) (hne : U.Nonempty) : TauCeti.IsAnalyticSubmanifold n U

A nonempty open subset of 𝕜ⁿ is an n-dimensional analytic submanifold.

theorem TauCeti.isAnalyticSubmanifold_singleton {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n : ℕ} (a : Fin n → 𝕜) : IsAnalyticSubmanifold 0 {a}

A point of 𝕜ⁿ is a 0-dimensional analytic submanifold.

theorem TauCeti.IsAnalyticSubmanifold.inter {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n d : ℕ} {S U : Set (Fin n → 𝕜)} (hS : IsAnalyticSubmanifold d S) (hU : IsOpen U) (hne : (S ∩ U).Nonempty) : IsAnalyticSubmanifold d (S ∩ U)

The intersection of an analytic submanifold with an open set meeting it is an analytic submanifold of the same dimension.

theorem TauCeti.IsAnalyticSubmanifold.of_isOpen_preimage_val {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n d : ℕ} {S T : Set (Fin n → 𝕜)} (hS : IsAnalyticSubmanifold d S) (hTS : T ⊆ S) (hT : IsOpen (Subtype.val ⁻¹' T)) (hne : T.Nonempty) : IsAnalyticSubmanifold d T

A nonempty relatively open subset of an analytic submanifold is an analytic submanifold of the same dimension. Relative openness is expressed using the subtype topology.

Analytic functions on analytic submanifolds

def TauCeti.AnalyticOnSubmanifold {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (d : ℕ) (f : (Fin n → 𝕜) → E) (S : Set (Fin n → 𝕜)) : Prop

A function f on 𝕜ⁿ is analytic on S in dimension d if every point x ∈ S lies in the source of an analytic chart e of S in which the coordinate expression u ↦ f (e.symm (u, 0)), a function of u ∈ 𝕜ᵈ, is analytic at the first d coordinates of e x. By TauCeti.AnalyticOnSubmanifold.analyticAt_chart, the coordinate expression is then analytic in every analytic chart around x.

Equations

• One or more equations did not get rendered due to their size.

theorem TauCeti.analyticOnSubmanifold_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n d : ℕ} {S : Set (Fin n → 𝕜)} {f : (Fin n → 𝕜) → E} : AnalyticOnSubmanifold d f S ↔ ∀ x ∈ S, ∃ (e : OpenPartialHomeomorph (Fin n → 𝕜) (Fin n → 𝕜)), x ∈ e.source ∧ IsAnalyticChart d S e ∧ AnalyticAt 𝕜 (fun (u : Fin d → 𝕜) => f (↑e.symm ((firstCoords 𝕜 d n) u))) ((firstCoords 𝕜 n d) (↑e x))

A function is analytic on S exactly when it has an analytic coordinate expression in some analytic chart around every point of S.

theorem TauCeti.AnalyticOnSubmanifold.analyticAt_chart {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n d : ℕ} {S : Set (Fin n → 𝕜)} {e : OpenPartialHomeomorph (Fin n → 𝕜) (Fin n → 𝕜)} {x : Fin n → 𝕜} {f : (Fin n → 𝕜) → E} (hf : AnalyticOnSubmanifold d f S) (hx : x ∈ S) (he : IsAnalyticChart d S e) (hxe : x ∈ e.source) : AnalyticAt 𝕜 (fun (u : Fin d → 𝕜) => f (↑e.symm ((firstCoords 𝕜 d n) u))) ((firstCoords 𝕜 n d) (↑e x))

Independence of the chart. If f is analytic on S, its coordinate expression in every analytic chart of S is analytic at the coordinates of every point of S in the source.

theorem TauCeti.AnalyticOnSubmanifold.analyticOnNhd {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n d : ℕ} {S : Set (Fin n → 𝕜)} {e : OpenPartialHomeomorph (Fin n → 𝕜) (Fin n → 𝕜)} {f : (Fin n → 𝕜) → E} (hf : AnalyticOnSubmanifold d f S) (he : IsAnalyticChart d S e) (hd : d ≤ n) : AnalyticOnNhd 𝕜 (fun (u : Fin d → 𝕜) => f (↑e.symm ((firstCoords 𝕜 d n) u))) (⇑(firstCoords 𝕜 d n) ⁻¹' e.target)

Analyticity in coordinates. If f is analytic on a set S in dimension d ≤ n, its coordinate expression u ↦ f (e.symm (u, 0)) in any analytic chart e of S is analytic on the open subset of 𝕜ᵈ where it is defined.

theorem TauCeti.AnalyticOnSubmanifold.congr {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n d : ℕ} {S : Set (Fin n → 𝕜)} {f g : (Fin n → 𝕜) → E} (hf : AnalyticOnSubmanifold d f S) (hfg : Set.EqOn f g S) : AnalyticOnSubmanifold d g S

Analyticity on S only depends on the values on S.

theorem TauCeti.AnalyticOnSubmanifold.exists_analyticAt_eqOn {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n d : ℕ} {S : Set (Fin n → 𝕜)} {x : Fin n → 𝕜} {f : (Fin n → 𝕜) → E} (hf : AnalyticOnSubmanifold d f S) (hx : x ∈ S) : ∃ (U : Set (Fin n → 𝕜)), IsOpen U ∧ x ∈ U ∧ ∃ (g : (Fin n → 𝕜) → E), AnalyticAt 𝕜 g x ∧ Set.EqOn f g (S ∩ U)

A function analytic on a submanifold has an ambient extension analytic at each point. The extension agrees with the function on the submanifold in an open neighborhood.

theorem TauCeti.AnalyticOnSubmanifold.exists_analyticOnNhd_eqOn {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n d : ℕ} {S : Set (Fin n → 𝕜)} {x : Fin n → 𝕜} {f : (Fin n → 𝕜) → E} (hf : AnalyticOnSubmanifold d f S) (hd : d ≤ n) (hx : x ∈ S) : ∃ (U : Set (Fin n → 𝕜)), IsOpen U ∧ x ∈ U ∧ ∃ (g : (Fin n → 𝕜) → E), AnalyticOnNhd 𝕜 g U ∧ Set.EqOn f g (S ∩ U)

A function analytic on a submanifold of dimension d ≤ n has an ambient analytic extension on an open neighborhood of each point.

theorem TauCeti.AnalyticOnSubmanifold.continuousOn {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n d : ℕ} {S : Set (Fin n → 𝕜)} {f : (Fin n → 𝕜) → E} (hf : AnalyticOnSubmanifold d f S) : ContinuousOn f S

A function analytic on a submanifold is continuous on it.

theorem TauCeti.AnalyticOnSubmanifold.inter {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n d : ℕ} {S U : Set (Fin n → 𝕜)} {f : (Fin n → 𝕜) → E} (hf : AnalyticOnSubmanifold d f S) (hU : IsOpen U) : AnalyticOnSubmanifold d f (S ∩ U)

The restriction of an analytic function on S to the intersection of S with an open set is analytic.

theorem TauCeti.AnalyticOnSubmanifold.prod {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n d : ℕ} {S : Set (Fin n → 𝕜)} {f : (Fin n → 𝕜) → E} {g : (Fin n → 𝕜) → F} (hf : AnalyticOnSubmanifold d f S) (hg : AnalyticOnSubmanifold d g S) : AnalyticOnSubmanifold d (fun (x : Fin n → 𝕜) => (f x, g x)) S

A pair of analytic functions on S is analytic on S.

theorem TauCeti.AnalyticOnSubmanifold.comp {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {m n d d' : ℕ} {S : Set (Fin n → 𝕜)} {T : Set (Fin m → 𝕜)} {g : (Fin m → 𝕜) → E} {f : (Fin n → 𝕜) → Fin m → 𝕜} (hg : AnalyticOnSubmanifold d' g T) (hf : AnalyticOnSubmanifold d f S) (h : Set.MapsTo f S T) : AnalyticOnSubmanifold d (g ∘ f) S

Composition. If f is analytic on S and maps S into a set T, and g is analytic on T in dimension d', then g ∘ f is analytic on S. No hypothesis on T is needed: g being analytic on T already provides analytic charts of T around the values of f.

theorem TauCeti.IsAnalyticSubmanifold.analyticOnSubmanifold_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n d : ℕ} {S : Set (Fin n → 𝕜)} {f : (Fin n → 𝕜) → E} (hS : IsAnalyticSubmanifold d S) : AnalyticOnSubmanifold d f S ↔ ∀ x ∈ S, ∀ (e : OpenPartialHomeomorph (Fin n → 𝕜) (Fin n → 𝕜)), IsAnalyticChart d S e → x ∈ e.source → AnalyticAt 𝕜 (fun (u : Fin d → 𝕜) => f (↑e.symm ((firstCoords 𝕜 d n) u))) ((firstCoords 𝕜 n d) (↑e x))

On a set with analytic charts around each point, a function is analytic in dimension d exactly when its coordinate expression in every analytic chart is analytic at the coordinates of every point of the set in the source.

theorem TauCeti.analyticOnSubmanifold_congr {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n d : ℕ} {S : Set (Fin n → 𝕜)} {f g : (Fin n → 𝕜) → E} (hfg : Set.EqOn f g S) : AnalyticOnSubmanifold d f S ↔ AnalyticOnSubmanifold d g S

Analyticity on S only depends on the values on S.

theorem TauCeti.analyticOnSubmanifold_of_locally_analyticOnSubmanifold {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n d : ℕ} {S : Set (Fin n → 𝕜)} {f : (Fin n → 𝕜) → E} (h : ∀ x ∈ S, ∃ (U : Set (Fin n → 𝕜)), IsOpen U ∧ x ∈ U ∧ AnalyticOnSubmanifold d f (S ∩ U)) : AnalyticOnSubmanifold d f S

Locality. A function analytic on a neighbourhood in S of each point of S is analytic on S.

theorem AnalyticOnNhd.analyticOnSubmanifold {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n d : ℕ} {S : Set (Fin n → 𝕜)} {f : (Fin n → 𝕜) → E} (hf : AnalyticOnNhd 𝕜 f S) (hS : TauCeti.IsAnalyticSubmanifold d S) : TauCeti.AnalyticOnSubmanifold d f S

A function analytic at each point of an analytic submanifold S of 𝕜ⁿ, as a function on 𝕜ⁿ, is analytic on S.

theorem AnalyticOnNhd.comp_analyticOnSubmanifold {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n d : ℕ} {S : Set (Fin n → 𝕜)} {f : (Fin n → 𝕜) → E} {g : E → F} {t : Set E} (hg : AnalyticOnNhd 𝕜 g t) (hf : TauCeti.AnalyticOnSubmanifold d f S) (h : Set.MapsTo f S t) : TauCeti.AnalyticOnSubmanifold d (g ∘ f) S

The composition of an analytic function on S with a function analytic on a set containing its values on S is analytic on S.