OAI/Dynamics/SmoothObstruction/NonlinearMatching.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SmoothObstruction.SmoothRemainder.remainder line 20
2. lemma OAI.SmoothObstruction.SmoothRemainder.remainder_zero line 23
3. theorem OAI.SmoothObstruction.SmoothRemainder.remainder_lipschitz line 28

   Source documentation

   The actual, rather than hypothesized, nonlinear remainder has the small Lipschitz constant needed by the boundary contraction.

   theorem remainder_lipschitz (f : E → F) {x : E} {δ C : ℝ}
       (hC : 0≤C)
       (hf : ∀ y∈closedBall x δ,DifferentiableAt ℝ f y)
       (hder : ∀ y∈closedBall x δ,‖fderiv ℝ f y-fderiv ℝ f x‖≤C*‖y-x‖)
       {u v : E} (hu : ‖u‖≤δ) (hv : ‖v‖≤δ) :
       ‖remainder f x u-remainder f x v‖≤C*δ*‖u-v‖ := by
   …

   Mentions: OAI.SmoothObstruction.SmoothRemainder.remainder

4. theorem OAI.SmoothObstruction.SmoothRemainder.uniform_on_compact line 58

   Source documentation

   On a compact set strictly inside a C² coordinate domain, one common radius and one common constant work for all actual Taylor remainders. The estimate is uniform in the center and in the smaller tube radius.

   theorem uniform_on_compact (f : E → F) {U K : Set E}
       (hU : IsOpen U) (hK : IsCompact K) (hKU : K⊆U)
       (hf : ContDiffOn ℝ 2 f U) :
       ∃ r C : ℝ,0<r ∧ 0<C ∧ ∀ x∈K,∀ δ : ℝ,δ≤r →
         (∀ u v : E,‖u‖≤δ → ‖v‖≤δ →
           ‖remainder f x u-remainder f x v‖≤C*δ*‖u-v‖) ∧
         (∀ u : E,‖u‖≤δ → ‖remainder f x u‖≤C*‖u‖^2) := by
   …

   Mentions: OAI.SmoothObstruction.SmoothRemainder.remainder

5. abbrev OAI.SmoothObstruction.ArrayRemainder.Paths line 105
6. abbrev OAI.SmoothObstruction.ArrayRemainder.Data line 106
7. def OAI.SmoothObstruction.ArrayRemainder.residual line 111

   Source documentation

   Actual one-step Taylor residuals. The affine matching and terminal constraints really have zero residual.

   noncomputable def residual (f₁ : Fin n₁ → E → E) (f₂ : Fin n₂ → E → E)
       (x₁ : Fin n₁ → E) (x₂ : Fin n₂ → E)
       (v : Paths E n₁ n₂) : Data E H G n₁ n₂ :=
   …

   Mentions: OAI.SmoothObstruction.ArrayRemainder.Paths, OAI.SmoothObstruction.ArrayRemainder.Data

8. lemma OAI.SmoothObstruction.ArrayRemainder.residual_zero line 117
9. theorem OAI.SmoothObstruction.ArrayRemainder.residual_lipschitz line 122
10. theorem OAI.SmoothObstruction.ArrayRemainder.residual_from_derivative line 155

    Source documentation

    One common compact-domain Taylor estimate gives a residual Lipschitz constant independent of the number of orbit steps.

    theorem residual_from_derivative (f₁ : Fin n₁ → E → E) (f₂ : Fin n₂ → E → E)
        (x₁ : Fin n₁ → E) (x₂ : Fin n₂ → E) {C δ : ℝ} (hC : 0≤C) (hδ : 0≤δ)
        (hd₁ : ∀ t,∀ y∈closedBall (x₁ t) δ,DifferentiableAt ℝ (f₁ t) y)
        (hd₂ : ∀ t,∀ y∈closedBall (x₂ t) δ,DifferentiableAt ℝ (f₂ t) y)
        (h₁ : ∀ t,∀ y∈closedBall (x₁ t) δ,‖fderiv ℝ (f₁ t) y-fderiv ℝ (f₁ t) (x₁ t)‖≤C*‖y-x₁ t‖)
        (h₂ : ∀ t,∀ y∈closedBall (x₂ t) δ,‖fderiv ℝ (f₂ t) y-fderiv ℝ (f₂ t) (x₂ t)‖≤C*‖y-x₂ t‖)
        {u v : Paths E n₁ n₂} (hu : ‖u‖≤δ) (hv : ‖v‖≤δ) :
        ‖residual (H:=H) (G:=G) f₁ f₂ x₁ x₂ u-residual f₁ f₂ x₁ x₂ v‖≤C*δ*‖u-v‖ :=
    …

    Mentions: OAI.SmoothObstruction.ArrayRemainder.Paths, OAI.SmoothObstruction.ArrayRemainder.residual

11. theorem OAI.SmoothObstruction.ArrayRemainder.genuine_step line 169

    Source documentation

    The nonlinear recurrence is exactly the actual coordinate orbit equation, not just a formal shadowing sequence.

    theorem genuine_step (f : E → E) (x x' v v' : E) (hbase : f x=x')
        (heq : v'-(fderiv ℝ f x) v=SmoothRemainder.remainder f x v) :
        f (x+v)=x'+v' := by
    …

    Mentions: OAI.SmoothObstruction.SmoothRemainder.remainder

12. theorem OAI.SmoothObstruction.NonlinearBoundary.solve line 190

    Source documentation

    The boundary-inverse contraction from source section4. The ambient space can be a finite array with its supremum norm: no step-count factor is introduced. Uniqueness is on the larger radius δ, not just the sharp shadowing radius.

    theorem solve (L : E ≃L[ℝ] F) (R : E → F) (a : F)
        {Q C r δ : ℝ} (hQ : 0 ≤ Q) (hC : 0 ≤ C) (hr : 0 ≤ r) (hδ : 0 < δ)
        (hL : ‖L.symm.toContinuousLinearMap‖ ≤ Q)
        (ha : ‖a‖ ≤ C*r) (hR0 : R 0 = 0)
        (hR : ∀ u ∈ closedBall (0 : E) δ, ∀ v ∈ closedBall (0 : E) δ,
          ‖R u-R v‖ ≤ C*δ*‖u-v‖)
        (hsmall : Q*C*δ ≤ 1/4) (hdata : Q*C*r ≤ δ/4) :
        ∃ v : E, ‖v‖ ≤ δ/2 ∧ ‖v‖ ≤ 2*C*Q*r ∧ L v = a+R v ∧
          ∀ u : E, ‖u‖ ≤ δ → L u = a+R u → u=v := by
    …

13. theorem OAI.SmoothObstruction.NonlinearBoundary.nonlinear_linear_error line 252

    Source documentation

    The nonlinear correction differs quadratically from the linear solution, with the exact inverse cost. This is the source estimate used for ideal coordinate exchange, once the sharp norm bound is inserted.

    theorem nonlinear_linear_error (L : E ≃L[ℝ] F) {R : E → F} {a : F}
        {v : E} {Q C : ℝ} (hL : ‖L.symm.toContinuousLinearMap‖ ≤ Q)
        (_hC : 0 ≤ C) (hR : ‖R v‖ ≤ C*‖v‖^2) (heq : L v=a+R v) :
        ‖v-L.symm a‖ ≤ Q*C*‖v‖^2 := by
    …

14. theorem OAI.SmoothObstruction.FiniteGreen.Matching.nonlinear_orbits line 279

    Source documentation

    The finite boundary inverse and actual Taylor residual yield a genuine pair of nonlinear coordinate orbits, with a common middle point. All terminal equations remain exact. The derivative and propagation estimates are precisely the finite-window inputs, not the desired orbit conclusion.

    theorem nonlinear_orbits (L : (B₁.initialSpace × B₂.initialSpace) ≃L[ℝ] E)
        (hL : ∀ x,L x=(x.1:E)-(x.2:E)) {U K C r δ : ℝ}
        (hU : 1≤U) (hK : ‖L.symm.toContinuousLinearMap‖≤K)
        (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₁ : Fin n₁ → E → E) (f₂ : Fin n₂ → E → E)
        (x₁ : Fin (n₁+1) → E) (x₂ : Fin (n₂+1) → E)
    …

    Mentions: OAI.SmoothObstruction.FiniteGreen.Matching.correction

15. theorem OAI.SmoothObstruction.FiniteGreen.Matching.nonlinear_orbits_unique line 372

    Source documentation

    The finite boundary inverse and actual Taylor residual yield a genuine pair of nonlinear coordinate orbits, with a common middle point. All terminal equations remain exact. The derivative and propagation estimates are precisely the finite-window inputs, not the desired orbit conclusion.

    theorem nonlinear_orbits_unique (L : (B₁.initialSpace × B₂.initialSpace) ≃L[ℝ] E)
        (hL : ∀ x,L x=(x.1:E)-(x.2:E)) {U K C r δ : ℝ}
        (hU : 1≤U) (hK : ‖L.symm.toContinuousLinearMap‖≤K)
        (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₁ : Fin n₁ → E → E) (f₂ : Fin n₂ → E → E)
        (x₁ : Fin (n₁+1) → E) (x₂ : Fin (n₂+1) → E)
    …

    Mentions: OAI.SmoothObstruction.FiniteGreen.Matching.correction

16. lemma OAI.SmoothObstruction.IdealExchange.annihilator_bound line 490

    Source documentation

    Orthogonal gap control followed by an oblique complementary projector. This retains the reference inverse cost instead of silently treating the nonorthogonal slow/fast decomposition as orthogonal.

    lemma annihilator_bound (U V : Submodule ℝ E) (Q : E →L[ℝ] E)
        {ε G : ℝ} (hG : 0≤G) (_hε : 0≤ε)
        (hclose : ‖U.starProjection-V.starProjection‖≤ε)
        (hQ : ‖Q‖≤G) (hzero : ∀ v∈V,Q v=0) (x : U) :
        ‖Q (x:E)‖≤G*ε*‖x‖ := by
    …

17. theorem OAI.SmoothObstruction.IdealExchange.graph_exchange_error line 507

    Source documentation

    A pair of small endpoint graphs over nearby complementary spaces gives ideal exchange at time zero; the large full-window shadowing cost does not multiply the space-comparison error.

    theorem graph_exchange_error {A₀ : FiniteGreen.Evolution E}
        (B₀ : FiniteGreen.Splitting A₀) (U V : Submodule ℝ E)
        (C D : E →L[ℝ] E) (a : U) (b : V) (m : E)
        {ε κ G R : ℝ} (hε : 0≤ε) (hκ : 0≤κ) (hG : 0≤G) (_hR : 0≤R)
        (hcU : ‖U.starProjection-(B₀.slow 0).range.starProjection‖≤ε)
        (hcV : ‖V.starProjection-(B₀.fast 0).range.starProjection‖≤ε)
        (hC : ‖C‖≤κ) (hD : ‖D‖≤κ)
        (hP : ‖B₀.slow 0‖≤G) (hQ : ‖B₀.fast 0‖≤G)
        (ha : ‖a‖≤R) (hb : ‖b‖≤R)
        (hm : (a:E)+C a-((b:E)+D b)=m) :
        ‖((a:E)+C a)-B₀.slow 0 m‖≤2*G*(ε+κ)*R := by
    …

    Mentions: OAI.SmoothObstruction.FiniteGreen.Evolution, OAI.SmoothObstruction.FiniteGreen.Splitting

18. theorem OAI.SmoothObstruction.FiniteGreen.Matching.linear_initial_error line 559

    Source documentation

    Quantitative ideal exchange for the actual zero-forcing boundary inverse. The middle cost is O(exp(C b n)), separate from full-orbit exp(C g n).

    theorem linear_initial_error
        (L : (B₁.initialSpace×B₂.initialSpace) ≃L[ℝ] E)
        (hL : ∀ x,L x=(x.1:E)-(x.2:E))
        {K P ε κ : ℝ} (hK : ‖L.symm.toContinuousLinearMap‖≤K)
        (hP : 0≤P) (hε : 0≤ε) (hκ : 0≤κ)
        (hsmall : ‖L.symm.toContinuousLinearMap.comp (correction C₁ C₂)‖≤1/2)
        (hc₁ : ‖B₁.initialSpace.starProjection-(B₀.slow 0).range.starProjection‖≤ε)
        (hc₂ : ‖B₂.initialSpace.starProjection-(B₀.fast 0).range.starProjection‖≤ε)
        (hk₁ : ‖C₁.kernel‖≤κ) (hk₂ : ‖C₂.kernel‖≤κ)
        (hs : ‖B₀.slow 0‖≤P) (hf : ‖B₀.fast 0‖≤P)
        (v₁ v₂ : ℕ → E) (m : E)
        (hv₁ : ∀ t<n₁,v₁ (t+1)=A₁.map (t+1) t (v₁ t))
    …

    Mentions: OAI.SmoothObstruction.FiniteGreen.Matching.correction

19. theorem OAI.SmoothObstruction.ArrayRemainder.residual_quadratic line 620

    Source documentation

    The actual array residual is quadratic in the sup norm, with a constant independent of either window length. The smaller radius is the array norm.

    theorem residual_quadratic (f₁ : Fin n₁ → E → E) (f₂ : Fin n₂ → E → E)
        (x₁ : Fin n₁ → E) (x₂ : Fin n₂ → E) {C δ : ℝ} (hC : 0≤C)
        (hd₁ : ∀ t,∀ y∈closedBall (x₁ t) δ,DifferentiableAt ℝ (f₁ t) y)
        (hd₂ : ∀ t,∀ y∈closedBall (x₂ t) δ,DifferentiableAt ℝ (f₂ t) y)
        (h₁ : ∀ t,∀ y∈closedBall (x₁ t) δ,‖fderiv ℝ (f₁ t) y-fderiv ℝ (f₁ t) (x₁ t)‖≤C*‖y-x₁ t‖)
        (h₂ : ∀ t,∀ y∈closedBall (x₂ t) δ,‖fderiv ℝ (f₂ t) y-fderiv ℝ (f₂ t) (x₂ t)‖≤C*‖y-x₂ t‖)
        {v : Paths E n₁ n₂} (hv : ‖v‖≤δ) :
        ‖residual (H:=H) (G:=G) f₁ f₂ x₁ x₂ v‖≤C*‖v‖^2 := by
    …

    Mentions: OAI.SmoothObstruction.ArrayRemainder.Paths, OAI.SmoothObstruction.ArrayRemainder.residual

20. theorem OAI.SmoothObstruction.FiniteGreen.Matching.array_linear_initial_error line 644
21. theorem OAI.SmoothObstruction.FiniteGreen.Matching.array_nonlinear_initial_error line 687

    Source documentation

    Linear graph-space error and nonlinear residual have DIFFERENT costs. In particular, no full-window inverse multiplies the common-bin gap error.

    theorem array_nonlinear_initial_error
        (L : (B₁.initialSpace×B₂.initialSpace) ≃L[ℝ] E)
        (hL : ∀ x,L x=(x.1:E)-(x.2:E))
        {K P ε κ Q C : ℝ} (hK : ‖L.symm.toContinuousLinearMap‖≤K)
        (hP : 0≤P) (hε : 0≤ε) (hκ : 0≤κ) (hC : 0≤C)
        (hsmall : ‖L.symm.toContinuousLinearMap.comp (correction C₁ C₂)‖≤1/2)
        (hc₁ : ‖B₁.initialSpace.starProjection-(B₀.slow 0).range.starProjection‖≤ε)
        (hc₂ : ‖B₂.initialSpace.starProjection-(B₀.fast 0).range.starProjection‖≤ε)
        (hk₁ : ‖C₁.kernel‖≤κ) (hk₂ : ‖C₂.kernel‖≤κ)
        (hs : ‖B₀.slow 0‖≤P) (hf : ‖B₀.fast 0‖≤P)
        (R : Paths E n₁ n₂ → Data E H G n₁ n₂) (v : Paths E n₁ n₂) (m : E)
        (hR : ‖R v‖≤C*‖v‖^2)
    …

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