CoordinateTubes.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

def OAI.SmoothObstruction.CoordinateTubes.carrier line 24
Source documentation
Ambient open carrier of an arbitrary open subset of a chart source. It does not assert a smooth extension across a manifold boundary.
```
def carrier (a : M) (U : Set M) : Set (EuclideanSpace ℝ (Fin d)) :=
…
```
lemma OAI.SmoothObstruction.CoordinateTubes.isOpen_carrier line 27
lemma OAI.SmoothObstruction.CoordinateTubes.coord_mem_carrier line 30
lemma OAI.SmoothObstruction.CoordinateTubes.mem_of_coord_mem_carrier line 41

theorem OAI.SmoothObstruction.CoordinateTubes.uniform_margin line 49

Source documentation

Compact charts provide a uniform positive COORDINATE margin for any specified finite open enlargement, also in half-space models.

theorem uniform_margin {ι : Type*} [Fintype ι] (a : ι → M) (K U : ι → Set M)
    (hK : ∀ i,IsCompact (K i)) (hU : ∀ i,IsOpen (U i))
    (hKU : ∀ i,K i⊆U i) (hKs : ∀ i,K i⊆(chartAt H (a i)).source) :
    ∃ δ : ℝ,0<δ ∧ ∀ i x,x∈K i → ∀ y,y∈(chartAt H (a i)).source →
      ‖(extChartAt I (a i)) y-(extChartAt I (a i)) x‖≤δ → y∈U i := by
…

theorem OAI.SmoothObstruction.CoordinateTubes.uniform_metric_tube line 81

Source documentation

In a compatible metric, the same coordinate margin puts nearby carried points in any prescribed geometric atlas tube.

theorem uniform_metric_tube {ι : Type*} [Fintype ι]
    (a : ι → M) (K : ι → Set M) (hK : ∀ i,IsCompact (K i))
    (hKs : ∀ i,K i⊆(chartAt H (a i)).source) {r : ℝ} (hr : 0<r) :
    ∃ δ : ℝ,0<δ ∧ ∀ i x,x∈K i → ∀ y,y∈(chartAt H (a i)).source →
      ‖(extChartAt I (a i)) y-(extChartAt I (a i)) x‖≤δ →
        y∈cthickening r (K i) := by
…

theorem OAI.SmoothObstruction.CoordinateTubes.uniform_inverse_modulus line 102

Source documentation

Uniform inverse-chart modulus on finitely many compact patches. This works with a closed model range, so includes the closed half-space without postulating an ambient extension of an inverse chart.

theorem uniform_inverse_modulus {ι : Type*} [Fintype ι]
    (hclosed : IsClosed (range I)) (a : ι → M) (K : ι → Set M)
    (hK : ∀ i,IsCompact (K i)) (hKs : ∀ i,K i⊆(chartAt H (a i)).source)
    {ε : ℝ} (hε : 0<ε) :
    ∃ δ : ℝ,0<δ ∧ ∀ i x,x∈K i → ∀ y,y∈(chartAt H (a i)).source →
      ‖(extChartAt I (a i)) y-(extChartAt I (a i)) x‖≤δ → dist y x<ε := by
…

theorem OAI.SmoothObstruction.CoordinateTubes.uniform_target_tube line 154

Source documentation

A uniform coordinate ball restricted to the model range lies in the actual inverse-chart domain. This is a target statement, not an assertion about the total value assigned to a partial chart outside its source.

theorem uniform_target_tube {ι : Type*} [Fintype ι]
    (a : ι → M) (K : ι → Set M) (hK : ∀ i,IsCompact (K i))
    (hKs : ∀ i,K i⊆(chartAt H (a i)).source) :
    ∃ r : ℝ,0<r ∧ ∀ i x,x∈K i →
      closedBall ((extChartAt I (a i)) x) r∩range I⊆(extChartAt I (a i)).target := by
…

def OAI.SmoothObstruction.ManifoldCoordinates.BilateralGauge.restrict line 185
Source documentation
Restriction of an actual bilateral gauge keeps exactly the same bases, not a recomputed QR path or a newly chosen stationary witness.
```
def BilateralGauge.restrict (S : Diffeomorph I I M M ∞) (a : ι → M) (c : M → ι)
    {n N : ℕ} {B R : ℝ} {x : M} (A : BilateralGauge I S a c n B R x) (hN : N≤n) :
    BilateralGauge I S a c N B R x where
…
```
Mentions: OAI.SmoothObstruction.ManifoldCoordinates.BilateralGauge

theorem OAI.SmoothObstruction.ManifoldCoordinates.actual_tube_comparison line 206

Source documentation

Strengthen actual short comparison by a prescribed uniform atlas tube. Membership of the nearby orbit at ALL intermediate times is a conclusion.

theorem actual_tube_comparison (hclosed : IsClosed (range I))
    (S : Diffeomorph I I M M ∞) (a : ι → M) (K : ι → Set M)
    (hK : ∀ i,IsCompact (K i)) (hKU : ∀ i,K i⊆(chartAt H (a i)).source)
    {τ : ℝ} (hτ : 0<τ) :
    ∃ r C : ℝ,0<r ∧ 1≤C ∧ ∀ (c : ℕ → ι) (x y : M) (N : ℕ),
      (∀ t≤N,S^[t] x∈K (c t)) → I.IsInteriorPoint x → I.IsInteriorPoint y →
      y∈(chartAt H (a (c 0))).source →
      C ^ N*‖(extChartAt I (a (c 0))) y-(extChartAt I (a (c 0))) x‖≤r →
      (∀ t≤N,S^[t] y∈(chartAt H (a (c t))).source ∧
        S^[t] y∈cthickening τ (K (c t))) ∧
      ‖fderiv ℝ (ShortDerivative.iterate (fun t => localMap I S (a (c t)) (a (c (t+1)))) N)
          ((extChartAt I (a (c 0))) y)-
…

Mentions: OAI.SmoothObstruction.ShortDerivative.iterate, OAI.SmoothObstruction.ManifoldCoordinates.localMap

theorem OAI.SmoothObstruction.ManifoldCoordinates.uniform_genuine_bin_gauges line 234

Source documentation

Genuine good-path gauges can be attached simultaneously to the two reference chart codes of a nearby orbit. No continued chart membership, frame continuity, or derivative comparison is an extra hypothesis.

theorem uniform_genuine_bin_gauges (hclosed : IsClosed (range I))
    (S : Diffeomorph I I M M ∞) (a : ι → M) (K : ι → Set M)
    (hK : ∀ i,IsCompact (K i)) (hKU : ∀ i,K i⊆(chartAt H (a i)).source) :
    ∃ rF CF rB CB D : ℝ,0<rF ∧ 1≤CF ∧ 0<rB ∧ 1≤CB ∧ 1≤D ∧
      ∀ (c : M → ι) (J : Type*) (x : J → M) (e : J) (cF cB : ℕ → ι)
        (n N : ℕ) (B R h : ℝ) (A : ∀ i,BilateralGauge I S a c n B R (x i)),
        (∀ y,y∈K (c y)) → N≤n → cB 0=cF 0 →
        (∀ t≤N,S^[t] (x e)∈K (cF t)) →
        (∀ t≤N,S.symm^[t] (x e)∈K (cB t)) →
        (∀ i,I.IsInteriorPoint (x i)) →
        (∀ i,x i∈(chartAt H (a (cF 0))).source) →
        (∀ i,‖(extChartAt I (a (cF 0))) (x i)-(extChartAt I (a (cF 0))) (x e)‖≤h) →
…

Mentions: OAI.SmoothObstruction.ManifoldCoordinates.BilateralGauge