Coordinates.lean`

17 declarations, 0 contain sorry, 0 declared as axioms

abbrev OAI.SmoothObstruction.ManifoldCoordinates.E line 14
def OAI.SmoothObstruction.ManifoldCoordinates.coord line 16
def OAI.SmoothObstruction.ManifoldCoordinates.domain line 20
theorem OAI.SmoothObstruction.ManifoldCoordinates.continuousOn_coord line 25
Source documentation
The genuine derivative in any independently fixed pair of regular charts, including half-space charts.
```
theorem continuousOn_coord (S : Diffeomorph I I M M ∞) (a b : M) :
    ContinuousOn (coord I S a b) (domain I S a b) := by
…
```
Mentions: OAI.SmoothObstruction.ManifoldCoordinates.coord, OAI.SmoothObstruction.ManifoldCoordinates.domain
def OAI.SmoothObstruction.ManifoldCoordinates.coordEquiv line 53
theorem OAI.SmoothObstruction.ManifoldCoordinates.coordEquiv_coe line 59
theorem OAI.SmoothObstruction.ManifoldCoordinates.bijective_coord line 66
Source documentation
The represented derivative is invertible at every point of its actual coordinate domain. This is not postulated as a cocycle input.
```
theorem bijective_coord (S : Diffeomorph I I M M ∞) (a b x : M)
    (hx : x∈domain I S a b) : Function.Bijective (coord I S a b x) := by
…
```
Mentions: OAI.SmoothObstruction.ManifoldCoordinates.domain, OAI.SmoothObstruction.ManifoldCoordinates.coord
theorem OAI.SmoothObstruction.ManifoldCoordinates.bound_on_compact line 72
Source documentation
Uniform two-sided derivative bounds on any compact chart-pair patch.
```
theorem bound_on_compact (S : Diffeomorph I I M M ∞) (a b : M)
    {K : Set M} (hK : IsCompact K) (hsub : K⊆domain I S a b) :
    ∃ C : ℝ, 0<C ∧ ∀ x∈K, ‖coord I S a b x‖≤C ∧
      ∀ v, ‖v‖≤C*‖coord I S a b x v‖ := by
…
```
Mentions: OAI.SmoothObstruction.ManifoldCoordinates.domain, OAI.SmoothObstruction.ManifoldCoordinates.coord

theorem OAI.SmoothObstruction.FiniteAtlas.compact_inner_cover line 114

Source documentation

Compact inner patches covering the whole compact space. This applies to half-space and nonorientable atlas charts without a global frame.

theorem compact_inner_cover (U : M → Set M) (hU : ∀ x,IsOpen (U x))
    (hxU : ∀ x,x∈U x) :
    ∃ (ι : Type u) (_ : Fintype ι) (a : ι → M) (K : ι → Set M),
      (∀ i,IsCompact (K i)) ∧ (∀ i,K i⊆U (a i)) ∧ ∀ x,∃ i,x∈K i := by
…

theorem OAI.SmoothObstruction.FiniteAtlas.measurable_selector line 132
Source documentation
Deterministic measurable choice of the first containing compact patch. No measurable selection theorem is postulated.
```
theorem measurable_selector (K : ι → Set Ω) (hK : ∀ i,MeasurableSet (K i))
    (hcover : ∀ x,∃ i,x∈K i) :
    ∃ a : Ω → ι,Measurable a ∧ ∀ x,x∈K (a x) := by
…
```
abbrev OAI.SmoothObstruction.CompactMatrix.Alphabet line 177
Source documentation
Compact alphabet of uniformly bounded, uniformly invertible derivative matrices. The coercion remembers the actual matrix, not an extra axiom.
```
abbrev Alphabet (d : ℕ) (K : ℝ) :=
…
```
instance OAI.SmoothObstruction.CompactMatrix.(instance at line 181) line 181
lemma OAI.SmoothObstruction.CompactMatrix.injective line 200
def OAI.SmoothObstruction.CompactMatrix.equiv line 206
lemma OAI.SmoothObstruction.CompactMatrix.equiv_coe line 211
lemma OAI.SmoothObstruction.CompactMatrix.continuous_equiv line 214

theorem OAI.SmoothObstruction.ManifoldCoordinates.actual_coordinate_cocycle_discrete line 230

Source documentation

A bounded measurable cocycle of the genuine derivative, in a finite system of measurable chart regions with compact inner patches.

theorem actual_coordinate_cocycle_discrete (S : Diffeomorph I I M M ∞) :
    ∃ (ι : Type u) (_ : Fintype ι) (_ : MeasurableSpace ι) (_ : MeasurableSingletonClass ι)
      (a : ι → M) (K : ι → Set M) (c : M → ι) (C : ℝ)
      (A : M → CompactMatrix.Alphabet d C),
      (∀ i,IsCompact (K i)) ∧ (∀ i,K i⊆(chartAt H (a i)).source) ∧
      Measurable c ∧ (∀ x,x∈K (c x)) ∧ 0<C ∧ Measurable A ∧
      ∀ x,(A x).val=coord I S (a (c x)) (a (c (S x))) x := by
…

Mentions: OAI.SmoothObstruction.CompactMatrix.Alphabet, OAI.SmoothObstruction.ManifoldCoordinates.coord