ODE

Results named in Tau Ceti's TauCeti.Analysis.ODE modules and in no roadmap's section, as Tau Ceti has them at commit ace60277.

TheoremCarathéodory's existence theorem for linear equations#

Let M : ℝ → E →L[ℝ] E be almost everywhere strongly measurable and essentially bounded on (a, b), and let F : ℝ → E be integrable on (a, b). Then the linear equation x' = M(t) x + F(t) with x(a) = x₀ has a solution in Carathéodory's sense: a curve x continuous on [a, b] with x a = x₀ and x t = x₀ + ∫ s in a..t, (M s (x s) + F s) for every t ∈ [a, b].

TauCeti.exists_continuousOn_eq_forall_mem_Icc_eq_picard.{u_1} {E : Type u_1} [NormedAddCommGroup E]
  [NormedSpace ℝ E] {M : ℝ → E →L[ℝ] E} {F : ℝ → E} {a b K : ℝ} [CompleteSpace E]
  (hM : MeasureTheory.AEStronglyMeasurable M (MeasureTheory.volume.restrict (Set.Ioo a b)))
  (hK : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo a b), ‖M t‖ ≤ K)
  (hF : MeasureTheory.IntegrableOn F (Set.Ioo a b) MeasureTheory.volume) (x₀ : E) :
  ∃ x,
    ContinuousOn x (Set.Icc a b) ∧
      x a = x₀ ∧ ∀ t ∈ Set.Icc a b, x t = ODE.picard (fun s y => (M s) y + F s) a x₀ x t
Lean

Formalized in Tau Ceti as TauCeti.exists_continuousOn_eq_forall_mem_Icc_eq_picard.

Sources
LeanTauCeti.exists_continuousOn_eq_forall_mem_Icc_eq_picard

TheoremThe Frobenius theorem for total differential equations#

Let E and F be finite-dimensional real normed spaces and let f : E × F → (E →L[ℝ] F) be C^(n+1) near p₀, for instance C¹. The total differential equation D u x = f (x, u x) has a local solution through every point near p₀ if and only if f satisfies the Frobenius integrability condition near p₀.

TauCeti.eventually_exists_hasFDerivAt_iff_eventually_isFrobeniusIntegrableAt.{u} {E F : Type u}
  [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F]
  [FiniteDimensional ℝ E] [FiniteDimensional ℝ F] {n : ℕ∞} {f : E × F → E →L[ℝ] F} {s : Set (E × F)}
  {p₀ : E × F} (hf : ContDiffOn ℝ (↑n + 1) f s) (hs : s ∈ nhds p₀) :
  (∀ᶠ (p : E × F) in nhds p₀,
      ∃ u, u p.1 = p.2 ∧ ∀ᶠ (x : E) in nhds p.1, HasFDerivAt u (f (x, u x)) x) ↔
    ∀ᶠ (p : E × F) in nhds p₀, TauCeti.IsFrobeniusIntegrableAt f p
Lean

Formalized in Tau Ceti as TauCeti.eventually_exists_hasFDerivAt_iff_eventually_isFrobeniusIntegrableAt.

Sources
LeanTauCeti.eventually_exists_hasFDerivAt_iff_eventually_isFrobeniusIntegrableAt
Uses 1 · Used by 1
Proof usesThe local Frobenius theorem (TauCeti.exists_eventually_hasFDerivAt_of_isFrobeniusIntegrableAt)
Used byThe Frobenius theorem in coordinates

TheoremGrönwall's inequality, integral form#

If φ is continuous on [a, b], 0 ≤ K and φ t ≤ c + K ∫ₐᵗ φ for every t ∈ [a, b], then φ t ≤ c exp (K (t - a)) on [a, b].

TauCeti.le_mul_exp_of_le_add_mul_integral {φ : ℝ → ℝ} {a b c K : ℝ}
  (hφ : ContinuousOn φ (Set.Icc a b)) (hK : 0 ≤ K)
  (h : ∀ t ∈ Set.Icc a b, φ t ≤ c + K * ∫ (s : ℝ) in a..t, φ s) (t : ℝ) :
  t ∈ Set.Icc a b → φ t ≤ c * Real.exp (K * (t - a))
Lean

Formalized in Tau Ceti as TauCeti.le_mul_exp_of_le_add_mul_integral.

Other forms

Grönwall's inequality for monotone functions, almost-everywhere form. Formalized in Tau Ceti as TauCeti.mul_exp_integral_le_of_mul_le_deriv.

TauCeti.mul_exp_integral_le_of_mul_le_deriv {g k : ℝ → ℝ} {s t : ℝ} (hst : s ≤ t)
  (hg : MonotoneOn g (Set.Icc s t)) (hgs : 0 ≤ g s)
  (hk : IntervalIntegrable k MeasureTheory.volume s t)
  (h : ∀ᵐ (σ : ℝ), σ ∈ Set.Ioo s t → k σ * g σ ≤ deriv g σ) :
  g s * Real.exp (∫ (σ : ℝ) in s..t, k σ) ≤ g t
Sources
LeanTauCeti.le_mul_exp_of_le_add_mul_integral · TauCeti.mul_exp_integral_le_of_mul_le_deriv

TheoremThe local Frobenius theorem (TauCeti.exists_eventually_hasFDerivAt_of_isFrobeniusIntegrableAt)#

Let E and F be finite-dimensional real normed spaces and let f : E × F → (E →L[ℝ] F) be C^(n+1) near (x₀, y₀), for instance C¹. If f satisfies the Frobenius integrability condition near (x₀, y₀), then the total differential equation D u x = f (x, u x) has a local solution u with u x₀ = y₀, which is C^(n+1) at x₀.

TauCeti.exists_eventually_hasFDerivAt_of_isFrobeniusIntegrableAt.{u} {E F : Type u}
  [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F]
  [FiniteDimensional ℝ E] [FiniteDimensional ℝ F] {n : ℕ∞} {f : E × F → E →L[ℝ] F} {s : Set (E × F)}
  {x₀ : E} {y₀ : F} (hf : ContDiffOn ℝ (↑n + 1) f s) (hs : s ∈ nhds (x₀, y₀))
  (hint : ∀ᶠ (p : E × F) in nhds (x₀, y₀), TauCeti.IsFrobeniusIntegrableAt f p) :
  ∃ u, u x₀ = y₀ ∧ ContDiffAt ℝ (↑n + 1) u x₀ ∧ ∀ᶠ (x : E) in nhds x₀, HasFDerivAt u (f (x, u x)) x
Lean

Formalized in Tau Ceti as TauCeti.exists_eventually_hasFDerivAt_of_isFrobeniusIntegrableAt.

Sources
LeanTauCeti.exists_eventually_hasFDerivAt_of_isFrobeniusIntegrableAt
Used by 2
Used byThe Frobenius theorem for total differential equations · The Frobenius theorem in coordinates

TheoremThe local stable-manifold theorem, Lipschitz form#

Near a hyperbolic equilibrium the initial values of the forward solutions that stay in a fixed small ball, truncated by the condition ‖P x‖ ≤ ρ, form the graph of a Lipschitz map over a ball in the stable subspace range P.

ContinuousLinearMap.exists_setOf_exists_isIntegralCurveOn_mapsTo_closedBall_eq_image.{u_1}
  {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] {K α ε : NNReal}
  {A P : X →L[ℝ] X} {N : X → X} {r : ℝ}
  (hs :
    ∀ (t : ℝ), 0 ≤ t → ∀ (v : X), ‖(NormedSpace.exp (t • A)) (P v)‖ ≤ ↑K * Real.exp (-↑α * t) * ‖v‖)
  (hu : ∀ t ≤ 0, ∀ (v : X), ‖(NormedSpace.exp (t • A)) (v - P v)‖ ≤ ↑K * Real.exp (↑α * t) * ‖v‖)
  (hN : LipschitzOnWith ε N (Metric.closedBall 0 r)) (hsmall : 2 * K * (ε * 2) < α) (hN0 : N 0 = 0)
  (hP : IsIdempotentElem P) (hAP : Commute A P) (hr0 : 0 < r) :
  ∃ ρ > 0,
    {x |
        (∃ y,
            IsIntegralCurveOn y (fun x z => A z + N z) (Set.Ici 0) ∧
              y 0 = x ∧ Set.MapsTo y (Set.Ici 0) (Metric.closedBall 0 r)) ∧
          ‖P x‖ ≤ ρ} =
      (fun v => v + A.localStableGraphMap P N r hs hu ⋯ hN hsmall v) ''
        (Set.range ⇑P ∩ Metric.closedBall 0 ρ)
Lean

Formalized in Tau Ceti as ContinuousLinearMap.exists_setOf_exists_isIntegralCurveOn_mapsTo_closedBall_eq_image.

Sources
LeanContinuousLinearMap.exists_setOf_exists_isIntegralCurveOn_mapsTo_closedBall_eq_image

TheoremThe local unstable-manifold theorem, Lipschitz form#

Near a hyperbolic equilibrium the initial values of backward solutions confined to a fixed small ball, truncated by the norm of their 1 - P component, form a graph over a ball in range (1 - P).

ContinuousLinearMap.exists_setOf_exists_isIntegralCurveOn_Iic_mapsTo_closedBall_eq_image.{u_1}
  {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] {K α ε : NNReal}
  {A P : X →L[ℝ] X} {N : X → X} {r : ℝ}
  (hs :
    ∀ (t : ℝ), 0 ≤ t → ∀ (v : X), ‖(NormedSpace.exp (t • A)) (P v)‖ ≤ ↑K * Real.exp (-↑α * t) * ‖v‖)
  (hu : ∀ t ≤ 0, ∀ (v : X), ‖(NormedSpace.exp (t • A)) (v - P v)‖ ≤ ↑K * Real.exp (↑α * t) * ‖v‖)
  (hN : LipschitzOnWith ε N (Metric.closedBall 0 r)) (hsmall : 2 * K * (ε * 2) < α) (hN0 : N 0 = 0)
  (hP : IsIdempotentElem P) (hAP : Commute A P) (hr0 : 0 < r) :
  ∃ ρ > 0,
    {x |
        (∃ y,
            IsIntegralCurveOn y (fun x z => A z + N z) (Set.Iic 0) ∧
              y 0 = x ∧ Set.MapsTo y (Set.Iic 0) (Metric.closedBall 0 r)) ∧
          ‖(ContinuousLinearMap.id ℝ X - P) x‖ ≤ ρ} =
      (fun v => v + A.localUnstableGraphMap P N r hs hu ⋯ hN hsmall v) ''
        (Set.range ⇑(ContinuousLinearMap.id ℝ X - P) ∩ Metric.closedBall 0 ρ)
Lean

Formalized in Tau Ceti as ContinuousLinearMap.exists_setOf_exists_isIntegralCurveOn_Iic_mapsTo_closedBall_eq_image.

Sources
LeanContinuousLinearMap.exists_setOf_exists_isIntegralCurveOn_Iic_mapsTo_closedBall_eq_image

TheoremThe straightening theorem (flow-box theorem)#

A C^n vector field w, 1 ≤ n, defined near a point a of a finite-dimensional real normed space, with w a ≠ 0, is constant in suitable C^n coordinates: there is an open partial homeomorphism φ, C^n on its source with C^n inverse on its target, such that a ∈ φ.source and dφ_y (w y) = w a for every y ∈ φ.source.

TauCeti.exists_openPartialHomeomorph_fderiv_eq_const.{u_1} {E : Type u_1} [NormedAddCommGroup E]
  [NormedSpace ℝ E] [FiniteDimensional ℝ E] {n : ℕ∞} (hn : 1 ≤ n) {w : E → E} {s : Set E} {a : E}
  (hw : ContDiffOn ℝ (↑n) w s) (hs : s ∈ nhds a) (ha : w a ≠ 0) :
  ∃ φ,
    a ∈ φ.source ∧
      (∀ y ∈ φ.source, ContDiffAt ℝ (↑n) (↑φ) y) ∧
        (∀ z ∈ φ.target, ContDiffAt ℝ (↑n) (↑φ.symm) z) ∧
          ∀ y ∈ φ.source, (fderiv ℝ (↑φ) y) (w y) = w a
Lean

Formalized in Tau Ceti as TauCeti.exists_openPartialHomeomorph_fderiv_eq_const.

Sources
LeanTauCeti.exists_openPartialHomeomorph_fderiv_eq_const
Uses 1 · Used by 1
Proof usesThe inverse function theorem, with a C^n inverse on the whole target
Used byThe straightening theorem [Lee, Thm. 9.22]

TheoremUniqueness in the local Frobenius theorem#

Two solutions of the total differential equation D u x = f (x, u x) near x₀ taking the same value at x₀ agree near x₀, as soon as f is Lipschitz near (x₀, u₁ x₀). Neither integrability nor finite dimensionality is needed: along each ray from x₀ both solutions solve the same ordinary differential equation.

TauCeti.eventuallyEq_of_eventually_hasFDerivAt.{u_1, u_2} {E : Type u_1} {F : Type u_2}
  [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F]
  {f : E × F → E →L[ℝ] F} {u₁ u₂ : E → F} {x₀ : E} {K : NNReal} {s : Set (E × F)}
  (hs : s ∈ nhds (x₀, u₁ x₀)) (hf : LipschitzOnWith K f s)
  (hu₁ : ∀ᶠ (x : E) in nhds x₀, HasFDerivAt u₁ (f (x, u₁ x)) x)
  (hu₂ : ∀ᶠ (x : E) in nhds x₀, HasFDerivAt u₂ (f (x, u₂ x)) x) (h₀ : u₁ x₀ = u₂ x₀) :
  u₁ =ᶠ[nhds x₀] u₂
Lean

Formalized in Tau Ceti as TauCeti.eventuallyEq_of_eventually_hasFDerivAt.

Sources
LeanTauCeti.eventuallyEq_of_eventually_hasFDerivAt

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.