structure LocalisationData {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] (I' : ModelWithCorners 𝕜 E' H') {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] (f : M → M') : Type (max (max (max (max u_2 u_4) u_5) u_7) (u_8 + 1))

Definition def:localisation_data.

• cont : Continuous f
• ι' : Type u_8
• N : ℕ
• φ : IndexType self.N → OpenSmoothEmbedding (modelWithCornersSelf 𝕜 E) E I M
• ψ : self.ι' → OpenSmoothEmbedding (modelWithCornersSelf 𝕜 E') E' I' M'
• j : IndexType self.N → self.ι'
• h₁ : ⋃ (i : IndexType self.N), ↑(self.φ i) '' Metric.ball 0 1 = Set.univ
• h₂ : ⋃ (i' : self.ι'), ↑(self.ψ i') '' Metric.ball 0 1 = Set.univ
• h₃ (i : IndexType self.N) : Set.range (f ∘ ↑(self.φ i)) ⊆ ↑(self.ψ (self.j i)) '' Metric.ball 0 1
• h₄ : LocallyFinite fun (i' : self.ι') => Set.range ↑(self.ψ i')
• lf_φ : LocallyFinite fun (i : IndexType self.N) => Set.range ↑(self.φ i)

@[reducible, inline]

abbrev LocalisationData.ψj {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {f : M → M'} (ld : LocalisationData I I' f) : IndexType ld.N → OpenSmoothEmbedding (modelWithCornersSelf 𝕜 E') E' I' M'

Equations

• ld.ψj = ld.ψ ∘ ld.j

def LocalisationData.ι {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {f : M → M'} (L : LocalisationData I I' f) : Type

The type indexing the source charts of the given localisation data.

Equations

• L.ι = IndexType L.N

theorem LocalisationData.iUnion_succ' {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {f : M → M'} (ld : LocalisationData I I' f) {β : Type u_8} (s : ld.ι → Set β) (i : IndexType ld.N) : ⋃ (j : IndexType ld.N), ⋃ (_ : j ≤ i), s j = (⋃ (j : IndexType ld.N), ⋃ (_ : j < i), s j) ∪ s i

theorem nice_atlas_target (E' : Type u_4) [NormedAddCommGroup E'] [NormedSpace ℝ E'] [FiniteDimensional ℝ E'] {H' : Type u_5} [TopologicalSpace H'] (I' : ModelWithCorners ℝ E' H') [I'.Boundaryless] (M' : Type u_6) [MetricSpace M'] [SigmaCompactSpace M'] [LocallyCompactSpace M'] [Nonempty M'] [ChartedSpace H' M'] [IsManifold I' (↑⊤) M'] : ∃ (n : ℕ) (ψ : IndexType n → OpenSmoothEmbedding (modelWithCornersSelf ℝ E') E' I' M'), (LocallyFinite fun (i' : IndexType n) => Set.range ↑(ψ i')) ∧ ⋃ (i' : IndexType n), ↑(ψ i') '' Metric.ball 0 1 = Set.univ

def targetCharts (E' : Type u_4) [NormedAddCommGroup E'] [NormedSpace ℝ E'] [FiniteDimensional ℝ E'] {H' : Type u_5} [TopologicalSpace H'] (I' : ModelWithCorners ℝ E' H') [I'.Boundaryless] (M' : Type u_6) [MetricSpace M'] [SigmaCompactSpace M'] [LocallyCompactSpace M'] [Nonempty M'] [ChartedSpace H' M'] [IsManifold I' (↑⊤) M'] (i' : IndexType ⋯.choose) : OpenSmoothEmbedding (modelWithCornersSelf ℝ E') E' I' M'

A collection of charts on a manifold M' which are smooth open embeddings with domain the whole model space, and which cover the manifold when restricted in each case to the unit ball.

Equations

• targetCharts E' I' M' i' = ⋯.choose i'

theorem targetCharts_cover (E' : Type u_4) [NormedAddCommGroup E'] [NormedSpace ℝ E'] [FiniteDimensional ℝ E'] {H' : Type u_5} [TopologicalSpace H'] (I' : ModelWithCorners ℝ E' H') [I'.Boundaryless] (M' : Type u_6) [MetricSpace M'] [SigmaCompactSpace M'] [LocallyCompactSpace M'] [Nonempty M'] [ChartedSpace H' M'] [IsManifold I' (↑⊤) M'] : ⋃ (i' : IndexType ⋯.choose), ↑(targetCharts E' I' M' i') '' Metric.ball 0 1 = Set.univ

theorem nice_atlas_domain (E : Type u_1) [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {M : Type u_2} [TopologicalSpace M] [SigmaCompactSpace M] [LocallyCompactSpace M] [T2Space M] {H : Type u_3} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) [I.Boundaryless] [Nonempty M] [ChartedSpace H M] [IsManifold I (↑⊤) M] (E' : Type u_4) [NormedAddCommGroup E'] [NormedSpace ℝ E'] [FiniteDimensional ℝ E'] {H' : Type u_5} [TopologicalSpace H'] (I' : ModelWithCorners ℝ E' H') [I'.Boundaryless] {M' : Type u_6} [MetricSpace M'] [SigmaCompactSpace M'] [LocallyCompactSpace M'] [Nonempty M'] [ChartedSpace H' M'] [IsManifold I' (↑⊤) M'] {f : M → M'} (hf : Continuous f) : ∃ (n : ℕ) (φ : IndexType n → OpenSmoothEmbedding (modelWithCornersSelf ℝ E) E I M), (∀ (i : IndexType n), ∃ (i' : IndexType ⋯.choose), Set.range ↑(φ i) ⊆ f ⁻¹' (↑(targetCharts E' I' M' i') '' Metric.ball 0 1)) ∧ (LocallyFinite fun (i : IndexType n) => Set.range ↑(φ i)) ∧ ⋃ (i : IndexType n), ↑(φ i) '' Metric.ball 0 1 = Set.univ

def stdLocalisationData (E : Type u_1) [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {M : Type u_2} [TopologicalSpace M] [SigmaCompactSpace M] [LocallyCompactSpace M] [T2Space M] {H : Type u_3} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) [I.Boundaryless] [Nonempty M] [ChartedSpace H M] [IsManifold I (↑⊤) M] (E' : Type u_4) [NormedAddCommGroup E'] [NormedSpace ℝ E'] [FiniteDimensional ℝ E'] {H' : Type u_5} [TopologicalSpace H'] (I' : ModelWithCorners ℝ E' H') [I'.Boundaryless] {M' : Type u_6} [MetricSpace M'] [SigmaCompactSpace M'] [LocallyCompactSpace M'] [Nonempty M'] [ChartedSpace H' M'] [IsManifold I' (↑⊤) M'] {f : M → M'} (hf : Continuous f) : LocalisationData I I' f

Lemma lem:ex_localisation Any continuous map between manifolds has some localisation data.

Equations

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

theorem localisation_stability {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {M : Type u_2} [TopologicalSpace M] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [ChartedSpace H M] {E' : Type u_4} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [FiniteDimensional ℝ E'] {H' : Type u_5} [TopologicalSpace H'] {I' : ModelWithCorners ℝ E' H'} {M' : Type u_6} [MetricSpace M'] [ChartedSpace H' M'] {f : M → M'} (ld : LocalisationData I I' f) : ∃ (ε : M → ℝ) (_ : ∀ (m : M), 0 < ε m) (_ : Continuous ε), ∀ (g : M → M'), (∀ (m : M), dist (g m) (f m) < ε m) → ∀ (i : IndexType ld.N), Set.range (g ∘ ↑(ld.φ i)) ⊆ Set.range ↑(ld.ψj i)

Lemma lem:localisation_stability.

def LocalisationData.ε {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {M : Type u_2} [TopologicalSpace M] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [ChartedSpace H M] {E' : Type u_4} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [FiniteDimensional ℝ E'] {H' : Type u_5} [TopologicalSpace H'] {I' : ModelWithCorners ℝ E' H'} {M' : Type u_6} [MetricSpace M'] [ChartedSpace H' M'] {f : M → M'} (ld : LocalisationData I I' f) : M → ℝ

Equations

• ld.ε = ⋯.choose

theorem LocalisationData.ε_pos {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {M : Type u_2} [TopologicalSpace M] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [ChartedSpace H M] {E' : Type u_4} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [FiniteDimensional ℝ E'] {H' : Type u_5} [TopologicalSpace H'] {I' : ModelWithCorners ℝ E' H'} {M' : Type u_6} [MetricSpace M'] [ChartedSpace H' M'] {f : M → M'} (ld : LocalisationData I I' f) (m : M) : 0 < ld.ε m

theorem LocalisationData.ε_cont {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {M : Type u_2} [TopologicalSpace M] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [ChartedSpace H M] {E' : Type u_4} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [FiniteDimensional ℝ E'] {H' : Type u_5} [TopologicalSpace H'] {I' : ModelWithCorners ℝ E' H'} {M' : Type u_6} [MetricSpace M'] [ChartedSpace H' M'] {f : M → M'} (ld : LocalisationData I I' f) : Continuous ld.ε

theorem LocalisationData.ε_spec {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {M : Type u_2} [TopologicalSpace M] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [ChartedSpace H M] {E' : Type u_4} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [FiniteDimensional ℝ E'] {H' : Type u_5} [TopologicalSpace H'] {I' : ModelWithCorners ℝ E' H'} {M' : Type u_6} [MetricSpace M'] [ChartedSpace H' M'] {f : M → M'} (ld : LocalisationData I I' f) (g : M → M') (_hg : ∀ (m : M), dist (g m) (f m) < ld.ε m) (i : ld.ι) : Set.range (g ∘ ↑(ld.φ i)) ⊆ Set.range ↑(ld.ψj i)

theorem exists_stability_dist {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {M : Type u_2} [TopologicalSpace M] [SigmaCompactSpace M] [LocallyCompactSpace M] [T2Space M] {H : Type u_3} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) [I.Boundaryless] [Nonempty M] [ChartedSpace H M] [IsManifold I (↑⊤) M] {E' : Type u_4} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [FiniteDimensional ℝ E'] {H' : Type u_5} [TopologicalSpace H'] (I' : ModelWithCorners ℝ E' H') [I'.Boundaryless] {M' : Type u_6} [MetricSpace M'] [SigmaCompactSpace M'] [LocallyCompactSpace M'] [Nonempty M'] [ChartedSpace H' M'] [IsManifold I' (↑⊤) M'] {f : M → M'} (hf : Continuous f) : ∃ (ε : M → ℝ), (∀ (m : M), 0 < ε m) ∧ Continuous ε ∧ ∀ (x : M), ∃ (φ : OpenSmoothEmbedding (modelWithCornersSelf ℝ E) E I M) (ψ : OpenSmoothEmbedding (modelWithCornersSelf ℝ E') E' I' M'), x ∈ Set.range ↑φ ∧ ∀ (g : M → M'), (∀ (m : M), dist (g m) (f m) < ε m) → Set.range (g ∘ ↑φ) ⊆ Set.range ↑ψ