Semianalytic sets

A subset s of a real normed space E is semianalytic at a point x if, on some neighbourhood U of x, it agrees with a finite Boolean combination of zero sets {y | f y = 0} and positivity sets {y | 0 < f y} of real functions f analytic on U. The functions, the neighbourhood and the Boolean formula may all depend on x. The set s is semianalytic if it is semianalytic at every point of E, including the points outside s and its frontier points.

We record the finite Boolean combinations over a fixed set U as TauCeti.IsAnalyticBooleanCombination U t: membership of t in the algebra of sets (MeasureTheory.generateSetAlgebra) generated by the zero sets and positivity sets of the functions analytic on U, in the same way as TauCeti.IsSemialgebraic is defined from polynomials.

Main declarations

• TauCeti.IsAnalyticBooleanCombination U t: t is a finite Boolean combination of zero sets and positivity sets of functions analytic on U.
• TauCeti.SemianalyticAt s x: s is semianalytic at x.
• TauCeti.IsSemianalytic s: s is semianalytic at every point.

Main results

• TauCeti.IsAnalyticBooleanCombination.exists_eq_setOf_sign: the sign-condition normal form; a finite Boolean combination over U is described by a condition on the signs of finitely many functions analytic on U.
• TauCeti.SemianalyticAt.exists_subset: a presentation exists on every sufficiently small neighbourhood, and TauCeti.semianalyticAt_congr: being semianalytic at x depends only on the germ of the set at x.
• TauCeti.semianalyticAt_iff_exists_iUnion: equivalence of presentations; near x a set is semianalytic if and only if it is a finite union of sets {f = 0, g₁ > 0, …, gₖ > 0} with f, g₁, …, gₖ analytic on the neighbourhood.
• Finite Boolean operations: TauCeti.isSetAlgebra_setOf_semianalyticAt and TauCeti.isSetAlgebra_setOf_isSemianalytic, with the named consequences, and LocallyFinite.isSemianalytic_iUnion for locally finite unions.
• TauCeti.SemianalyticAt.preimage_of_analyticOnNhd, TauCeti.SemianalyticAt.preimage and TauCeti.IsSemianalytic.preimage: preimages under analytic maps; Equiv.isSemianalytic_image_iff: invariance under analytic isomorphisms, and PartialEquiv.semianalyticAt_preimage_symm_iff: its pointwise form for local analytic isomorphisms such as charts.
• TauCeti.IsSemialgebraic.isSemianalytic: semialgebraic subsets of σ → ℝ are semianalytic.

References

S. Łojasiewicz, Triangulation of semi-analytic sets, Annali della Scuola Normale Superiore di Pisa (3) 18 (1964), 449–474, §1, for the definition of semianalytic sets.

E. Bierstone and P. D. Milman, Semianalytic and subanalytic sets, Publications Mathématiques de l'IHÉS 67 (1988), 5–42, §2, for the normal form with a single equation in each conjunct.

Finite Boolean combinations of analytic sign conditions

def TauCeti.IsAnalyticBooleanCombination {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (U t : Set E) : Prop

A set t ⊆ E is a finite Boolean combination of analytic sign conditions on U if it belongs to the algebra of sets generated by the zero sets {x | f x = 0} and the positivity sets {x | 0 < f x} of the real functions f analytic on U. Only the part of t inside U is meaningful for semianalyticity.

theorem TauCeti.isAnalyticBooleanCombination_def {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {U t : Set E} : IsAnalyticBooleanCombination U t ↔ t ∈ MeasureTheory.generateSetAlgebra ({t : Set E | ∃ (f : E → ℝ), AnalyticOnNhd ℝ f U ∧ t = {x : E | f x = 0}} ∪ {t : Set E | ∃ (f : E → ℝ), AnalyticOnNhd ℝ f U ∧ t = {x : E | 0 < f x}})

A set is a finite Boolean combination of analytic sign conditions on U if and only if it belongs to the algebra of sets generated by the zero sets and positivity sets of the functions analytic on U.

theorem TauCeti.isAnalyticBooleanCombination_setOf_eq_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {U : Set E} {f : E → ℝ} (hf : AnalyticOnNhd ℝ f U) : IsAnalyticBooleanCombination U {x : E | f x = 0}

The zero set of a function analytic on U is a Boolean combination of analytic sign conditions on U.

theorem TauCeti.isAnalyticBooleanCombination_setOf_pos {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {U : Set E} {f : E → ℝ} (hf : AnalyticOnNhd ℝ f U) : IsAnalyticBooleanCombination U {x : E | 0 < f x}

The positivity set of a function analytic on U is a Boolean combination of analytic sign conditions on U.

theorem TauCeti.isSetAlgebra_setOf_isAnalyticBooleanCombination {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (U : Set E) : MeasureTheory.IsSetAlgebra {t : Set E | IsAnalyticBooleanCombination U t}

The finite Boolean combinations of analytic sign conditions on U form an algebra of sets.

theorem TauCeti.setOf_isAnalyticBooleanCombination_subset {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {U : Set E} {ℬ : Set (Set E)} (hℬ : MeasureTheory.IsSetAlgebra ℬ) (pos : ∀ (f : E → ℝ), AnalyticOnNhd ℝ f U → {x : E | 0 < f x} ∈ ℬ) : {t : Set E | IsAnalyticBooleanCombination U t} ⊆ ℬ

The finite Boolean combinations of analytic sign conditions on U form the smallest algebra of sets containing the zero set and the positivity set of every function analytic on U.

@[simp]

theorem TauCeti.isAnalyticBooleanCombination_empty {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (U : Set E) : IsAnalyticBooleanCombination U ∅

The empty set is a Boolean combination of analytic sign conditions.

@[simp]

theorem TauCeti.isAnalyticBooleanCombination_univ {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (U : Set E) : IsAnalyticBooleanCombination U Set.univ

The whole space is a Boolean combination of analytic sign conditions.

theorem TauCeti.IsAnalyticBooleanCombination.compl {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {U t : Set E} (ht : IsAnalyticBooleanCombination U t) : IsAnalyticBooleanCombination U tᶜ

The complement of a Boolean combination of analytic sign conditions is one.

theorem TauCeti.IsAnalyticBooleanCombination.union {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {U t t' : Set E} (ht : IsAnalyticBooleanCombination U t) (ht' : IsAnalyticBooleanCombination U t') : IsAnalyticBooleanCombination U (t ∪ t')

The union of two Boolean combinations of analytic sign conditions is one.

theorem TauCeti.IsAnalyticBooleanCombination.inter {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {U t t' : Set E} (ht : IsAnalyticBooleanCombination U t) (ht' : IsAnalyticBooleanCombination U t') : IsAnalyticBooleanCombination U (t ∩ t')

The intersection of two Boolean combinations of analytic sign conditions is one.

theorem TauCeti.IsAnalyticBooleanCombination.sdiff {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {U t t' : Set E} (ht : IsAnalyticBooleanCombination U t) (ht' : IsAnalyticBooleanCombination U t') : IsAnalyticBooleanCombination U (t \ t')

The difference of two Boolean combinations of analytic sign conditions is one.

theorem TauCeti.IsAnalyticBooleanCombination.biUnion {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {U : Set E} {ι : Type u_3} {I : Set ι} (hI : I.Finite) {t : ι → Set E} (ht : ∀ i ∈ I, IsAnalyticBooleanCombination U (t i)) : IsAnalyticBooleanCombination U (⋃ i ∈ I, t i)

A finite union of Boolean combinations of analytic sign conditions is one.

theorem TauCeti.IsAnalyticBooleanCombination.biInter {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {U : Set E} {ι : Type u_3} {I : Set ι} (hI : I.Finite) {t : ι → Set E} (ht : ∀ i ∈ I, IsAnalyticBooleanCombination U (t i)) : IsAnalyticBooleanCombination U (⋂ i ∈ I, t i)

A finite intersection of Boolean combinations of analytic sign conditions is one.

theorem TauCeti.IsAnalyticBooleanCombination.iUnion {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {U : Set E} {ι : Type u_3} [Finite ι] {t : ι → Set E} (ht : ∀ (i : ι), IsAnalyticBooleanCombination U (t i)) : IsAnalyticBooleanCombination U (⋃ (i : ι), t i)

The union of a finite family of Boolean combinations of analytic sign conditions is one.

theorem TauCeti.IsAnalyticBooleanCombination.iInter {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {U : Set E} {ι : Type u_3} [Finite ι] {t : ι → Set E} (ht : ∀ (i : ι), IsAnalyticBooleanCombination U (t i)) : IsAnalyticBooleanCombination U (⋂ (i : ι), t i)

The intersection of a finite family of Boolean combinations of analytic sign conditions is one.

theorem TauCeti.IsAnalyticBooleanCombination.mono {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {U V t : Set E} (ht : IsAnalyticBooleanCombination U t) (hVU : V ⊆ U) : IsAnalyticBooleanCombination V t

A Boolean combination of sign conditions of functions analytic on U is also one for functions analytic on any smaller set V ⊆ U.

theorem TauCeti.IsAnalyticBooleanCombination.preimage {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {V : Set E} {U t : Set F} (ht : IsAnalyticBooleanCombination U t) {g : E → F} (hg : AnalyticOnNhd ℝ g V) (hgVU : Set.MapsTo g V U) : IsAnalyticBooleanCombination V (g ⁻¹' t)

The preimage of a Boolean combination of analytic sign conditions on U under a map g analytic on V and mapping V into U is a Boolean combination of analytic sign conditions on V.

theorem TauCeti.isAnalyticBooleanCombination_setOf_sign_eq {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {U : Set E} {f : E → ℝ} (hf : AnalyticOnNhd ℝ f U) (ε : SignType) : IsAnalyticBooleanCombination U {x : E | SignType.sign (f x) = ε}

The set where a function analytic on U has a prescribed sign is a Boolean combination of analytic sign conditions on U.

theorem TauCeti.isAnalyticBooleanCombination_setOf_sign {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {U : Set E} {ι : Type u_3} [Finite ι] {f : ι → E → ℝ} (hf : ∀ (i : ι), AnalyticOnNhd ℝ (f i) U) (Φ : (ι → SignType) → Prop) : IsAnalyticBooleanCombination U {x : E | Φ fun (i : ι) => SignType.sign (f i x)}

A condition on the signs of finitely many functions analytic on U defines a Boolean combination of analytic sign conditions on U.

theorem TauCeti.IsAnalyticBooleanCombination.exists_eq_setOf_sign {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {U t : Set E} (ht : IsAnalyticBooleanCombination U t) : ∃ (m : ℕ) (f : Fin m → E → ℝ), (∀ (i : Fin m), AnalyticOnNhd ℝ (f i) U) ∧ ∃ (Φ : (Fin m → SignType) → Prop), t = {x : E | Φ fun (i : Fin m) => SignType.sign (f i x)}

Sign-condition normal form. A Boolean combination of analytic sign conditions on U is described by a condition on the signs of finitely many functions analytic on U.

Semianalyticity at a point

def TauCeti.SemianalyticAt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (s : Set E) (x : E) : Prop

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.

theorem TauCeti.semianalyticAt_def {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {s : Set E} {x : E} : SemianalyticAt s x ↔ ∃ U ∈ nhds x, ∃ (t : Set E), IsAnalyticBooleanCombination U t ∧ s ∩ U = t ∩ U

A set is semianalytic at x if and only 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.

theorem TauCeti.SemianalyticAt.exists_subset {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {s V : Set E} {x : E} (hs : SemianalyticAt s x) (hV : V ∈ nhds x) : ∃ U ∈ nhds x, U ⊆ V ∧ ∃ (t : Set E), IsAnalyticBooleanCombination U t ∧ s ∩ U = t ∩ U

Shrinking invariance. If s is semianalytic at x, then it has a presentation on a neighbourhood of x inside any prescribed neighbourhood V of x.

theorem TauCeti.SemianalyticAt.congr {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {s s' : Set E} {x : E} (hs : SemianalyticAt s x) (h : s =ᶠ[nhds x] s') : SemianalyticAt s' x

Being semianalytic at x only depends on the germ of the set at x.

theorem TauCeti.semianalyticAt_congr {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {s s' : Set E} {x : E} (h : s =ᶠ[nhds x] s') : SemianalyticAt s x ↔ SemianalyticAt s' x

Being semianalytic at x only depends on the germ of the set at x.

theorem AnalyticAt.semianalyticAt_setOf_eq_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {x : E} (hf : AnalyticAt ℝ f x) : TauCeti.SemianalyticAt {y : E | f y = 0} x

The zero set of a function analytic at x is semianalytic at x.

theorem AnalyticAt.semianalyticAt_setOf_pos {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {x : E} (hf : AnalyticAt ℝ f x) : TauCeti.SemianalyticAt {y : E | 0 < f y} x

The positivity set of a function analytic at x is semianalytic at x.

theorem TauCeti.isSetAlgebra_setOf_semianalyticAt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (x : E) : MeasureTheory.IsSetAlgebra {s : Set E | SemianalyticAt s x}

The sets semianalytic at a point form an algebra of sets.

@[simp]

theorem TauCeti.semianalyticAt_empty {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {x : E} : SemianalyticAt ∅ x

The empty set is semianalytic at every point.

@[simp]

theorem TauCeti.semianalyticAt_univ {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {x : E} : SemianalyticAt Set.univ x

The whole space is semianalytic at every point.

theorem TauCeti.SemianalyticAt.compl {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {s : Set E} {x : E} (hs : SemianalyticAt s x) : SemianalyticAt sᶜ x

The complement of a set semianalytic at x is semianalytic at x.

@[simp]

theorem TauCeti.semianalyticAt_compl_iff {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {s : Set E} {x : E} : SemianalyticAt sᶜ x ↔ SemianalyticAt s x

A set is semianalytic at x if and only if its complement is.

theorem TauCeti.SemianalyticAt.union {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {s s' : Set E} {x : E} (hs : SemianalyticAt s x) (hs' : SemianalyticAt s' x) : SemianalyticAt (s ∪ s') x

The union of two sets semianalytic at x is semianalytic at x.

theorem TauCeti.SemianalyticAt.inter {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {s s' : Set E} {x : E} (hs : SemianalyticAt s x) (hs' : SemianalyticAt s' x) : SemianalyticAt (s ∩ s') x

The intersection of two sets semianalytic at x is semianalytic at x.

theorem TauCeti.SemianalyticAt.sdiff {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {s s' : Set E} {x : E} (hs : SemianalyticAt s x) (hs' : SemianalyticAt s' x) : SemianalyticAt (s \ s') x

The difference of two sets semianalytic at x is semianalytic at x.

theorem TauCeti.SemianalyticAt.biUnion {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {x : E} {ι : Type u_3} {I : Set ι} (hI : I.Finite) {s : ι → Set E} (hs : ∀ i ∈ I, SemianalyticAt (s i) x) : SemianalyticAt (⋃ i ∈ I, s i) x

A finite union of sets semianalytic at x is semianalytic at x.

theorem TauCeti.SemianalyticAt.biInter {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {x : E} {ι : Type u_3} {I : Set ι} (hI : I.Finite) {s : ι → Set E} (hs : ∀ i ∈ I, SemianalyticAt (s i) x) : SemianalyticAt (⋂ i ∈ I, s i) x

A finite intersection of sets semianalytic at x is semianalytic at x.

theorem TauCeti.SemianalyticAt.iUnion {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {x : E} {ι : Type u_3} [Finite ι] {s : ι → Set E} (hs : ∀ (i : ι), SemianalyticAt (s i) x) : SemianalyticAt (⋃ (i : ι), s i) x

The union of a finite family of sets semianalytic at x is semianalytic at x.

theorem TauCeti.SemianalyticAt.iInter {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {x : E} {ι : Type u_3} [Finite ι] {s : ι → Set E} (hs : ∀ (i : ι), SemianalyticAt (s i) x) : SemianalyticAt (⋂ (i : ι), s i) x

The intersection of a finite family of sets semianalytic at x is semianalytic at x.

theorem TauCeti.SemianalyticAt.preimage {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {x : E} {s : Set F} {g : E → F} (hs : SemianalyticAt s (g x)) (hg : AnalyticAt ℝ g x) : SemianalyticAt (g ⁻¹' s) x

Analytic preimages. The preimage of a set semianalytic at g x under a map g analytic at x is semianalytic at x.

theorem TauCeti.SemianalyticAt.preimage_of_analyticOnNhd {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {x : E} {s : Set F} {g : E → F} {W : Set E} (hs : SemianalyticAt s (g x)) (hW : W ∈ nhds x) (hg : AnalyticOnNhd ℝ g W) : SemianalyticAt (g ⁻¹' s) x

Analytic preimages. The preimage of a set semianalytic at g x under a map g analytic on a neighbourhood W of x is semianalytic at x.

Equivalence of presentations

theorem TauCeti.semianalyticAt_iff_exists_iUnion {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {s : Set E} {x : E} : SemianalyticAt s x ↔ ∃ U ∈ nhds x, ∃ (m : ℕ) (k : ℕ) (f : Fin m → E → ℝ) (g : Fin m → Fin k → E → ℝ), (∀ (i : Fin m), AnalyticOnNhd ℝ (f i) U) ∧ (∀ (i : Fin m) (j : Fin k), AnalyticOnNhd ℝ (g i j) U) ∧ s ∩ U = (⋃ (i : Fin m), {y : E | f i y = 0} ∩ ⋂ (j : Fin k), {y : E | 0 < g i j y}) ∩ U

Equivalence 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.

Semianalytic sets

def TauCeti.IsSemianalytic {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (s : Set E) : Prop

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.

theorem TauCeti.isSemianalytic_iff {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {s : Set E} : IsSemianalytic s ↔ ∀ (x : E), SemianalyticAt s x

A set is semianalytic if and only if it is semianalytic at every point.

theorem TauCeti.IsSemianalytic.semianalyticAt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {s : Set E} (hs : IsSemianalytic s) (x : E) : SemianalyticAt s x

A semianalytic set is semianalytic at every point.

theorem AnalyticOnNhd.isSemianalytic_setOf_eq_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} (hf : AnalyticOnNhd ℝ f Set.univ) : TauCeti.IsSemianalytic {x : E | f x = 0}

The zero set of a real analytic function is semianalytic.

theorem AnalyticOnNhd.isSemianalytic_setOf_pos {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} (hf : AnalyticOnNhd ℝ f Set.univ) : TauCeti.IsSemianalytic {x : E | 0 < f x}

The positivity set of a real analytic function is semianalytic.

theorem TauCeti.isSetAlgebra_setOf_isSemianalytic (E : Type u_1) [NormedAddCommGroup E] [NormedSpace ℝ E] : MeasureTheory.IsSetAlgebra {s : Set E | IsSemianalytic s}

The semianalytic sets form an algebra of sets.

@[simp]

theorem TauCeti.isSemianalytic_empty {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] : IsSemianalytic ∅

The empty set is semianalytic.

@[simp]

theorem TauCeti.isSemianalytic_univ {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] : IsSemianalytic Set.univ

The whole space is semianalytic.

theorem TauCeti.IsSemianalytic.compl {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {s : Set E} (hs : IsSemianalytic s) : IsSemianalytic sᶜ

The complement of a semianalytic set is semianalytic.

theorem TauCeti.IsSemianalytic.union {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {s s' : Set E} (hs : IsSemianalytic s) (hs' : IsSemianalytic s') : IsSemianalytic (s ∪ s')

The union of two semianalytic sets is semianalytic.

theorem TauCeti.IsSemianalytic.inter {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {s s' : Set E} (hs : IsSemianalytic s) (hs' : IsSemianalytic s') : IsSemianalytic (s ∩ s')

The intersection of two semianalytic sets is semianalytic.

theorem TauCeti.IsSemianalytic.sdiff {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {s s' : Set E} (hs : IsSemianalytic s) (hs' : IsSemianalytic s') : IsSemianalytic (s \ s')

The difference of two semianalytic sets is semianalytic.

theorem TauCeti.IsSemianalytic.biUnion {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {ι : Type u_3} {I : Set ι} (hI : I.Finite) {s : ι → Set E} (hs : ∀ i ∈ I, IsSemianalytic (s i)) : IsSemianalytic (⋃ i ∈ I, s i)

A finite union of semianalytic sets is semianalytic.

theorem TauCeti.IsSemianalytic.biInter {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {ι : Type u_3} {I : Set ι} (hI : I.Finite) {s : ι → Set E} (hs : ∀ i ∈ I, IsSemianalytic (s i)) : IsSemianalytic (⋂ i ∈ I, s i)

A finite intersection of semianalytic sets is semianalytic.

theorem TauCeti.IsSemianalytic.iUnion {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {ι : Type u_3} [Finite ι] {s : ι → Set E} (hs : ∀ (i : ι), IsSemianalytic (s i)) : IsSemianalytic (⋃ (i : ι), s i)

The union of a finite family of semianalytic sets is semianalytic.

theorem TauCeti.IsSemianalytic.iInter {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {ι : Type u_3} [Finite ι] {s : ι → Set E} (hs : ∀ (i : ι), IsSemianalytic (s i)) : IsSemianalytic (⋂ (i : ι), s i)

The intersection of a finite family of semianalytic sets is semianalytic.

theorem TauCeti.IsSemianalytic.preimage {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {s : Set F} (hs : IsSemianalytic s) {g : E → F} (hg : AnalyticOnNhd ℝ g Set.univ) : IsSemianalytic (g ⁻¹' s)

Analytic preimages. The preimage of a semianalytic set under a real analytic map is semianalytic.

@[simp]

theorem TauCeti.isSemianalytic_compl_iff {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {s : Set E} : IsSemianalytic sᶜ ↔ IsSemianalytic s

A set is semianalytic if and only if its complement is.

theorem LocallyFinite.isSemianalytic_iUnion {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)

Locally finite unions. The union of a locally finite family of semianalytic sets is semianalytic.

theorem PartialEquiv.semianalyticAt_preimage_symm_iff {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {s : Set E} {x : E} (e : PartialEquiv E F) (hx : e.source ∈ nhds x) (he : AnalyticAt ℝ (↑e) x) (he' : AnalyticAt ℝ (↑e.symm) (↑e x)) : TauCeti.SemianalyticAt (↑e.symm ⁻¹' s) (↑e x) ↔ TauCeti.SemianalyticAt s x

Analytic isomorphisms, locally. For a partial equivalence e whose source is a neighbourhood of x, with e analytic at x and its inverse analytic at e x, the set e.symm ⁻¹' s is semianalytic at e x if and only if s is semianalytic at x. This applies to charts and other local analytic isomorphisms.

theorem Equiv.semianalyticAt_image_iff {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {s : Set E} {x : E} (e : E ≃ F) (he : AnalyticAt ℝ (⇑e) x) (he' : AnalyticAt ℝ (⇑e.symm) (e x)) : TauCeti.SemianalyticAt (⇑e '' s) (e x) ↔ TauCeti.SemianalyticAt s x

Analytic isomorphisms, locally. For a bijection e analytic at x whose inverse is analytic at e x, the image e '' s is semianalytic at e x if and only if s is semianalytic at x.

theorem Equiv.isSemianalytic_image_iff {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) _root_.Set.univ) (he' : AnalyticOnNhd ℝ (⇑e.symm) _root_.Set.univ) : TauCeti.IsSemianalytic (⇑e '' s) ↔ TauCeti.IsSemianalytic s

Analytic isomorphisms. For a bijection e that is analytic with analytic inverse, the image e '' s is semianalytic if and only if s is semianalytic.

theorem TauCeti.IsSemialgebraic.isSemianalytic {σ : Type u_3} [Fintype σ] {s : Set (σ → ℝ)} (hs : IsSemialgebraic s) : IsSemianalytic s

A semialgebraic subset of σ → ℝ, for a finite type σ, is semianalytic: polynomial functions are analytic.

theorem TauCeti.IsSemialgebraic.isAnalyticBooleanCombination_preimage {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {A : Type u_3} {S : Set (A → ℝ)} (hS : IsSemialgebraic S) {U : Set E} {c : E → A → ℝ} (hc : ∀ (a : A), AnalyticOnNhd ℝ (fun (x : E) => c x a) U) : IsAnalyticBooleanCombination U (c ⁻¹' S)

Substituting analytic functions. The preimage of a semialgebraic set S ⊆ A → ℝ under a map c whose coordinates c · a are analytic on U is a Boolean combination of analytic sign conditions on U.