OAI/Dynamics/SmoothObstruction/Charts.lean

GitHub source file

48 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SmoothObstruction.GoodStationary.floor_burden_eq line 18
2. lemma OAI.SmoothObstruction.GoodStationary.burden_ge_one line 26
3. lemma OAI.SmoothObstruction.GoodStationary.eventual_log_le_burden line 33
4. lemma OAI.SmoothObstruction.OrbitCocycle.code_iterate line 66
5. lemma OAI.SmoothObstruction.OrbitCocycle.matrix_at_actual line 74
6. theorem OAI.SmoothObstruction.OrbitCocycle.actual_good_gauges line 89

   Source documentation

   Quantitative finite gauges for the genuine bounded measurable cocycle. The compact stationary QR lift, square-summable burdens, compact good sets, and their original base masses are all constructed. On every good witness the operator identity uses the ACTUAL original cocycle, not a free triangular surrogate or a separately assumed frame process.

   theorem actual_good_gauges (S : X ≃ₜ X) (A : X → CompactMatrix.Alphabet d K)
       (hA : Measurable A) (μ : ProbabilityMeasure X)
       (hS : MeasurePreserving S (μ : Measure X) (μ : Measure X))
       {η : ℝ} (hη : 0<η) :
       ∃ (ν : ProbabilityMeasure (Path (X:=X) (d:=d) (K:=K) × QR.Frame d))
   …

   Mentions: OAI.SmoothObstruction.CompactMatrix.Alphabet, OAI.SmoothObstruction.OrbitCocycle.Path, OAI.SmoothObstruction.QR.Frame

7. theorem OAI.SmoothObstruction.ManifoldCoordinates.manifold_good_gauges_discrete line 141

   Source documentation

   Actual compact-manifold derivative gauges, constructed uniformly from smoothness, compactness and the invariant original probability. The finite chart selector, stationary frame lift, summable error sequence, large compact middle-point sets and two-sided invertible gauges are all produced. This is the linear input to the nonlinear switching proof, not that proof.

   theorem manifold_good_gauges_discrete (S : Diffeomorph I I M M ∞)
       (μ : ProbabilityMeasure M) (hS : MeasurePreserving S (μ : Measure M) (μ : Measure M))
       {η : ℝ} (hη : 0<η) :
       ∃ (ι : Type u) (_ : Fintype ι) (_ : MeasurableSpace ι) (_ : MeasurableSingletonClass ι)
         (a : ι → M) (K : ι → Set M) (c : M → ι) (D : ℝ)
         (A : M → CompactMatrix.Alphabet d D),
         (∀ i,IsCompact (K i)) ∧ (∀ i,K i⊆(chartAt H (a i)).source) ∧
         Measurable c ∧ (∀ x,x∈K (c x)) ∧ 0<D ∧ Measurable A ∧
         (∀ x,(A x).val=coord I S (a (c x)) (a (c (S x))) x) ∧
         ∃ (ν : ProbabilityMeasure (OrbitCocycle.Path (X:=M) (d:=d) (K:=D) × QR.Frame d))
   …

   Mentions: OAI.SmoothObstruction.CompactMatrix.Alphabet, OAI.SmoothObstruction.ManifoldCoordinates.coord, OAI.SmoothObstruction.OrbitCocycle.Path, OAI.SmoothObstruction.QR.Frame

8. lemma OAI.SmoothObstruction.ManifoldCoordinates.coord_inverse_step line 191

   Source documentation

   Actual reverse derivative in a pair of fixed charts, also at boundary points.

   lemma coord_inverse_step (S : Diffeomorph I I M M ∞) (a b x : M)
       (hx : x∈(chartAt H a).source) (hy : S x∈(chartAt H b).source) :
       coord I S.symm b a (S x)*coord I S a b x=1 := by
   …

   Mentions: OAI.SmoothObstruction.ManifoldCoordinates.coord

9. lemma OAI.SmoothObstruction.OrbitCocycle.homeomorph_pow_iterate line 227
10. lemma OAI.SmoothObstruction.OrbitCocycle.actual_middle line 234
11. lemma OAI.SmoothObstruction.OrbitCocycle.backward_center line 241
12. lemma OAI.SmoothObstruction.ManifoldCoordinates.reverse_gauge_step line 258

    Source documentation

    Reversing a genuine finite derivative gauge is exact; the backward rates are the negatives of the forward rates, and the same center basis is used. No second derivative of a long iterate is introduced.

    lemma reverse_gauge_step (S : Diffeomorph I I M M ∞)
        (c : ℕ → M) (x : ℕ → M) (P : ℕ → Matrix (Fin d) (Fin d) ℝ)
        (lam : Fin d → ℝ) (j : ℕ)
        (hx : S (x j)=x (j+1))
        (hsrc : x j∈(chartAt H (c j)).source)
        (htar : x (j+1)∈(chartAt H (c (j+1))).source)
        (hstep : (Matrix.toEuclideanCLM (n:=Fin d) (𝕜:=ℝ)).symm
    …

13. structure OAI.SmoothObstruction.ManifoldCoordinates.BilateralGauge line 303

    Source documentation

    A finite two-sided gauge of the ACTUAL derivative, based at time zero. This carries no splitting, threshold, switch, Jacobian or measure conclusion.

    structure BilateralGauge (S : Diffeomorph I I M M ∞) {ι : Type*}
        (a : ι → M) (c : M → ι) (n : ℕ) (B R : ℝ) (x : M) where
    …

14. lemma OAI.SmoothObstruction.ManifoldCoordinates.center_from_gauge line 324
15. theorem OAI.SmoothObstruction.ManifoldCoordinates.good_bilateral_gauges line 369

    Source documentation

    The compact, large original-measure good base sets now carry actual forward AND backward gauges about their own time-zero point. The QR path witness is eliminated existentially; no measurable frame selection is used.

    theorem good_bilateral_gauges [CompactSpace M] [MeasurableSpace M] [BorelSpace M]
        (S : Diffeomorph I I M M ∞) (μ : ProbabilityMeasure M)
        (hS : MeasurePreserving S (μ : Measure M) (μ : Measure M)) {η : ℝ} (hη : 0<η) :
        ∃ (ι : Type u) (_ : Fintype ι) (_ : MeasurableSpace ι) (_ : MeasurableSingletonClass ι)
          (a : ι → M) (K : ι → Set M) (c : M → ι),
          (∀ i,IsCompact (K i)) ∧ (∀ i,K i⊆(chartAt H (a i)).source) ∧
          Measurable c ∧ (∀ x,x∈K (c x)) ∧
          ∃ (b : ℕ → ℝ) (R C : ℝ) (G : ℕ → Set M),
            0≤R ∧ 0≤C ∧ (∀ k,0<b k) ∧ (∀ k,GoodStationary.floorAt k≤b k) ∧
            Summable (fun k => (b k)^2) ∧
            (∀ k,IsCompact (G k) ∧ 1-η/100≤(μ : Measure M).real (G k)) ∧
            ∀ᶠ k in atTop,∀ x∈G k,
    …

    Mentions: OAI.SmoothObstruction.GoodStationary.floorAt

16. def OAI.SmoothObstruction.ManifoldCoordinates.chartChange line 414
17. lemma OAI.SmoothObstruction.ManifoldCoordinates.chartChange_coe line 419
18. theorem OAI.SmoothObstruction.ManifoldCoordinates.coord_chart_change line 430

    Source documentation

    Exact cocycle conjugation for independently fixed carried charts. This is a relation between actual manifold derivatives, not a formal similarity hypothesis supplied in place of them.

    theorem coord_chart_change (S : Diffeomorph I I M M ∞) (a b a' b' x : M)
        (hx : x∈domain I S a b) (hx' : x∈domain I S a' b') :
        coord I S a' b' x=
          (chartChange I b b' (S x) hx.2 hx'.2 : E (d:=d) →L[ℝ] E (d:=d)) *
    …

    Mentions: OAI.SmoothObstruction.ManifoldCoordinates.domain, OAI.SmoothObstruction.ManifoldCoordinates.coord, OAI.SmoothObstruction.ManifoldCoordinates.chartChange, OAI.SmoothObstruction.ManifoldCoordinates.E

19. lemma OAI.SmoothObstruction.ManifoldCoordinates.chartChange_inverse line 442
20. lemma OAI.SmoothObstruction.CarriedCharts.finite_positive_lower line 454
21. theorem OAI.SmoothObstruction.CarriedCharts.uniform_domains line 473

    Source documentation

    The same radius works for every chart pair actually visited by S. Inputs need not stay in the selected compact patches: the neighboring orbit only needs to stay inside this fixed radius of the old orbit.

    theorem uniform_domains (S : M → M) (hS : Continuous S)
        (K U : ι → Set M) (hK : ∀ i,IsCompact (K i)) (hU : ∀ i,IsOpen (U i))
        (hKU : ∀ i,K i⊆U i) :
        ∃ r : ℝ,0 < r ∧ ∀ i j x,x∈K i → S x∈K j →
          closedBall x r⊆U i∩S ⁻¹' U j := by
    …

22. theorem OAI.SmoothObstruction.CarriedCharts.uniform_bilateral_domains line 492

    Source documentation

    Uniform carried domains for both time directions. No orientability, connectedness, or absence of a boundary was used in this construction.

    theorem uniform_bilateral_domains (S : M ≃ₜ M)
        (K U : ι → Set M) (hK : ∀ i,IsCompact (K i)) (hU : ∀ i,IsOpen (U i))
        (hKU : ∀ i,K i⊆U i) :
        ∃ r : ℝ,0 < r ∧
          (∀ i j x,x∈K i → S x∈K j → closedBall x r⊆U i∩S ⁻¹' U j) ∧
          (∀ i j x,x∈K i → S.symm x∈K j → closedBall x r⊆U i∩S.symm ⁻¹' U j) := by
    …

23. theorem OAI.SmoothObstruction.CarriedCharts.actual_chart_margins line 512

    Source documentation

    Application to the actual chart domains chosen by the finite-atlas producer. The selector may be discontinuous: no continuity is asserted or needed for the selected cocycle. Comparisons use its fixed CARRIED chart.

    theorem actual_chart_margins (S : M ≃ₜ M) (a : ι → M) (K : ι → Set M)
        (hK : ∀ i,IsCompact (K i)) (hKU : ∀ i,K i⊆(chartAt H (a i)).source)
        (c : M → ι) (hc : ∀ x,x∈K (c x)) :
        ∃ r : ℝ,0 < r ∧ ∀ x y,dist y x ≤ r →
          y∈(chartAt H (a (c x))).source ∧
          S y∈(chartAt H (a (c (S x)))).source ∧
          S.symm y∈(chartAt H (a (c (S.symm x)))).source := by
    …

24. theorem OAI.SmoothObstruction.ManifoldCoordinates.uniform_chart_changes line 540

    Source documentation

    Uniform bounds on actual chart conversions throughout fixed enlarged compact patches. Thus gauges may be transported from a discontinuously selected atlas to a carried atlas without adding point/scale-dependent constants. These are derivatives of the identity on M, also at its boundary.

    theorem uniform_chart_changes (a : ι → M) (K : ι → Set M)
        (hK : ∀ i,IsCompact (K i)) (hKU : ∀ i,K i⊆(chartAt H (a i)).source) :
        ∃ r D : ℝ,0 < r ∧ 1 ≤ D ∧ ∀ i j x,
          x∈cthickening r (K i) → x∈cthickening r (K j) →
          x∈(chartAt H (a i)).source ∧ x∈(chartAt H (a j)).source ∧
          ‖coord I (Diffeomorph.refl I M ∞) (a i) (a j) x‖ ≤ D ∧
          ‖coord I (Diffeomorph.refl I M ∞) (a j) (a i) x‖ ≤ D := by
    …

    Mentions: OAI.SmoothObstruction.ManifoldCoordinates.coord

25. theorem OAI.SmoothObstruction.ManifoldCoordinates.uniform_carried_gauge line 586

    Source documentation

    Uniformly transport genuine finite gauges between any selected and carried chart sequences lying in the enlarged finite atlas. All norm losses are the same fixed D; the actual manifold-derivative conjugation identity is proved above, and is not an extra cocycle assumption.

    theorem uniform_carried_gauge (a : ι → M) (K : ι → Set M)
        (hK : ∀ i,IsCompact (K i)) (hKU : ∀ i,K i⊆(chartAt H (a i)).source) :
        ∃ r D : ℝ,0 < r ∧ 1 ≤ D ∧
          ∀ (S : Diffeomorph I I M M ∞) (x : ℕ → M) (c e : ℕ → ι)
            (P Q : ℕ → Matrix (Fin d) (Fin d) ℝ) (lam : Fin d → ℝ) (N : ℕ) (B : ℝ),
            (∀ t≤N,x t∈cthickening r (K (c t))) →
            (∀ t≤N,x t∈cthickening r (K (e t))) →
            (∀ t<N,S (x t)=x (t+1)) →
            (∀ t,P t*Q t=1 ∧ Q t*P t=1) →
            (∀ t≤N,‖P t‖≤Real.exp B ∧ ‖Q t‖≤Real.exp B) →
            (∀ t<N,(Matrix.toEuclideanCLM (n:=Fin d) (𝕜:=ℝ)).symm
    …

26. theorem OAI.SmoothObstruction.ManifoldCoordinates.uniform_carried_gauge_explicit line 681

    Source documentation

    Uniformly transport genuine finite gauges between any selected and carried chart sequences lying in the enlarged finite atlas. All norm losses are the same fixed D; the actual manifold-derivative conjugation identity is proved above, and is not an extra cocycle assumption.

    theorem uniform_carried_gauge_explicit (a : ι → M) (K : ι → Set M)
        (hK : ∀ i,IsCompact (K i)) (hKU : ∀ i,K i⊆(chartAt H (a i)).source) :
        ∃ r D : ℝ,0 < r ∧ 1 ≤ D ∧
          ∀ (S : Diffeomorph I I M M ∞) (x : ℕ → M) (c e : ℕ → ι)
            (P Q : ℕ → Matrix (Fin d) (Fin d) ℝ) (lam : Fin d → ℝ) (N : ℕ) (B : ℝ),
            (∀ t≤N,x t∈cthickening r (K (c t))) →
            (∀ t≤N,x t∈cthickening r (K (e t))) →
            (∀ t<N,S (x t)=x (t+1)) →
            (∀ t,P t*Q t=1 ∧ Q t*P t=1) →
            (∀ t≤N,‖P t‖≤Real.exp B ∧ ‖Q t‖≤Real.exp B) →
            (∀ t<N,(Matrix.toEuclideanCLM (n:=Fin d) (𝕜:=ℝ)).symm
    …

27. structure OAI.SmoothObstruction.ShortBin.Gauge line 770
28. def OAI.SmoothObstruction.ShortBin.Gauge.ofFinite line 787

    Source documentation

    Extend only beyond the finite window by its terminal value. This extension is algebraically invertible at every index and never affects an actual derivative equation within the window.

    noncomputable def Gauge.ofFinite {d n : ℕ} {B : ℝ}
        (P Q : ℕ → Matrix (Fin d) (Fin d) ℝ) (lam : Fin d → ℝ)
        (hi : ∀ t≤n,P t*Q t=1 ∧ Q t*P t=1)
        (hb : ∀ t≤n,‖P t‖≤Real.exp B ∧ ‖Q t‖≤Real.exp B) : Gauge d n B where
    …

    Mentions: OAI.SmoothObstruction.ShortBin.Gauge

29. theorem OAI.SmoothObstruction.ManifoldCoordinates.uniform_carried_bilateral line 812

    Source documentation

    Attach the actual stationary gauges to any two fixed carried chart codes. Forward and backward gauges have exactly the SAME center bases, not merely nearby center subspaces. A single uniform additive burden pays all chart changes, independently of the number of iterates.

    theorem uniform_carried_bilateral (a : ι → M) (K : ι → Set M)
        (hK : ∀ i,IsCompact (K i)) (hKU : ∀ i,K i⊆(chartAt H (a i)).source) :
        ∃ r D : ℝ,0<r ∧ 1≤D ∧
          ∀ (S : Diffeomorph I I M M ∞) (c : M → ι) (x : M) (n : ℕ) (B R : ℝ)
            (A : BilateralGauge I S a c n B R x) (eF eB : ℕ → ι),
            (∀ y,y∈K (c y)) → eB 0=eF 0 →
            (∀ t≤n,S^[t] x∈cthickening r (K (eF t))) →
            (∀ t≤n,S.symm^[t] x∈cthickening r (K (eB t))) →
            ∃ F Z : ShortBin.Gauge d n (B+Real.log D),
              (∀ i,F.lam i=A.lam i) ∧ (∀ i,Z.lam i= -A.lam i) ∧
              Z.U 0=F.U 0 ∧ Z.V 0=F.V 0 ∧
              (∀ t<n,(Matrix.toEuclideanCLM (n:=Fin d) (𝕜:=ℝ)).symm
    …

    Mentions: OAI.SmoothObstruction.ManifoldCoordinates.BilateralGauge, OAI.SmoothObstruction.ShortBin.Gauge

30. theorem OAI.SmoothObstruction.ManifoldCoordinates.uniform_carried_bilateral_explicit line 864
31. def OAI.SmoothObstruction.ManifoldCoordinates.localMap line 937
32. theorem OAI.SmoothObstruction.ManifoldCoordinates.coord_eq_fderivWithin line 943

    Source documentation

    The actual derivative cocycle is the derivative of the actual local coordinate map. Charts may be independently selected at each endpoint; the formula is valid on half-space models without changing derivatives.

    theorem coord_eq_fderivWithin (S : Diffeomorph I I M M ∞) (a b x : M)
        (hx : x∈domain I S a b) :
        fderivWithin ℝ (localMap I S a b) (range I) ((extChartAt I a) x)=coord I S a b x := by
    …

    Mentions: OAI.SmoothObstruction.ManifoldCoordinates.domain, OAI.SmoothObstruction.ManifoldCoordinates.localMap, OAI.SmoothObstruction.ManifoldCoordinates.coord

33. theorem OAI.SmoothObstruction.ManifoldCoordinates.hasFDerivAt_localMap line 971

    Source documentation

    In an interior orbit tube this is an ordinary derivative, exactly the input of the finite-array nonlinear construction.

    theorem hasFDerivAt_localMap (S : Diffeomorph I I M M ∞) (a b x : M)
        (hx : x∈domain I S a b)
        (hint : (extChartAt I a) x∈interior (range I)) :
        HasFDerivAt (localMap I S a b) (coord I S a b x) ((extChartAt I a) x) := by
    …

    Mentions: OAI.SmoothObstruction.ManifoldCoordinates.domain, OAI.SmoothObstruction.ManifoldCoordinates.localMap, OAI.SmoothObstruction.ManifoldCoordinates.coord

34. theorem OAI.SmoothObstruction.ManifoldCoordinates.contDiffAt_localMap line 996

    Source documentation

    Actual coordinate expressions are genuinely smooth in every retained interior tube. For a boundary model no smooth extension is assumed here: the statement uses the interior of the original model range.

    theorem contDiffAt_localMap (S : Diffeomorph I I M M ∞) (a b x : M)
        (hx : x∈domain I S a b)
        (hint : (extChartAt I a) x∈interior (range I)) :
        ContDiffAt ℝ ∞ (localMap I S a b) ((extChartAt I a) x) := by
    …

    Mentions: OAI.SmoothObstruction.ManifoldCoordinates.domain, OAI.SmoothObstruction.ManifoldCoordinates.localMap

35. theorem OAI.SmoothObstruction.ManifoldCoordinates.projected_localMap line 1013

    Source documentation

    Fixed target linear projections preserve the actual local regularity and have the expected derivative: this builds the endpoint maps used by the inverse-function branch, not a new abstract replacement for DS^n.

    theorem projected_localMap {F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F]
        (P : E (d:=d) →L[ℝ] F) (S : Diffeomorph I I M M ∞) (a b x : M)
    …

    Mentions: OAI.SmoothObstruction.ManifoldCoordinates.E

36. theorem OAI.SmoothObstruction.CarriedCharts.uniform_c2_boundary line 1033

    Source documentation

    Uniform C2 bounds up to a closed model boundary, WITHOUT an extension assumption. Ordinary derivatives are taken only in the original interior; the bound is independent of distance to the boundary.

    theorem uniform_c2_boundary (f : ι → E → F) (K U : ι → Set E) (H : Set E)
        (hK : ∀ i,IsCompact (K i)) (hU : ∀ i,IsOpen (U i)) (hH : IsClosed H)
        (hKU : ∀ i,K i⊆U i) (huniq : ∀ i,UniqueDiffOn ℝ (U i∩H))
        (hf : ∀ i,ContDiffOn ℝ ∞ (f i) (U i∩H)) :
        ∃ r C : ℝ,0 < r ∧ 1 ≤ C ∧ ∀ i x,x∈K i →
          closedBall x r⊆U i ∧ ∀ y∈closedBall x r,y∈interior H →
            ContDiffAt ℝ ∞ (f i) y ∧
            ‖fderiv ℝ (f i) y‖ ≤ C ∧ ‖fderiv ℝ (fderiv ℝ (f i)) y‖ ≤ C := by
    …

37. def OAI.SmoothObstruction.ManifoldCoordinates.domainU line 1101

    Source documentation

    An ambient open carrier of the exact local expression's relative coordinate domain. It is NOT a smooth extension of the expression.

    def domainU (S : Diffeomorph I I M M ∞) (a b : M) : Set (E (d:=d)) :=
    …

    Mentions: OAI.SmoothObstruction.ManifoldCoordinates.E

38. lemma OAI.SmoothObstruction.ManifoldCoordinates.isOpen_domainU line 1105
39. lemma OAI.SmoothObstruction.ManifoldCoordinates.map_mem_domainU line 1110
40. theorem OAI.SmoothObstruction.ManifoldCoordinates.contDiffOn_localMap line 1121
41. theorem OAI.SmoothObstruction.ManifoldCoordinates.actual_uniform_c2 line 1141

    Source documentation

    Genuine uniform first and second derivative bounds for all actually used local chart pairs. Valid for the closed half-space model, uniformly as the reference point approaches the boundary. No extension theorem or long-iterate C2 bound has been assumed.

    theorem actual_uniform_c2 [T2Space M] {ι : Type*} [Fintype ι]
        (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) :
        ∃ r C : ℝ,0 < r ∧ 1 ≤ C ∧ ∀ i j x,x∈K i → S x∈K j →
          closedBall ((extChartAt I (a i)) x) r⊆domainU I S (a i) (a j) ∧
          ∀ y∈closedBall ((extChartAt I (a i)) x) r,y∈interior (range I) →
            ContDiffAt ℝ ∞ (localMap I S (a i) (a j)) y ∧
            ‖fderiv ℝ (localMap I S (a i) (a j)) y‖ ≤ C ∧
            ‖fderiv ℝ (fderiv ℝ (localMap I S (a i) (a j))) y‖ ≤ C := by
    …

    Mentions: OAI.SmoothObstruction.ManifoldCoordinates.domainU, OAI.SmoothObstruction.ManifoldCoordinates.localMap

42. lemma OAI.SmoothObstruction.ManifoldCoordinates.interior_coord line 1175
43. theorem OAI.SmoothObstruction.ManifoldCoordinates.localMap_maps_interior line 1185

    Source documentation

    Carried local expressions preserve the original model interior on exactly their actual relative domains, even for manifolds with boundary.

    theorem localMap_maps_interior (S : Diffeomorph I I M M ∞) (a b : M) :
        MapsTo (localMap I S a b) (domainU I S a b∩interior (range I))
          (interior (range I)) := by
    …

    Mentions: OAI.SmoothObstruction.ManifoldCoordinates.localMap, OAI.SmoothObstruction.ManifoldCoordinates.domainU

44. lemma OAI.SmoothObstruction.ManifoldCoordinates.localMap_coordinates line 1203
45. lemma OAI.SmoothObstruction.StandardModels.real_closed line 1213
46. lemma OAI.SmoothObstruction.StandardModels.real_convex line 1214
47. lemma OAI.SmoothObstruction.StandardModels.half_closed line 1215
48. lemma OAI.SmoothObstruction.StandardModels.half_convex line 1218