ProductCoordinates.lean`

21 declarations, 0 contain sorry, 0 declared as axioms

def OAI.SmoothObstruction.ProductBasis.blockMap line 19
lemma OAI.SmoothObstruction.ProductBasis.blockMap_apply line 26
lemma OAI.SmoothObstruction.ProductBasis.sum_norm_sq line 33
lemma OAI.SmoothObstruction.ProductBasis.norm_blockMap line 41
Source documentation
The source's basis consists of orthonormal columns within each summand. Its forward norm is uniformly bounded even when the angle is small.
```
lemma norm_blockMap (U V : Submodule ℝ E) (h : IsCompl U V)
    (bU : OrthonormalBasis ι ℝ U) (bV : OrthonormalBasis κ ℝ V) :
    ‖(blockMap U V h bU bV).toContinuousLinearMap‖≤Real.sqrt 2 := by
…
```
Mentions: OAI.SmoothObstruction.ProductBasis.blockMap
lemma OAI.SmoothObstruction.ProductBasis.blockMap_symm_components line 55

lemma OAI.SmoothObstruction.ProductBasis.norm_blockMap_symm line 66

Source documentation

Only the inverse pays the complementary-projection condition number.

lemma norm_blockMap_symm (U V : Submodule ℝ E) (h : IsCompl U V)
    (bU : OrthonormalBasis ι ℝ U) (bV : OrthonormalBasis κ ℝ V)
    {H : ℝ} (hH : 0≤H)
    (hU : ∀ x,‖U.projectionOnto V h x‖≤H*‖x‖)
    (hV : ∀ x,‖V.projectionOnto U h.symm x‖≤H*‖x‖) :
    ‖(blockMap U V h bU bV).symm.toContinuousLinearMap‖≤Real.sqrt 2*H := by
…

Mentions: OAI.SmoothObstruction.ProductBasis.blockMap

theorem OAI.SmoothObstruction.ProductBasis.exists_coordinates line 93

Source documentation

A fixed ambient coordinate alphabet for the orthonormal-within-group product basis. The rank may vary from bin to bin without being charged as an orbit code. Even rank-zero groups retain the exact mixing property.

theorem exists_coordinates (U V : Submodule ℝ E) (h : IsCompl U V)
    {H : ℝ} (hH : 0≤H)
    (hU : ∀ x,‖U.projectionOnto V h x‖≤H*‖x‖)
    (hV : ∀ x,‖V.projectionOnto U h.symm x‖≤H*‖x‖) :
    ∃ A : E ≃L[ℝ] E,
      ‖A.toContinuousLinearMap‖≤Real.sqrt 2 ∧
      ‖A.symm.toContinuousLinearMap‖≤Real.sqrt 2*H ∧
      ∀ x y : E,∀ i : Fin d,
        (A.symm (x+(U.projectionOnto V h (y-x):E))) i=(A.symm x) i ∨
        (A.symm (x+(U.projectionOnto V h (y-x):E))) i=(A.symm y) i := by
…

lemma OAI.SmoothObstruction.FiniteGreen.Splitting.ranges_isCompl line 161
lemma OAI.SmoothObstruction.FiniteGreen.Splitting.range_projection_slow line 179
lemma OAI.SmoothObstruction.FiniteGreen.Splitting.range_projection_fast line 190

theorem OAI.SmoothObstruction.ProductBasis.splitting_coordinates line 209

Source documentation

The authentic complementary splitting produces its own uniform product coordinate map, with the exact slow/fast ideal mix and no rank assumptions.

theorem splitting_coordinates {T : Evolution E} (B : Splitting T) (t : ℕ)
    {H : ℝ} (hH : 0≤H) (hs : ‖B.slow t‖≤H) (hf : ‖B.fast t‖≤H) :
    ∃ A : E ≃L[ℝ] E,
      ‖A.toContinuousLinearMap‖≤Real.sqrt 2 ∧
      ‖A.symm.toContinuousLinearMap‖≤Real.sqrt 2*H ∧
      ∀ x y : E,∀ i : Fin d,
        (A.symm (x+B.slow t (y-x))) i=(A.symm x) i ∨
        (A.symm (x+B.slow t (y-x))) i=(A.symm y) i := by
…

theorem OAI.SmoothObstruction.ShortBin.Gauge.product_coordinates line 236

Source documentation

Authentic gauges give product coordinates for the original coarse bin. The coordinate groups are allowed to have either rank zero or full rank.

theorem Gauge.product_coordinates (A : Gauge d n K) (S : Finset (Fin d)) :
    ∃ L : EuclideanSpace ℝ (Fin d) ≃L[ℝ] EuclideanSpace ℝ (Fin d),
      ‖L.toContinuousLinearMap‖≤Real.sqrt 2 ∧
      ‖L.symm.toContinuousLinearMap‖≤Real.sqrt 2*Real.exp (2*K) ∧
      ∀ x y : EuclideanSpace ℝ (Fin d),∀ i : Fin d,
        (L.symm (x+(A.splitting S).slow 0 (y-x))) i=(L.symm x) i ∨
        (L.symm (x+(A.splitting S).slow 0 (y-x))) i=(L.symm y) i := by
…

Mentions: OAI.SmoothObstruction.ShortBin.Gauge

theorem OAI.SmoothObstruction.FiniteBins.product_coordinates line 257

Source documentation

Extend the genuinely selected bin coordinates to unused bins. The arbitrary identity coordinates are never used by a retained input.

theorem product_coordinates (P : X → C) (G : Set X) (hK : 0≤K)
    (A : Active P G → ShortBin.Gauge d n K) (S : Active P G → Finset (Fin d)) :
    ∃ L : C → E ≃L[ℝ] E,
      (∀ c,‖(L c).toContinuousLinearMap‖≤Real.sqrt 2) ∧
      (∀ c,‖(L c).symm.toContinuousLinearMap‖≤Real.sqrt 2*Real.exp (2*K)) ∧
      ∀ c : Active P G,∀ x y : E,∀ i : Fin d,
        ((L c.val).symm (x+((A c).splitting (S c)).slow 0 (y-x))) i=
          ((L c.val).symm x) i ∨
        ((L c.val).symm (x+((A c).splitting (S c)).slow 0 (y-x))) i=
          ((L c.val).symm y) i := by
…

Mentions: OAI.SmoothObstruction.FiniteBins.Active, OAI.SmoothObstruction.ShortBin.Gauge

theorem OAI.SmoothObstruction.AtlasCores.finite_cores line 297

Source documentation

Compact cores of a finite measurable cover cost arbitrarily little of the original measure. No relative distribution inside a selector fiber is used.

theorem finite_cores (μ : Measure M) [IsFiniteMeasure μ]
    [Measure.InnerRegularCompactLTTop μ] (A : ι → Set M)
    (hA : ∀ i,MeasurableSet (A i)) (hcover : ∀ x,∃ i,x∈A i)
    (ε : ℝ≥0) (hε : 0<ε) :
    ∃ K : ι → Set M,(∀ i,K i⊆A i) ∧ (∀ i,IsCompact (K i)) ∧
      μ (⋃ i,K i)ᶜ≤ε := by
…

lemma OAI.SmoothObstruction.AtlasCores.finite_positive_min line 327
Source documentation
Positive finitely many scales have a positive common lower bound, including an empty index type. This avoids a nonempty-atlas convention.
```
lemma finite_positive_min (a : ι → ℝ) (ha : ∀ i,0<a i) :
    ∃ r : ℝ,0<r ∧ ∀ i,r≤a i := by
…
```

theorem OAI.SmoothObstruction.AtlasCores.separated_neighborhoods line 347

Source documentation

Disjoint compact chart cores admit one radius whose closed thickenings remain pairwise disjoint and inside the designated open charts.

theorem separated_neighborhoods (K U : ι → Set M)
    (hK : ∀ i,IsCompact (K i)) (hU : ∀ i,IsOpen (U i))
    (hKU : ∀ i,K i⊆U i) (hdisj : Pairwise (fun i j => Disjoint (K i) (K j))) :
    ∃ r : ℝ,0<r ∧ (∀ i,cthickening r (K i)⊆U i) ∧
      Pairwise (fun i j => Disjoint (cthickening r (K i)) (cthickening r (K j))) := by
…

theorem OAI.SmoothObstruction.AtlasCores.selector_cores line 372

Source documentation

The finite atlas selector now yields coherent disjoint retained chart cores and a single positive safety radius, with error measured in the ORIGINAL law.

theorem selector_cores [CompactSpace M] [MeasurableSpace ι]
    [MeasurableSingletonClass ι] (μ : Measure M) [IsFiniteMeasure μ]
    (c : M → ι) (hc : Measurable c) (U : ι → Set M)
    (hU : ∀ i,IsOpen (U i)) (hcU : ∀ x,x∈U (c x))
    (ε : ℝ≥0) (hε : 0<ε) :
    ∃ (K : ι → Set M) (r : ℝ),
      (∀ i,IsCompact (K i)) ∧ (∀ i,K i⊆c ⁻¹' {i}) ∧
      μ (⋃ i,K i)ᶜ≤ε ∧ 0<r ∧
      (∀ i,cthickening r (K i)⊆U i) ∧
      Pairwise (fun i j => Disjoint (cthickening r (K i)) (cthickening r (K j))) := by
…

theorem OAI.SmoothObstruction.AtlasCores.protected_selector line 406

Source documentation

Modify a chart selector only in disjoint protected neighborhoods. On the retained compact cores the new selector is genuinely locally constant, so nearby switched endpoints recover the same chart label.

theorem protected_selector (c : M → ι) (hc : Measurable c)
    (U V : ι → Set M) (hV : ∀ i,MeasurableSet (V i))
    (hVU : ∀ i,V i⊆U i) (hcU : ∀ x,x∈U (c x))
    (hd : Pairwise (fun i j => Disjoint (V i) (V j))) :
    ∃ q : M → ι,Measurable q ∧ (∀ x,x∈U (q x)) ∧
      (∀ i,∀ x∈V i,q x=i) ∧
      ∀ x,x∉⋃ i,V i → q x=c x := by
…

theorem OAI.SmoothObstruction.AtlasCores.stable_selector line 446

Source documentation

A coherent finite chart selector with an original-measure compact core and a uniform endpoint recoverability radius. Nothing is conditioned on a good Oseledets/frame set, and no intermediate chart codes refine the cells.

theorem stable_selector [CompactSpace M] (μ : Measure M) [IsFiniteMeasure μ]
    (c : M → ι) (hc : Measurable c) (U : ι → Set M)
    (hU : ∀ i,IsOpen (U i)) (hcU : ∀ x,x∈U (c x))
    (ε : ℝ≥0) (hε : 0<ε) :
    ∃ (q : M → ι) (K : ι → Set M) (r : ℝ),
      Measurable q ∧ (∀ x,x∈U (q x)) ∧
      (∀ i,IsCompact (K i)) ∧ μ (⋃ i,K i)ᶜ≤ε ∧ 0<r ∧
      (∀ i,∀ x∈K i,q x=i) ∧
      ∀ x∈⋃ i,K i,∀ y,dist y x≤r → q y=q x := by
…

theorem OAI.SmoothObstruction.AtlasCores.compact_stable_selector line 479

Source documentation

A stable selector can be chosen in any prescribed positive enlargement of the original compact patches. This preserves uniform chart bounds while charging only one fixed compact-core error in the original measure.

theorem compact_stable_selector (μ : Measure M) [IsFiniteMeasure μ]
    (c : M → ι) (hc : Measurable c) (K : ι → Set M)
    (hcK : ∀ x,x∈K (c x))
    {r : ℝ} (hr : 0<r) (ε : ℝ≥0) (hε : 0<ε) :
    ∃ (q : M → ι) (L : ι → Set M) (s : ℝ),
      Measurable q ∧ (∀ x,x∈cthickening r (K (q x))) ∧
      (∀ i,IsCompact (L i)) ∧ μ (⋃ i,L i)ᶜ≤ε ∧ 0<s ∧
      (∀ i,L i⊆K i) ∧ (∀ i,∀ x∈L i,q x=i) ∧
      ∀ x∈⋃ i,L i,∀ y,dist y x ≤ s → q y=q x := by
…

theorem OAI.SmoothObstruction.ManifoldCoordinates.good_stable_gauges line 520

Source documentation

Stable endpoint chart labels and actual good gauges are compatible. The chart-core error is fixed before the dyadic sequence is constructed; no orbit code or endpoint label is added to the future cell partition.

theorem good_stable_gauges (S : Diffeomorph I I M M ∞)
    (μ : ProbabilityMeasure M) (hS : MeasurePreserving S (μ : Measure M) (μ : Measure M))
    {η : ℝ} (hη : 0<η) (ε : ℝ≥0) (hε : 0<ε) :
    ∃ (ι : Type u) (_ : Fintype ι) (_ : MeasurableSpace ι) (_ : MeasurableSingletonClass ι)
      (a : ι → M) (K L : ι → Set M) (q : M → ι) (s : ℝ),
      (∀ i,IsCompact (K i)) ∧ (∀ i,K i⊆(chartAt H (a i)).source) ∧
      Measurable q ∧ (∀ x,x∈K (q x)) ∧
      (∀ i,IsCompact (L i)) ∧ (μ : Measure M) (⋃ i,L i)ᶜ≤ε ∧ 0<s ∧
      (∀ i,L i⊆K i) ∧ (∀ i,∀ x∈L i,q x=i) ∧
      (∀ x∈⋃ i,L i,∀ y,dist y x ≤ s → q y=q x) ∧
      ∃ (b : ℕ → ℝ) (R C : ℝ) (G : ℕ → Set M),
        0≤R ∧ 0≤C ∧ (∀ k,0<b k) ∧ (∀ k,GoodStationary.floorAt k≤b k) ∧
…

Mentions: OAI.SmoothObstruction.GoodStationary.floorAt