OAI/Dynamics/SmoothObstruction/BoundaryMatching.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SmoothObstruction.ShortBin.Gauge.evolution line 21
2. def OAI.SmoothObstruction.ShortBin.Gauge.splitting line 23
3. lemma OAI.SmoothObstruction.ShortBin.Gauge.space_eq_range line 26
4. theorem OAI.SmoothObstruction.ShortBin.gauge_matching line 33

   Source documentation

   The orthogonal common-bin space comparisons construct the middle matching equivalence for two genuine gauges with a possibly positive slow threshold. Complementarity is proved, not assumed for the moving spaces.

   theorem gauge_matching (A₀ A Z : Gauge d n K) (S₀ S T : Finset (Fin d))
       {ε : ℝ} (hε : 0≤ε) (hεhalf : ε≤1/2)
       (hdS : S₀.card=S.card) (hdT : S₀ᶜ.card=T.card)
       (hcS : ‖(A₀.space S₀).starProjection-(A.space S).starProjection‖≤ε)
       (hcT : ‖(A₀.space S₀ᶜ).starProjection-(Z.space T).starProjection‖≤ε)
       (hsmall : Real.exp (2*K)*(2*ε)≤1/2) :
       ∃ L : (((A.splitting S).slow 0).range×((Z.splitting T).slow 0).range) ≃L[ℝ]
         EuclideanSpace ℝ (Fin d),
         (∀ x,L x=(x.1:EuclideanSpace ℝ (Fin d))-(x.2:EuclideanSpace ℝ (Fin d))) ∧
         ‖L.symm.toContinuousLinearMap‖≤2*Real.exp (2*K) := by
   …

   Mentions: OAI.SmoothObstruction.ShortBin.Gauge

5. theorem OAI.SmoothObstruction.ManifoldCoordinates.uniform_genuine_single_gauges line 75

   Source documentation

   A one-sided family of actual gauges can be carried to reference charts using only the short orbit interval. This is also applicable at a long-window endpoint, without demanding good data beyond that endpoint.

   theorem uniform_genuine_single_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) :
       ∃ r C₁ D : ℝ,0<r ∧ 1≤C₁ ∧ 1≤D ∧
         ∀ (c : M → ι) (J : Type*) (x : J → M) (e : J) (cR : ℕ → ι)
           (N : ℕ) (B h : ℝ) (A : J → ShortBin.Gauge d N B),
           (∀ y,y∈K (c y)) →
           (∀ i,∀ t<N,(Matrix.toEuclideanCLM (n:=Fin d) (𝕜:=ℝ)).symm
   …

   Mentions: OAI.SmoothObstruction.ShortBin.Gauge

6. def OAI.SmoothObstruction.ManifoldCoordinates.BilateralGauge.endpointBackward line 139

   Source documentation

   The past short segment of the true forward gauge, centered at its long endpoint. Rates are merely negated; the original starting threshold remains available, and no new stationary witness is chosen.

   noncomputable def BilateralGauge.endpointBackward (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) : ShortBin.Gauge d N B where
   …

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

7. lemma OAI.SmoothObstruction.ManifoldCoordinates.BilateralGauge.endpointBackward_step line 151
8. def OAI.SmoothObstruction.ManifoldCoordinates.BilateralGauge.symm line 180

   Source documentation

   Reverse the two-sided gauge without changing any coordinate basis.

   def BilateralGauge.symm (S : Diffeomorph I I M M ∞) (a : ι → M) (c : M → ι)
       {n : ℕ} {B R : ℝ} {x : M} (A : BilateralGauge I S a c n B R x) :
       BilateralGauge I S.symm a c n B R x where
   …

   Mentions: OAI.SmoothObstruction.ManifoldCoordinates.BilateralGauge

9. theorem OAI.SmoothObstruction.ManifoldCoordinates.uniform_endpoint_fast_comparison line 204

   Source documentation

   Quantitative endpoint comparison at a FIXED starting threshold, for all actual witnesses reaching one endpoint bin. Only the past short segment is used at the forward endpoint. The displayed basis identities attach the comparison to the actual long-window spaces.

   theorem uniform_endpoint_fast_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) :
       ∃ r C₁ D : ℝ,0<r ∧ 1≤C₁ ∧ 1≤D ∧
         ∀ (c : M → ι) (J : Type*) (x : J → M) (e : J) (cR : ℕ → ι)
           (n N : ℕ) (B R h γ g : ℝ) (T : J → Finset (Fin d))
           (A : ∀ i,BilateralGauge I S a c n B R (x i)),
           (∀ y,y∈K (c y)) → N≤n →
           (∀ t≤N,S.symm^[t] (S^[n] (x e))∈K (cR t)) →
           (∀ i,I.IsInteriorPoint (S^[n] (x i))) →
           (∀ i,S^[n] (x i)∈(chartAt H (a (cR 0))).source) →
           (∀ i,‖(extChartAt I (a (cR 0))) (S^[n] (x i))-
   …

   Mentions: OAI.SmoothObstruction.ManifoldCoordinates.BilateralGauge

10. def OAI.SmoothObstruction.FiniteGreen.Splitting.initialSpace line 271
11. lemma OAI.SmoothObstruction.FiniteGreen.Splitting.slow_initial line 272
12. lemma OAI.SmoothObstruction.FiniteGreen.Splitting.Terminal.trajectory_initial line 280
13. lemma OAI.SmoothObstruction.FiniteGreen.Splitting.Terminal.trajectory_zero line 288
14. def OAI.SmoothObstruction.FiniteGreen.Matching.correction line 301
15. lemma OAI.SmoothObstruction.FiniteGreen.Matching.correction_apply line 306
16. lemma OAI.SmoothObstruction.FiniteGreen.Matching.correction_norm line 310
17. theorem OAI.SmoothObstruction.FiniteGreen.Matching.solve line 331

    Source documentation

    The exact two half-orbit boundary problem. The only matching input is complementarity of the unperturbed initial spaces. The small graph terms are inverted by a proved Neumann construction, not by assuming invertibility.

    theorem solve (L : (B₁.initialSpace × B₂.initialSpace) ≃L[ℝ] E)
        (hL : ∀ x,L x=(x.1:E)-(x.2:E))
        (hsmall : ‖L.symm.toContinuousLinearMap.comp (correction C₁ C₂)‖ < 1)
        (f₁ f₂ : ℕ → E) (h₁ : H) (h₂ : G) (m : E) :
        ∃ v₁ v₂ : ℕ → E,
          (∀ t<n₁,v₁ (t+1)=A₁.map (t+1) t (v₁ t)+f₁ t) ∧
          (∀ t<n₂,v₂ (t+1)=A₂.map (t+1) t (v₂ t)+f₂ t) ∧
          C₁.P (v₁ n₁)=h₁ ∧ C₂.P (v₂ n₂)=h₂ ∧ v₁ 0-v₂ 0=m ∧
          ∀ w₁ w₂ : ℕ → E,
            (∀ t<n₁,w₁ (t+1)=A₁.map (t+1) t (w₁ t)+f₁ t) →
            (∀ t<n₂,w₂ (t+1)=A₂.map (t+1) t (w₂ t)+f₂ t) →
            C₁.P (w₁ n₁)=h₁ → C₂.P (w₂ n₂)=h₂ → w₁ 0-w₂ 0=m →
    …

    Mentions: OAI.SmoothObstruction.FiniteGreen.Matching.correction

18. lemma OAI.SmoothObstruction.FiniteGreen.Evolution.forward_bound line 395
19. lemma OAI.SmoothObstruction.FiniteGreen.Evolution.backward_bound line 422
20. lemma OAI.SmoothObstruction.FiniteGreen.Splitting.Terminal.trajectory_bound line 455

    Source documentation

    A uniform half-orbit estimate. A polynomial factor in n is harmless under the source's log(n+1)≤bn floor, but is explicitly retained here.

    lemma trajectory_bound (f : ℕ → E) (a : E) (h : H) {G F : ℝ}
        (hG : 1≤G) (hF : 0≤F) (ha : B.slow 0 a=a)
        (hs : ∀ s u,s≤u → u≤n → ‖(A.map u s).comp (B.slow s)‖ ≤ G)
        (hb : ∀ s u,s≤u → u≤n → ‖(A.map s u).comp (B.fast u)‖ ≤ G)
        (hJ : ‖C.J‖ ≤ G) (hP : ‖C.P‖ ≤ G)
        (hf : ∀ j<n,‖f j‖ ≤ F) (hh : ‖h‖ ≤ F) {t : ℕ} (ht : t≤n) :
        ‖C.trajectory f a h t‖ ≤ (G+G^4)*‖a‖+(2*G+G^4)*(n:ℝ)*F+G^2*F := by
    …

21. theorem OAI.SmoothObstruction.FiniteGreen.Matching.solution_bound line 496

    Source documentation

    A quantitative bound for every genuine two-half boundary solution. The explicit polynomial is retained; the source's logarithmic time floor later absorbs it into the subexponential factor.

    theorem solution_bound (L : (B₁.initialSpace × B₂.initialSpace) ≃L[ℝ] E)
        (hL : ∀ x,L x=(x.1:E)-(x.2:E)) {U K F : ℝ}
        (hU : 1≤U) (hK : ‖L.symm.toContinuousLinearMap‖≤K) (hF : 0≤F)
        (hsmall : ‖L.symm.toContinuousLinearMap.comp (correction C₁ C₂)‖≤1/2)
        (hs₁ : ∀ s u,s≤u → u≤n₁ → ‖(A₁.map u s).comp (B₁.slow s)‖≤U)
        (hb₁ : ∀ s u,s≤u → u≤n₁ → ‖(A₁.map s u).comp (B₁.fast u)‖≤U)
        (hs₂ : ∀ s u,s≤u → u≤n₂ → ‖(A₂.map u s).comp (B₂.slow s)‖≤U)
        (hb₂ : ∀ s u,s≤u → u≤n₂ → ‖(A₂.map s u).comp (B₂.fast u)‖≤U)
        (hJ₁ : ‖C₁.J‖≤U) (hP₁ : ‖C₁.P‖≤U)
        (hJ₂ : ‖C₂.J‖≤U) (hP₂ : ‖C₂.P‖≤U)
        (f₁ f₂ w₁ w₂ : ℕ → E) (h₁ : H) (h₂ : G) (m : E)
        (hf₁ : ∀ j<n₁,‖f₁ j‖≤F) (hf₂ : ∀ j<n₂,‖f₂ j‖≤F)
    …

    Mentions: OAI.SmoothObstruction.FiniteGreen.Matching.correction

22. abbrev OAI.SmoothObstruction.FiniteGreen.Matching.Paths line 596
23. abbrev OAI.SmoothObstruction.FiniteGreen.Matching.Data line 597
24. def OAI.SmoothObstruction.FiniteGreen.Matching.boundaryLinear line 602

    Source documentation

    The actual finite-array boundary operator consists of both recurrence residuals, the middle matching equation, and the two terminal projections.

    noncomputable def boundaryLinear : Paths E n₁ n₂ →ₗ[ℝ] Data E H G n₁ n₂ where
    …

    Mentions: OAI.SmoothObstruction.FiniteGreen.Matching.Paths, OAI.SmoothObstruction.FiniteGreen.Matching.Data

25. def OAI.SmoothObstruction.FiniteGreen.Matching.boundary line 623
26. def OAI.SmoothObstruction.FiniteGreen.Matching.extend line 626
27. lemma OAI.SmoothObstruction.FiniteGreen.Matching.extend_apply line 630
28. theorem OAI.SmoothObstruction.FiniteGreen.Matching.boundary_bijective line 636

    Source documentation

    Finite-dimensional invertibility is a consequence of the Green formulas and the genuinely small terminal graph correction. No linear inverse is postulated.

    theorem boundary_bijective (L : (B₁.initialSpace × B₂.initialSpace) ≃L[ℝ] E)
        (hL : ∀ x,L x=(x.1:E)-(x.2:E))
        (hsmall : ‖L.symm.toContinuousLinearMap.comp (correction C₁ C₂)‖ < 1) :
        Function.Bijective (boundary C₁ C₂) := by
    …

    Mentions: OAI.SmoothObstruction.FiniteGreen.Matching.correction, OAI.SmoothObstruction.FiniteGreen.Matching.boundary

29. def OAI.SmoothObstruction.FiniteGreen.Matching.boundaryEquiv line 701
30. theorem OAI.SmoothObstruction.FiniteGreen.Matching.boundary_inverse_norm line 719