OAI/Dynamics/SmoothObstruction/EndpointFrames.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SmoothObstruction.EndpointFrame.exists_frame line 20

   Source documentation

   Finite endpoint coordinates are selected from a genuine ambient orthonormal basis, including the empty and full-dimensional endpoint groups.

   theorem exists_frame (W : Submodule ℝ E) (hdim : Module.finrank ℝ W=p) :
       ∃ (b : OrthonormalBasis (Fin d) ℝ E) (r : powersetCard (Fin d) p),
         (∀ j∈r,b j∈W) ∧ (∀ j∉r,b j∈Wᗮ) ∧
         (∀ x∈W,∀ j∉r,b.repr x j=0) := by
   …

2. def OAI.SmoothObstruction.EndpointFrame.coordinates line 60

   Source documentation

   The actual selected orthonormal coordinates, not a formal minor proxy.

   noncomputable def coordinates (b : OrthonormalBasis (Fin d) ℝ E)
       (r : powersetCard (Fin d) p) : E →L[ℝ] EuclideanSpace ℝ (Fin p) :=
   …

3. lemma OAI.SmoothObstruction.EndpointFrame.coordinates_apply line 67
4. lemma OAI.SmoothObstruction.EndpointFrame.coordinates_projection line 71
5. lemma OAI.SmoothObstruction.EndpointFrame.coordinates_eq_iff line 85

   Source documentation

   Endpoint-coordinate equality is precisely the reference projected endpoint datum used by the genuine boundary-value problem.

   lemma coordinates_eq_iff (W : Submodule ℝ E)
       (b : OrthonormalBasis (Fin d) ℝ E) (r : powersetCard (Fin d) p)
       (hr : ∀ j∈r,b j∈W) (hz : ∀ x∈W,∀ j∉r,b.repr x j=0) (x y : E) :
       coordinates b r x=coordinates b r y ↔ W.starProjection x=W.starProjection y := by
   …

   Mentions: OAI.SmoothObstruction.EndpointFrame.coordinates

6. lemma OAI.SmoothObstruction.ProductBasis.blockMap_basis_inl line 107
7. lemma OAI.SmoothObstruction.ProductBasis.blockMap_basis_inr line 119
8. def OAI.SmoothObstruction.EndpointFrame.joint line 138
9. def OAI.SmoothObstruction.EndpointFrame.jointLinear line 143
10. lemma OAI.SmoothObstruction.EndpointFrame.joint_hasFDerivAt line 149
11. lemma OAI.SmoothObstruction.EndpointFrame.joint_matrix line 158
12. lemma OAI.SmoothObstruction.EndpointFrame.joint_det line 182

    Source documentation

    The determinant of the actual joint endpoint differential in the common product input coordinates is exactly the block determinant estimated by the maximal-minor algebra. No leading volume lower floor is asserted.

    lemma joint_det (U V : Submodule ℝ E) (h : IsCompl U V)
        (bU : OrthonormalBasis (Fin p) ℝ U) (bV : OrthonormalBasis (Fin q) ℝ V)
        (bF bP : OrthonormalBasis (Fin d) ℝ E)
        (rF : powersetCard (Fin d) p) (rP : powersetCard (Fin d) q)
        (A B : E →L[ℝ] E) :
        ((jointLinear bF bP rF rP A B).comp (blockMap U V h bU bV).toContinuousLinearMap).det=
        (Matrix.fromBlocks (endpointMatrix bF p rF A (fun i => (bU i:E)))
          (endpointMatrix bF p rF A (fun i => (bV i:E)))
          (endpointMatrix bP q rP B (fun i => (bU i:E)))
          (endpointMatrix bP q rP B (fun i => (bV i:E)))).det := by
    …

    Mentions: OAI.SmoothObstruction.EndpointFrame.jointLinear

13. def OAI.SmoothObstruction.EndpointBranch.derivative line 200
14. theorem OAI.SmoothObstruction.EndpointBranch.local_branch line 207

    Source documentation

    Smooth local solution of all four endpoint equations, with its ACTUAL nondegenerate derivative. This statement is insensitive to zero-dimensional endpoint groups and keeps all four endpoint derivatives separate.

    theorem local_branch (f₀ f₁ g₀ g₁ : E → E) (x y z w : E)
        (A B C D : E ≃L[ℝ] E) (σ : (E×E) ≃L[ℝ] (E×E))
        (hf₀ : ContDiffAt ℝ ∞ f₀ x) (hf₁ : ContDiffAt ℝ ∞ f₁ y)
        (hg₀ : ContDiffAt ℝ ∞ g₀ z) (hg₁ : ContDiffAt ℝ ∞ g₁ w)
        (hA : HasFDerivAt f₀ (A : E →L[ℝ] E) x)
        (hB : HasFDerivAt f₁ (B : E →L[ℝ] E) y)
        (hC : HasFDerivAt g₀ (C : E →L[ℝ] E) z)
        (hD : HasFDerivAt g₁ (D : E →L[ℝ] E) w)
        (heq : Prod.map g₀ g₁ (z,w)=σ (Prod.map f₀ f₁ (x,y))) :
        ∃ Φ : E×E → E×E, Φ (x,y)=(z,w) ∧ ContDiffAt ℝ ∞ Φ (x,y) ∧
          HasFDerivAt Φ (derivative A B C D σ : (E×E) →L[ℝ] (E×E)) (x,y) ∧
          ∀ᶠ u in 𝓝 (x,y),Prod.map g₀ g₁ (Φ u)=σ (Prod.map f₀ f₁ u) := by
    …

    Mentions: OAI.SmoothObstruction.EndpointBranch.derivative

15. lemma OAI.SmoothObstruction.EndpointBranch.derivative_det line 252
16. lemma OAI.SmoothObstruction.EndpointBranch.derivative_abs_det line 275
17. def OAI.SmoothObstruction.EndpointBranch.exchange line 288

    Source documentation

    Exchange the past coordinates and leave the future coordinates fixed.

    def exchange : ((F×P)×(F×P)) ≃L[ℝ] ((F×P)×(F×P)) where
    …

18. lemma OAI.SmoothObstruction.EndpointBranch.exchange_abs_det line 298
19. lemma OAI.SmoothObstruction.JacobianBounds.abs_ratio_bounds line 312
20. theorem OAI.SmoothObstruction.JacobianBounds.four_cancel line 323

    Source documentation

    Four relative maximal-minor errors cancel the actual leading volumes individually. Rates of the two input orbits never need to be compared.

    theorem four_cancel
        (a b c d u v w z : ℝ) (ha : 0<a) (hb : 0<b) (hc : 0<c) (hd : 0<d)
        (hu : |u/(a*b)-1|≤(1/10:ℝ)) (hv : |v/(c*d)-1|≤(1/10:ℝ))
        (hw : |w/(a*d)-1|≤(1/10:ℝ)) (hz : |z/(c*b)-1|≤(1/10:ℝ)) :
        w≠0 ∧ z≠0 ∧ (81/121:ℝ)≤|u| *|v| /(|w| *|z|) ∧
          |u| *|v| /(|w| *|z|)≤(121/81:ℝ) := by
    …

21. theorem OAI.SmoothObstruction.JacobianBounds.density_lower line 351

    Source documentation

    A mild smooth-density error leaves enough room for the unnormalized factor-two pushforward estimate.

    theorem density_lower {J din dout : ℝ} (hdin : 0≤din)
        (hJ : (81/121:ℝ)≤J) (hd : (3/4:ℝ)*din≤dout) : din≤2*(J*dout) := by
    …

22. def OAI.SmoothObstruction.EndpointBranch.equiv_of_det line 365
23. lemma OAI.SmoothObstruction.EndpointBranch.equiv_of_det_coe line 369
24. theorem OAI.SmoothObstruction.EndpointBranch.controlled_branch line 377

    Source documentation

    Construct the true smooth branch from four absolute, relative endpoint-minor estimates. None of the four endpoint derivatives is assumed invertible, and no leading volume is bounded away from zero.

    theorem controlled_branch (f₀ f₁ g₀ g₁ : E → E) (x y z w : E)
        (A B C D : E →L[ℝ] E) (σ : (E×E) ≃L[ℝ] (E×E))
        (hf₀ : ContDiffAt ℝ ∞ f₀ x) (hf₁ : ContDiffAt ℝ ∞ f₁ y)
        (hg₀ : ContDiffAt ℝ ∞ g₀ z) (hg₁ : ContDiffAt ℝ ∞ g₁ w)
        (hA : HasFDerivAt f₀ A x) (hB : HasFDerivAt f₁ B y)
        (hC : HasFDerivAt g₀ C z) (hD : HasFDerivAt g₁ D w)
        (heq : Prod.map g₀ g₁ (z,w)=σ (Prod.map f₀ f₁ (x,y)))
        (hσ : |(σ : (E×E) →L[ℝ] (E×E)).det|=1)
        (a b c d : ℝ) (ha : 0<a) (hb : 0<b) (hc : 0<c) (hd : 0<d)
        (haA : |(|A.det| / (a*b)-1)|≤(1/10:ℝ))
        (hbB : |(|B.det| / (c*d)-1)|≤(1/10:ℝ))
        (hcC : |(|C.det| / (a*d)-1)|≤(1/10:ℝ))
    …

25. def OAI.SmoothObstruction.EndpointBranch.sumExchange line 421

    Source documentation

    The exact future/past exchange in the orthonormal sum coordinates used for the endpoint block matrices.

    noncomputable def sumExchange : (F×F) ≃L[ℝ] (F×F) :=
    …

26. lemma OAI.SmoothObstruction.EndpointBranch.sumExchange_abs_det line 426
27. lemma OAI.SmoothObstruction.EndpointBranch.absolute_relative line 439

    Source documentation

    Signed relative determinants give precisely the absolute, relative volume estimates required by the actual inverse-function branch.

    lemma absolute_relative {u a b ε : ℝ} (h : |u/(a*b)-1|≤ε) :
        |(|u|/(|a| * |b|))-1|≤ε := by
    …

28. lemma OAI.SmoothObstruction.EndpointBranch.conjugate_det line 448

    Source documentation

    The common starting-basis determinant cancels exactly, without either orthogonality between the two summands or a determinant lower bound.

    lemma conjugate_det (L : E ≃L[ℝ] F) (A : E →L[ℝ] E) :
        (L.toContinuousLinearMap.comp (A.comp L.symm.toContinuousLinearMap)).det=A.det := by
    …

29. lemma OAI.SmoothObstruction.EndpointBranch.linear_conjugate_det line 463
30. theorem OAI.SmoothObstruction.EndpointBranch.physical_controlled_branch line 475

    Source documentation

    The controlled endpoint branch in the original physical coordinates. The same (possibly badly conditioned) starting basis is used for all four endpoint maps, and cancels exactly from the joint Jacobian.

    theorem physical_controlled_branch (L : F ≃L[ℝ] E)
        (f₀ f₁ g₀ g₁ : E → F) (x y z w : E)
        (A B C D : E →L[ℝ] F) (σ : (F×F) ≃L[ℝ] (F×F))
        (hf₀ : ContDiffAt ℝ ∞ f₀ x) (hf₁ : ContDiffAt ℝ ∞ f₁ y)
        (hg₀ : ContDiffAt ℝ ∞ g₀ z) (hg₁ : ContDiffAt ℝ ∞ g₁ w)
        (hA : HasFDerivAt f₀ A x) (hB : HasFDerivAt f₁ B y)
        (hC : HasFDerivAt g₀ C z) (hD : HasFDerivAt g₁ D w)
        (heq : Prod.map g₀ g₁ (z,w)=σ (Prod.map f₀ f₁ (x,y)))
        (hσ : |(σ : (F×F) →L[ℝ] (F×F)).det|=1)
        (a b c d : ℝ) (ha : 0<a) (hb : 0<b) (hc : 0<c) (hd : 0<d)
        (haA : |(|(A.comp L.toContinuousLinearMap).det| / (a*b)-1)|≤(1/10:ℝ))
        (hbB : |(|(B.comp L.toContinuousLinearMap).det| / (c*d)-1)|≤(1/10:ℝ))
    …

31. lemma OAI.SmoothObstruction.EndpointFrame.joint_contDiffAt line 535
32. theorem OAI.SmoothObstruction.EndpointFrame.joint_controlled_det line 546

    Source documentation

    The true joint endpoint differential inherits the four-volume relative bound from the genuine selected endpoint minors. The modulus is chosen only from the dimensions, and permits either group to be empty.

    theorem joint_controlled_det : ∃ δ : ℝ,0<δ ∧
        ∀ (U V : Submodule ℝ E) (h : IsCompl U V)
          (bU : OrthonormalBasis (Fin p) ℝ U) (bV : OrthonormalBasis (Fin q) ℝ V)
          (bF bP : OrthonormalBasis (Fin d) ℝ E)
          (rF : powersetCard (Fin d) p) (rP : powersetCard (Fin d) q)
          (f g : E → E) (x : E) (A₀ : Matrix (Fin p) (Fin p) ℝ)
          (D₀ : Matrix (Fin q) (Fin q) ℝ),
          DifferentiableAt ℝ f x → DifferentiableAt ℝ g x →
          A₀.det≠0 → D₀.det≠0 →
          let A := endpointMatrix bF p rF (fderiv ℝ f x) (fun i => (bU i:E))
    …

33. def OAI.SmoothObstruction.EndpointFrame.GoodEndpoint line 580

    Source documentation

    The same leading minor is used at the old and perturbed point.

    def GoodEndpoint {r s : ℕ} (δ : ℝ)
        (b : OrthonormalBasis (Fin d) ℝ E) (a : powersetCard (Fin d) r)
        (u : Fin r → E) (v : Fin s → E) (f : E → E) (x : E)
        (D₀ : Matrix (Fin r) (Fin r) ℝ) : Prop :=
    …

34. theorem OAI.SmoothObstruction.EndpointFrame.four_endpoint_branch line 593

    Source documentation

    Four actual endpoint maps produce one smooth two-point exchange germ. This is a relative determinant statement at all ranks, in the original physical coordinates. The common nonorthogonal input-basis determinant cancels, including when either block has rank zero.

    theorem four_endpoint_branch : ∃ δ : ℝ,0<δ ∧
        ∀ (U V : Submodule ℝ E) (_ : IsCompl U V)
          (u : OrthonormalBasis (Fin p) ℝ U) (v : OrthonormalBasis (Fin q) ℝ V)
          (b₀ b₁ c₀ c₁ : OrthonormalBasis (Fin d) ℝ E)
          (r₀ r₁ : powersetCard (Fin d) p) (s₀ s₁ : powersetCard (Fin d) q)
          (f₀ f₁ g₀ g₁ : E → E) (x y z w : E)
          (A₀ A₁ : Matrix (Fin p) (Fin p) ℝ) (D₀ D₁ : Matrix (Fin q) (Fin q) ℝ),
          GoodEndpoint δ b₀ r₀ (fun i => (u i:E)) (fun i => (v i:E)) f₀ x A₀ →
          GoodEndpoint δ b₀ r₀ (fun i => (u i:E)) (fun i => (v i:E)) f₀ z A₀ →
          GoodEndpoint δ b₁ r₁ (fun i => (u i:E)) (fun i => (v i:E)) f₁ y A₁ →
          GoodEndpoint δ b₁ r₁ (fun i => (u i:E)) (fun i => (v i:E)) f₁ w A₁ →
          GoodEndpoint δ c₀ s₀ (fun i => (v i:E)) (fun i => (u i:E)) g₀ x D₀ →
    …

    Mentions: OAI.SmoothObstruction.EndpointFrame.GoodEndpoint

35. lemma OAI.SmoothObstruction.ExteriorStability.endpointMatrix_projection line 671
36. theorem OAI.SmoothObstruction.EuclideanSplitting.endpoint_bounds line 689

    Source documentation

    Actual endpoint-coordinate matrices with a common input frame. The old leading volume, its perturbed relative value, and every true graph entry are controlled together. No lower volume floor, rate sign, positive rank, or orthogonality between the two input groups is required.

    theorem endpoint_bounds
        (U V : ℕ → Matrix (Fin d) (Fin d) ℝ) (lam : Fin d → ℝ)
        (hUV : ∀ t,U t*V t=1) (hVU : ∀ t,V t*U t=1)
        (S : Finset (Fin d)) (hSp : S.card=p) (n : ℕ) {γ g K C δ : ℝ}
        (hg : 0≤g) (hK : 0≤K) (hC : 0≤C) (hδ : 0≤δ)
        (hfast : ∀ j∈S,γ+g≤lam j) (hslow : ∀ j∉S,lam j≤γ-g)
        (hUs : ‖U 0‖≤Real.exp K) (hUt : ‖U n‖≤Real.exp K)
        (hVs : ‖V 0‖≤Real.exp K) (hVt : ‖V n‖≤Real.exp K)
        (hpoly : ∀ A : E₀ →L[ℝ] E₀,‖exterior p A‖≤C*(max 1 ‖A‖)^p)
        (W G Gslow : Submodule ℝ E₀) (hdim : Module.finrank ℝ W=p)
        (hend : ‖(groupSpace (U n) (V n) (hUV n) (hVU n) S).starProjection-W.starProjection‖≤1/2)
        (hstart : ‖(groupSpace (U 0) (V 0) (hUV 0) (hVU 0) S).starProjection-G.starProjection‖≤δ)
    …

    Mentions: OAI.SmoothObstruction.EuclideanSplitting.groupSpace

37. theorem OAI.SmoothObstruction.ManifoldCoordinates.actual_endpoint_minor line 751

    Source documentation

    A genuine old-chart endpoint map has the controlled minor used in the four-equation inverse theorem. Every nonlinear derivative estimate is derived from the original orbit tube and the real one-step gauge. Constants precede all ranks, bins, times and gauge choices.

    theorem actual_endpoint_minor (hclosed : IsClosed (range I))
        (S : Diffeomorph I I M M ∞) (a : ι → M) (L : ι → Set M)
        (hL : ∀ i,IsCompact (L i)) (hLU : ∀ i,L i⊆(chartAt H (a i)).source)
        (Dg : ℝ) (hDg : 0≤Dg) :
        ∃ r K₀ Crel C₁ : ℝ,0<r ∧ 1≤K₀ ∧ 0≤Crel ∧ 0≤C₁ ∧
          ∀ {p q : ℕ} (c : M → ι) (x y : M) (m : ℕ)
            (U V : ℕ → Matrix (Fin d) (Fin d) ℝ) (lam : Fin d → ℝ)
            (T : Finset (Fin d)) (_ : T.card=p) (γ g K b n R C δ β : ℝ),
            (∀ z,z∈L (c z)) → 0≤b → 0≤n → 1≤b*n → 0≤R →
            0≤g → 0≤K → K≤Dg*(b*n) → (m : ℝ)≤2*n → 0≤C → 0≤δ →
            ∀ (hUV : ∀ t,U t*V t=1) (hVU : ∀ t,V t*U t=1),
            (∀ t < m,(Matrix.toEuclideanCLM (n:=Fin d) (𝕜:=ℝ)).symm
    …