Real-analytic geometry and semianalytic triangulation
The declarations the status of Tau Ceti's roadmap names, and the other results named in the modules where only this status names declarations, or in folders below the areas where only it names 2 or more, as Tau Ceti has them at commit ace60277.
TheoremComplexification of a real analytic function on an open set#
A function of finitely many
real variables that is analytic on an open set U extends to a function F of as many complex
variables that is complex analytic on an open set W whose real points are exactly those of U.
The set W is invariant under complex conjugation, F agrees with f at the real points of
U, and F commutes with complex conjugation.
AnalyticOnNhd.exists_complexification.{u_1} {ι : Type u_1} [Fintype ι] {f : (ι → ℝ) → ℝ}
{U : Set (ι → ℝ)} (hf : AnalyticOnNhd ℝ f U) (hU : IsOpen U) :
∃ W,
IsOpen W ∧
(∀ (x : ι → ℝ), (fun i => ↑(x i)) ∈ W ↔ x ∈ U) ∧
(∀ (z : ι → ℂ), star z ∈ W ↔ z ∈ W) ∧
∃ F,
AnalyticOnNhd ℂ F W ∧
(∀ x ∈ U, (F fun i => ↑(x i)) = ↑(f x)) ∧ ∀ (z : ι → ℂ), F (star z) = star (F z)
Uses 1
TheoremComplexification of a real analytic map on an open set#
A map from ι → ℝ to κ → ℝ,
with ι and κ finite, that is analytic on an open set U extends to a map
F : (ι → ℂ) → (κ → ℂ) that is complex analytic on an open set W whose real points are exactly
those of U. The set W is invariant under complex conjugation, F agrees with f at the real
points of U, and F commutes with complex conjugation.
AnalyticOnNhd.exists_complexification_pi.{u_1, u_2} {ι : Type u_1} {κ : Type u_2} [Fintype ι]
[Fintype κ] {f : (ι → ℝ) → κ → ℝ} {U : Set (ι → ℝ)} (hf : AnalyticOnNhd ℝ f U) (hU : IsOpen U) :
∃ W,
IsOpen W ∧
(∀ (x : ι → ℝ), (fun i => ↑(x i)) ∈ W ↔ x ∈ U) ∧
(∀ (z : ι → ℂ), star z ∈ W ↔ z ∈ W) ∧
∃ F,
AnalyticOnNhd ℂ F W ∧
(∀ x ∈ U, (F fun i => ↑(x i)) = fun k => ↑(f x k)) ∧
∀ (z : ι → ℂ), F (star z) = star (F z)
Uses 1
TheoremUniqueness of complexifications#
Two complex analytic functions of finitely many variables
on an open neighborhood W of the real points of an open set U, agreeing at those real points,
agree on a smaller open set V ⊆ W that is invariant under complex conjugation and whose real
points are exactly those of U.
AnalyticOnNhd.exists_eqOn_of_forall_real.{u_1, u_3} {ι : Type u_1} [Fintype ι] {E : Type u_3}
[NormedAddCommGroup E] [NormedSpace ℂ E] {F G : (ι → ℂ) → E} {U : Set (ι → ℝ)} {W : Set (ι → ℂ)}
(hF : AnalyticOnNhd ℂ F W) (hG : AnalyticOnNhd ℂ G W) (hU : IsOpen U) (hW : IsOpen W)
(hUW : ∀ x ∈ U, (fun i => ↑(x i)) ∈ W) (hFG : ∀ x ∈ U, (F fun i => ↑(x i)) = G fun i => ↑(x i)) :
∃ V ⊆ W,
IsOpen V ∧
(∀ (x : ι → ℝ), (fun i => ↑(x i)) ∈ V ↔ x ∈ U) ∧
(∀ (z : ι → ℂ), star z ∈ V ↔ z ∈ V) ∧ Set.EqOn F G V
Uses 1
TheoremEquivalence of presentations#
A set is semianalytic at x if and only if, on some
neighbourhood U of x, it agrees with a finite union of sets
{y | f y = 0 ∧ 0 < g₁ y ∧ ⋯ ∧ 0 < gₖ y} with f, g₁, …, gₖ analytic on U.
TauCeti.semianalyticAt_iff_exists_iUnion.{u_1} {E : Type u_1} [NormedAddCommGroup E]
[NormedSpace ℝ E] {s : Set E} {x : E} :
TauCeti.SemianalyticAt s x ↔
∃ U ∈ nhds x,
∃ m k f g,
(∀ (i : Fin m), AnalyticOnNhd ℝ (f i) U) ∧
(∀ (i : Fin m) (j : Fin k), AnalyticOnNhd ℝ (g i j) U) ∧
s ∩ U = (⋃ i, {y | f i y = 0} ∩ ⋂ j, {y | 0 < g i j y}) ∩ U
Uses 1
TheoremAnalytic preimages#
The preimage of a semianalytic set under a real analytic map is semianalytic.
TauCeti.IsSemianalytic.preimage.{u_1, u_2} {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E]
[NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {s : Set F}
(hs : TauCeti.IsSemianalytic s) {g : E → F} (hg : AnalyticOnNhd ℝ g Set.univ) :
TauCeti.IsSemianalytic (g ⁻¹' s)
Uses 2 · Used by 1
TheoremAnalytic isomorphisms#
For a bijection e that is analytic with analytic inverse, the
image e '' s is semianalytic if and only if s is semianalytic.
Equiv.isSemianalytic_image_iff.{u_1, u_2} {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E]
[NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {s : Set E} (e : E ≃ F)
(he : AnalyticOnNhd ℝ (⇑e) Set.univ) (he' : AnalyticOnNhd ℝ (⇑e.symm) Set.univ) :
TauCeti.IsSemianalytic (⇑e '' s) ↔ TauCeti.IsSemianalytic s
Uses 2
TheoremGeometry.SimplicialComplex.space_cone_of_space_eq_intrinsicFrontier#
Coning a triangulation of the intrinsic frontier of a compact convex set C to a point of the
intrinsic interior of C triangulates C: every point of C is either the apex or lies on a
segment from the apex to a point of the intrinsic frontier.
Geometry.SimplicialComplex.space_cone_of_space_eq_intrinsicFrontier.{u_1} {E : Type u_1}
[AddCommGroup E] [_root_.Module ℝ E] [TopologicalSpace E] [IsTopologicalAddGroup E]
[ContinuousSMul ℝ E] [T2Space E] [DecidableEq E] {K : Geometry.SimplicialComplex ℝ E} {C : Set E}
{p : E} (hCc : IsCompact C) (hC : Convex ℝ C) (hK : K.space = intrinsicFrontier ℝ C)
(hp : p ∈ intrinsicInterior ℝ C) : (K.cone p ⋯).space = C
Lean
Formalized in Tau Ceti as Geometry.SimplicialComplex.space_cone_of_space_eq_intrinsicFrontier.
Sources
- Tau Ceti documentation:
Geometry.SimplicialComplex.space_cone_of_space_eq_intrinsicFrontier - Source of
Geometry.SimplicialComplex.space_cone_of_space_eq_intrinsicFrontierin TauCeti/Analysis/Convex/SimplicialComplex/Cone.lean - Tau Ceti roadmap status: Real-analytic geometry and semianalytic triangulation
Uses 2
DefinitionTauCeti.SemianalyticAt#
A set s ⊆ E is semianalytic at x if on some neighbourhood U of x it agrees with a
finite Boolean combination of zero sets and positivity sets of real functions analytic on U.
TauCeti.SemianalyticAt.{u_1} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (s : Set E)
(x : E) : Prop
DefinitionTauCeti.IsSemianalytic#
A set s ⊆ E is semianalytic if it is semianalytic at every point of E: near every point,
it agrees with a finite Boolean combination of zero sets and positivity sets of real analytic
functions defined near that point.
TauCeti.IsSemianalytic.{u_1} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (s : Set E) :
Prop
Uses 1 · Used by 4
TheoremLocally finite unions#
The union of a locally finite family of semianalytic sets is semianalytic.
LocallyFinite.isSemianalytic_iUnion.{u_1, u_3} {E : Type u_1} [NormedAddCommGroup E]
[NormedSpace ℝ E] {ι : Type u_3} {s : ι → Set E} (hfin : LocallyFinite s)
(hs : ∀ (i : ι), TauCeti.IsSemianalytic (s i)) : TauCeti.IsSemianalytic (⋃ i, s i)
Uses 2
TheoremTauCeti.IsSemialgebraic.isSemianalytic#
A semialgebraic subset of σ → ℝ, for a finite type σ, is semianalytic: polynomial
functions are analytic.
TauCeti.IsSemialgebraic.isSemianalytic.{u_3} {σ : Type u_3} [Fintype σ] {s : Set (σ → ℝ)}
(hs : TauCeti.IsSemialgebraic s) : TauCeti.IsSemianalytic s
Uses 2
DefinitionGeometry.SimplicialComplex.cone#
The cone pK on a simplicial complex K with apex p. Its faces are the nonempty finite sets
whose vertices other than p form a face of K or are empty: the faces of K, the faces of K
with p adjoined, and the vertex {p}.
Geometry.SimplicialComplex.cone.{u_1, u_2} {𝕜 : Type u_1} {E : Type u_2} [Field 𝕜] [LinearOrder 𝕜]
[IsStrictOrderedRing 𝕜] [AddCommGroup E] [_root_.Module 𝕜 E] [DecidableEq E]
(K : Geometry.SimplicialComplex 𝕜 E) (p : E) (h : K.IsConeApex p) : Geometry.SimplicialComplex 𝕜 E
Uses 1 · Used by 1
StructureGeometry.SimplicialComplex.IsConeApex#
A point p is a cone apex for a geometric simplicial complex K if p ∉ |K| and every
segment from p to a point y ∈ |K| meets |K| only at y. These are the conditions under
which joining p to the faces of K gives a simplicial complex, the cone K.cone p h.
Geometry.SimplicialComplex.IsConeApex.{u_1, u_2} {𝕜 : Type u_1} {E : Type u_2} [Field 𝕜]
[LinearOrder 𝕜] [AddCommGroup E] [_root_.Module 𝕜 E] (K : Geometry.SimplicialComplex 𝕜 E)
(p : E) : Prop
TheoremIdentity theorem on the real points#
A complex analytic function of finitely many variables that vanishes at the real points near a real point vanishes near that point.
AnalyticAt.eventually_eq_zero_of_eventually_real.{u_1, u_3} {ι : Type u_1} [Fintype ι]
{E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℂ E] {F : (ι → ℂ) → E} {a : ι → ℝ}
(hF : AnalyticAt ℂ F fun i => ↑(a i)) (h : ∀ᶠ (x : ι → ℝ) in nhds a, (F fun i => ↑(x i)) = 0) :
∀ᶠ (z : ι → ℂ) in nhds fun i => ↑(a i), F z = 0
Lean
Formalized in Tau Ceti as AnalyticAt.eventually_eq_zero_of_eventually_real.
Sources
Used by 8
TheoremReal analytic Weierstrass preparation theorem#
Let f : (ι → ℝ) × ℝ → ℝ be real analytic
at (x₀, t₀), with ι finite, and suppose the vertical slice t ↦ f (x₀, t) has finite order of
vanishing d at t₀. Then there exist real analytic coefficient functions c : Fin d → (ι → ℝ) →
ℝ vanishing at x₀ and a real analytic function u nonvanishing at (x₀, t₀) such that near
(x₀, t₀),
f (x, t) = (TauCeti.Polynomial.monicOfCoeff (fun i ↦ c i x)).eval (t - t₀) * u (x, t).
AnalyticAt.exists_weierstrassPreparation_real {ι : Type} [Fintype ι] {f : (ι → ℝ) × ℝ → ℝ}
{x₀ : ι → ℝ} {t₀ : ℝ} {d : ℕ} (hf : AnalyticAt ℝ f (x₀, t₀))
(hd : analyticOrderAt (fun t => f (x₀, t)) t₀ = ↑d) :
∃ c u,
(∀ (i : Fin d), AnalyticAt ℝ (c i) x₀) ∧
(∀ (i : Fin d), c i x₀ = 0) ∧
AnalyticAt ℝ u (x₀, t₀) ∧
u (x₀, t₀) ≠ 0 ∧
f =ᶠ[nhds (x₀, t₀)] fun p =>
Polynomial.eval (p.2 - t₀) (TauCeti.Polynomial.monicOfCoeff fun i => c i p.1) * u p
Uses 2
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.