OAI/Dynamics/ThreeTorus/PhysicalJets.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

Finite passage geometry families, physical charts, and all-jet bounds.

  1. structure OAI.ThreeTorus.PassageGeometryFamily line 18
  2. def OAI.ThreeTorus.PassageGeometryFamily.sigma line 49
  3. def OAI.ThreeTorus.PassageGeometryFamily.scale line 50
  4. lemma OAI.ThreeTorus.PassageGeometryFamily.scale_pos line 51
  5. lemma OAI.ThreeTorus.PassageGeometryFamily.sigma_continuous line 54
  6. def OAI.ThreeTorus.StateTracks line 60

    Source documentation

    The linked support displacement of an actual next state. The old support point is shared by the index and every temporal comparison.

    def StateTracks {ι κ : Type*} (F : PassagePackets ι) (G : PassagePackets κ)
    (parent : κ → ι) (B B' η : ℝ) : Prop :=
…

    Mentions: OAI.ThreeTorus.PassagePackets

  7. lemma OAI.ThreeTorus.StateTracks.density line 67
  8. lemma OAI.ThreeTorus.StateTracks.mono line 77
  9. lemma OAI.ThreeTorus.StateTracks.trans line 84
  10. lemma OAI.ThreeTorus.PassageGeometryFamily.smooth_jitter_of_output line 120

    Source documentation

    Smoothness of the retained speed recovers smoothness of the actual jitter; no additional regularity hypothesis on a passage is needed.

    lemma smooth_jitter_of_output {ι : Type*} (G : PassagePackets ι) {n : ℕ}
    (hn : 0 < n) (hG : G.V = fun x => (1+g.J₀ x/n)/n) :
    ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞) g.J₀ := by
…

    Mentions: OAI.ThreeTorus.PassagePackets

  11. def OAI.ThreeTorus.PassageGeometryFamily.correctedFamily line 134

    Source documentation

    The integer carrier contributes only a deck translation. Removing it makes the limit the literal old twist lift, including at derivative order 0.

    def correctedFamily (r : ℝ) (p : ℝ × ℝ) (x : Cover) : Cover :=
…

    Mentions: OAI.ThreeTorus.Cover

  12. lemma OAI.ThreeTorus.PassageGeometryFamily.correctedFamily_zero line 137
  13. lemma OAI.ThreeTorus.PassageGeometryFamily.correctedFamily_smooth line 145
  14. lemma OAI.ThreeTorus.PassageGeometryFamily.physical_jets_tendsto line 153

    Source documentation

    Every spatial jet still converges after an arbitrary fixed smooth change of physical coordinates. Both signs of the map use this same theorem.

    lemma physical_jets_tendsto (hV : ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞) V)
    (hJ : ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞) g.J₀)
    {A B : Cover → Cover} (hA : ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞) A)
    (hB : ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞) B)
    (r : ℝ) {K : Set Cover} (hK : IsCompact K) (d : ℕ) :
    TendstoUniformlyOn
      (fun (n : ℕ) x => iteratedFDeriv ℝ d
        (fun y => B (g.correctedFamily r ((n:ℝ)⁻¹,g.Δ n) (A y))) x)
      (fun x => iteratedFDeriv ℝ d
        (fun y => B ![A y 0+r*V (A y 1),A y 1,A y 2]) x) atTop K := by
…

    Mentions: OAI.ThreeTorus.Cover

  15. lemma OAI.ThreeTorus.PassageGeometryFamily.eventually_physical_jets line 177

    Source documentation

    Any finite list of physical smooth seminorm restrictions can be imposed before selecting the passage integer, simultaneously for map and inverse.

    lemma eventually_physical_jets {ι : Type*} [Fintype ι]
    (hV : ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞) V)
    (hJ : ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞) g.J₀)
    {A B : Cover → Cover} (hA : ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞) A)
    (hB : ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞) B)
    (r : ι → ℝ) (K : ι → Set Cover) (hK : ∀ i, IsCompact (K i)) (d : ι → ℕ)
    (ε : ι → ℝ) (he : ∀ i, 0 < ε i) :
    ∀ᶠ n : ℕ in atTop, ∀ i x, x ∈ K i →
      dist (iteratedFDeriv ℝ (d i)
        (fun y => B (g.correctedFamily (r i) ((n:ℝ)⁻¹,g.Δ n) (A y))) x)
        (iteratedFDeriv ℝ (d i)
          (fun y => B ![A y 0+r i*V (A y 1),A y 1,A y 2]) x) < ε i := by
…

    Mentions: OAI.ThreeTorus.Cover

  16. def OAI.ThreeTorus.tripleProject line 209
  17. def OAI.ThreeTorus.coverTwist line 211
  18. def OAI.ThreeTorus.coverChart line 214
  19. def OAI.ThreeTorus.coverChartInv line 215
  20. def OAI.ThreeTorus.coverDeck line 217
  21. lemma OAI.ThreeTorus.smooth_coverChart line 219
  22. lemma OAI.ThreeTorus.smooth_coverChartInv line 226
  23. lemma OAI.ThreeTorus.smooth_coverDeck line 233
  24. lemma OAI.ThreeTorus.tripleProject_coverDeck line 238
  25. lemma OAI.ThreeTorus.coverChart_graph line 246
  26. lemma OAI.ThreeTorus.coverChartInv_graph line 253
  27. structure OAI.ThreeTorus.PhysicalFrame line 260
  28. def OAI.ThreeTorus.PhysicalFrame.ident line 271
  29. def OAI.ThreeTorus.PhysicalFrame.mapLift line 280
  30. lemma OAI.ThreeTorus.PhysicalFrame.mapLift_smooth line 283
  31. def OAI.ThreeTorus.PassageGeometryFamily.primitive line 297
  32. lemma OAI.ThreeTorus.PassageGeometryFamily.primitive_smooth line 299
  33. lemma OAI.ThreeTorus.PassageGeometryFamily.primitive_matches line 303
  34. lemma OAI.ThreeTorus.PassageGeometryFamily.chart_twist_chartInv line 310
  35. def OAI.ThreeTorus.PhysicalFrame.next line 333
  36. lemma OAI.ThreeTorus.PhysicalFrame.next_mapLift line 350
  37. def OAI.ThreeTorus.physicalError line 377
  38. lemma OAI.ThreeTorus.physicalError_integrable line 380
  39. lemma OAI.ThreeTorus.physicalError_nonneg line 384
  40. lemma OAI.ThreeTorus.physicalError_chart line 387
  41. lemma OAI.ThreeTorus.physicalError_triangle line 392
  42. lemma OAI.ThreeTorus.physicalError_sum line 409