OAI/Dynamics/SmoothObstruction/GreenOperator.lean

GitHub source file

69 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.SmoothObstruction.FiniteGreen.Evolution line 21

   Source documentation

   Finite fundamental matrices, with the output time first.

   structure Evolution (E : Type*) [NormedAddCommGroup E] [NormedSpace ℝ E] where
   …

2. lemma OAI.SmoothObstruction.FiniteGreen.Evolution.self_apply line 29
3. lemma OAI.SmoothObstruction.FiniteGreen.Evolution.comp_apply line 30
4. def OAI.SmoothObstruction.FiniteGreen.Evolution.forward line 33
5. def OAI.SmoothObstruction.FiniteGreen.Evolution.backward line 36
6. lemma OAI.SmoothObstruction.FiniteGreen.Evolution.forward_zero line 39
7. lemma OAI.SmoothObstruction.FiniteGreen.Evolution.backward_end line 41
8. lemma OAI.SmoothObstruction.FiniteGreen.Evolution.forward_step line 44
9. lemma OAI.SmoothObstruction.FiniteGreen.Evolution.backward_step line 49
10. lemma OAI.SmoothObstruction.FiniteGreen.Evolution.forward_project line 56
11. lemma OAI.SmoothObstruction.FiniteGreen.Evolution.backward_project line 67
12. lemma OAI.SmoothObstruction.FiniteGreen.Evolution.recurrence_unique line 78
13. lemma OAI.SmoothObstruction.FiniteGreen.Evolution.backward_recurrence_unique line 87
14. structure OAI.SmoothObstruction.FiniteGreen.Splitting line 111

    Source documentation

    An invariant complementary splitting. Empty groups are permitted.

    structure Splitting (A : Evolution E) where
    …

    Mentions: OAI.SmoothObstruction.FiniteGreen.Evolution

15. lemma OAI.SmoothObstruction.FiniteGreen.Splitting.add_apply line 123
16. lemma OAI.SmoothObstruction.FiniteGreen.Splitting.slow_comm line 125
17. lemma OAI.SmoothObstruction.FiniteGreen.Splitting.fast_comm line 127
18. lemma OAI.SmoothObstruction.FiniteGreen.Splitting.slow_self line 129
19. lemma OAI.SmoothObstruction.FiniteGreen.Splitting.fast_self line 131
20. lemma OAI.SmoothObstruction.FiniteGreen.Splitting.slow_fast line 133
21. lemma OAI.SmoothObstruction.FiniteGreen.Splitting.fast_slow line 137
22. structure OAI.SmoothObstruction.FiniteGreen.Splitting.Terminal line 144

    Source documentation

    The endpoint projection has a specified bounded inverse on the actual fast space. It need not annihilate the slow space.

    structure Terminal (n : ℕ) where
    …

23. lemma OAI.SmoothObstruction.FiniteGreen.Splitting.Terminal.P_J line 153
24. lemma OAI.SmoothObstruction.FiniteGreen.Splitting.Terminal.J_P_fast line 154
25. lemma OAI.SmoothObstruction.FiniteGreen.Splitting.Terminal.fast_J line 156
26. def OAI.SmoothObstruction.FiniteGreen.Splitting.Terminal.terminalValue line 159
27. def OAI.SmoothObstruction.FiniteGreen.Splitting.Terminal.trajectory line 161
28. lemma OAI.SmoothObstruction.FiniteGreen.Splitting.Terminal.trajectory_step line 164
29. lemma OAI.SmoothObstruction.FiniteGreen.Splitting.Terminal.trajectory_terminal line 175
30. lemma OAI.SmoothObstruction.FiniteGreen.Splitting.Terminal.trajectory_slow_initial line 180
31. theorem OAI.SmoothObstruction.FiniteGreen.Splitting.Terminal.trajectory_unique line 189

    Source documentation

    Existence and uniqueness of the half-orbit boundary problem are proved from the actual finite recurrence. No implicit-function hypothesis.

    theorem trajectory_unique (f : ℕ → E) (a : E) (_ha : B.slow 0 a=a) (h : H)
        (v : ℕ → E) (hv : ∀ t<n,v (t+1)=A.map (t+1) t (v t)+f t)
        (h0 : B.slow 0 (v 0)=a) (hn : C.P (v n)=h) :
        ∀ t≤n,v t=C.trajectory f a h t := by
    …

32. def OAI.SmoothObstruction.FiniteGreen.Splitting.Terminal.kernel line 220

    Source documentation

    Endpoint correction on the slow initial data. Both decaying factors are kept explicitly, as required in (future-kernel-graph).

    noncomputable def kernel : E →L[ℝ] E :=
    …

33. lemma OAI.SmoothObstruction.FiniteGreen.Splitting.Terminal.kernel_factor line 223
34. lemma OAI.SmoothObstruction.FiniteGreen.Splitting.Terminal.kernel_norm line 233
35. def OAI.SmoothObstruction.EuclideanSplitting.evolution line 259
36. def OAI.SmoothObstruction.EuclideanSplitting.splitting line 271
37. lemma OAI.SmoothObstruction.EuclideanSplitting.forward_decay line 294
38. lemma OAI.SmoothObstruction.EuclideanSplitting.backward_decay line 309
39. lemma OAI.SmoothObstruction.EuclideanSplitting.splitting_slow_norm line 331
40. lemma OAI.SmoothObstruction.EuclideanSplitting.splitting_fast_norm line 338
41. theorem OAI.SmoothObstruction.EuclideanSplitting.unweighted_bounds line 345

    Source documentation

    The genuine unweighted Green bounds do not require negative slow rates. Their growth is only the threshold times the window, not the largest rate.

    theorem unweighted_bounds {K a : ℝ} {n : ℕ} (ha : 0≤a)
        (hU : ∀ t≤n,‖U t‖≤Real.exp K) (hV : ∀ t≤n,‖V t‖≤Real.exp K)
        (hs : ∀ j∈S,lam j≤a) (hf : ∀ j∈Sᶜ,-a≤lam j) :
        (∀ s t,s≤t → t≤n → ‖((evolution U V lam hUV hVU).map t s).comp
          ((splitting U V lam hUV hVU S).slow s)‖≤Real.exp (2*K+a*n)) ∧
        (∀ s t,s≤t → t≤n → ‖((evolution U V lam hUV hVU).map s t).comp
          ((splitting U V lam hUV hVU S).fast t)‖≤Real.exp (2*K+a*n)) := by
    …

    Mentions: OAI.SmoothObstruction.EuclideanSplitting.evolution, OAI.SmoothObstruction.EuclideanSplitting.splitting

42. theorem OAI.SmoothObstruction.EuclideanSplitting.endpoint_gap_bounds line 373

    Source documentation

    At the full endpoints the threshold cancels between slow forward and fast inverse growth, including the positive-slow case.

    theorem endpoint_gap_bounds {K γ g : ℝ} (n : ℕ)
        (hU : ∀ t≤n,‖U t‖≤Real.exp K) (hV : ∀ t≤n,‖V t‖≤Real.exp K)
        (hs : ∀ j∈S,lam j≤γ-g) (hf : ∀ j∈Sᶜ,γ+g≤lam j) :
        ‖((evolution U V lam hUV hVU).map n 0).comp
          ((splitting U V lam hUV hVU S).slow 0)‖≤Real.exp (2*K)*Real.exp ((γ-g)*n) ∧
        ‖((evolution U V lam hUV hVU).map 0 n).comp
          ((splitting U V lam hUV hVU S).fast n)‖≤Real.exp (2*K)*Real.exp (-(γ+g)*n) := by
    …

    Mentions: OAI.SmoothObstruction.EuclideanSplitting.evolution, OAI.SmoothObstruction.EuclideanSplitting.splitting

43. lemma OAI.SmoothObstruction.FiniteGreen.Splitting.slow_range_self line 393
44. lemma OAI.SmoothObstruction.FiniteGreen.Splitting.fast_range_self line 397
45. lemma OAI.SmoothObstruction.FiniteGreen.Splitting.slow_fast_range line 401
46. lemma OAI.SmoothObstruction.FiniteGreen.Splitting.fast_slow_range line 405
47. def OAI.SmoothObstruction.FiniteGreen.Splitting.referenceLinear line 412

    Source documentation

    Exact middle-time complementary matching. No determinant or angle nondegeneracy is assumed: it follows from the splitting identities.

    noncomputable def referenceLinear (t : ℕ) : ((B.slow t).range × (B.fast t).range) ≃ₗ[ℝ] E where
    …

48. def OAI.SmoothObstruction.FiniteGreen.Splitting.referenceMatching line 430
49. lemma OAI.SmoothObstruction.FiniteGreen.Splitting.referenceMatching_apply line 433
50. lemma OAI.SmoothObstruction.FiniteGreen.Splitting.referenceMatching_inverse_norm line 436
51. def OAI.SmoothObstruction.CloseProjection.restrictProjection line 456
52. lemma OAI.SmoothObstruction.CloseProjection.lower line 461

    Source documentation

    Equal-dimensional close spaces have a quantitatively invertible endpoint projection. This includes zero and full spaces without a separate convention.

    lemma lower (U V : Submodule ℝ E) (hclose : ‖U.starProjection-V.starProjection‖ ≤ 1/2) (x : U) :
        ‖x‖ ≤ 2*‖restrictProjection U V x‖ := by
    …

    Mentions: OAI.SmoothObstruction.CloseProjection.restrictProjection

53. lemma OAI.SmoothObstruction.CloseProjection.injective line 476
54. def OAI.SmoothObstruction.CloseProjection.equiv line 485
55. lemma OAI.SmoothObstruction.CloseProjection.equiv_apply line 491
56. lemma OAI.SmoothObstruction.CloseProjection.inverse_norm line 496
57. def OAI.SmoothObstruction.BoundaryNeumann.perturb line 514

    Source documentation

    A genuine inverse for an explicitly estimated perturbation of an invertible matching map. This is the Neumann step in source (4.15), with no bijectivity hypothesis on the perturbed map.

    noncomputable def perturb (L : E ≃L[ℝ] F) (D : E →L[ℝ] F)
        (h : ‖L.symm.toContinuousLinearMap.comp D‖ < 1) : E ≃L[ℝ] F :=
    …

58. lemma OAI.SmoothObstruction.BoundaryNeumann.perturb_apply line 519
59. lemma OAI.SmoothObstruction.BoundaryNeumann.inverse_bound line 526
60. lemma OAI.SmoothObstruction.BoundaryNeumann.inverse_norm line 554
61. def OAI.SmoothObstruction.CloseComplement.difference line 566
62. lemma OAI.SmoothObstruction.CloseComplement.difference_apply line 571
63. theorem OAI.SmoothObstruction.CloseComplement.exists_matching line 577

    Source documentation

    A pair of spaces close to a quantitatively complementary reference pair is genuinely complementary. The inverse is constructed by Neumann inversion on the reference product, and its norm is controlled.

    theorem exists_matching (U₀ V₀ U V : Submodule ℝ E)
        (L₀ : (U₀ × V₀) ≃L[ℝ] E) (hL₀ : ∀ x,L₀ x=(x.1:E)-(x.2:E))
        (hdU : Module.finrank ℝ U₀=Module.finrank ℝ U)
        (hdV : Module.finrank ℝ V₀=Module.finrank ℝ V)
        {ε K : ℝ} (hε : 0≤ε) (hεhalf : ε≤1/2)
        (hcU : ‖U₀.starProjection-U.starProjection‖≤ε)
        (hcV : ‖V₀.starProjection-V.starProjection‖≤ε)
        (hK : ‖L₀.symm.toContinuousLinearMap‖≤K) (hsmall : K*(2*ε)≤1/2) :
        ∃ L : (U × V) ≃L[ℝ] E,(∀ x,L x=(x.1:E)-(x.2:E)) ∧
          ‖L.symm.toContinuousLinearMap‖≤2*K := by
    …

64. def OAI.SmoothObstruction.FiniteGreen.Splitting.terminalProjection line 653

    Source documentation

    Fixed endpoint-bin orthogonal projection, together with its genuine inverse on the moving fast space. Empty endpoint spaces are included.

    noncomputable def terminalProjection (n : ℕ) (V : Submodule ℝ E)
        (hdim : Module.finrank ℝ (B.fast n).range=Module.finrank ℝ V)
        (hclose : ‖(B.fast n).range.starProjection-V.starProjection‖≤1/2) : B.Terminal (H:=V) n where
    …

65. lemma OAI.SmoothObstruction.FiniteGreen.Splitting.terminalProjection_P_norm line 678
66. lemma OAI.SmoothObstruction.FiniteGreen.Splitting.terminalProjection_J_norm line 688
67. lemma OAI.SmoothObstruction.FiniteGreen.Splitting.Terminal.kernel_norm_gap line 707

    Source documentation

    The endpoint graph correction is small even when the slow rates are positive. The two complementary exponentials cancel their threshold, leaving the spectral gap; no hyperbolic sign assumption was added.

    lemma kernel_norm_gap {G g γ : ℝ} (hG : 0≤G)
        (hback : ‖(A.map 0 n).comp (B.fast n)‖≤G*Real.exp (-(γ+g)*n))
        (hforw : ‖(A.map n 0).comp (B.slow 0)‖≤G*Real.exp ((γ-g)*n))
        (hJ : ‖C.J‖≤2) (hP : ‖C.P‖≤1) :
        ‖C.kernel‖≤2*G^2*Real.exp (-2*g*n) := by
    …

68. lemma OAI.SmoothObstruction.EuclideanSplitting.splitting_slow_range line 730
69. lemma OAI.SmoothObstruction.EuclideanSplitting.splitting_fast_range line 741