Documentation

Mathlib.Analysis.ODE.PicardLindelof

Picard-Lindelöf (Cauchy-Lipschitz) Theorem #

In this file we prove that an ordinary differential equation $\dot x=v(t, x)$ such that $v$ is Lipschitz continuous in $x$ and continuous in $t$ has a local solution, see IsPicardLindelof.exists_forall_hasDerivWithinAt_Icc_eq.

As a corollary, we prove that a time-independent locally continuously differentiable ODE has a local solution.

Implementation notes #

In order to split the proof into small lemmas, we introduce a structure PicardLindelof that holds all assumptions of the main theorem. This structure and lemmas in the PicardLindelof namespace should be treated as private implementation details. This is not to be confused with the Prop- valued structure IsPicardLindelof, which holds the long hypotheses of the Picard-Lindelöf theorem for actual use as part of the public API.

We only prove existence of a solution in this file. For uniqueness see ODE_solution_unique and related theorems in Mathlib/Analysis/ODE/Gronwall.lean.

Tags #

differential equation

structure IsPicardLindelof {E : Type u_2} [NormedAddCommGroup E] (v : EE) (tMin : ) (t₀ : ) (tMax : ) (x₀ : E) (L : NNReal) (R : ) (C : ) :

Prop structure holding the hypotheses of the Picard-Lindelöf theorem.

The similarly named PicardLindelof structure is part of the internal API for convenience, so as not to constantly invoke choice, but is not intended for public use.

Instances For
    theorem IsPicardLindelof.ht₀ {E : Type u_2} [NormedAddCommGroup E] {v : EE} {tMin : } {t₀ : } {tMax : } {x₀ : E} {L : NNReal} {R : } {C : } (self : IsPicardLindelof v tMin t₀ tMax x₀ L R C) :
    t₀ Set.Icc tMin tMax
    theorem IsPicardLindelof.hR {E : Type u_2} [NormedAddCommGroup E] {v : EE} {tMin : } {t₀ : } {tMax : } {x₀ : E} {L : NNReal} {R : } {C : } (self : IsPicardLindelof v tMin t₀ tMax x₀ L R C) :
    0 R
    theorem IsPicardLindelof.lipschitz {E : Type u_2} [NormedAddCommGroup E] {v : EE} {tMin : } {t₀ : } {tMax : } {x₀ : E} {L : NNReal} {R : } {C : } (self : IsPicardLindelof v tMin t₀ tMax x₀ L R C) (t : ) :
    t Set.Icc tMin tMaxLipschitzOnWith L (v t) (Metric.closedBall x₀ R)
    theorem IsPicardLindelof.cont {E : Type u_2} [NormedAddCommGroup E] {v : EE} {tMin : } {t₀ : } {tMax : } {x₀ : E} {L : NNReal} {R : } {C : } (self : IsPicardLindelof v tMin t₀ tMax x₀ L R C) (x : E) :
    x Metric.closedBall x₀ RContinuousOn (fun (t : ) => v t x) (Set.Icc tMin tMax)
    theorem IsPicardLindelof.norm_le {E : Type u_2} [NormedAddCommGroup E] {v : EE} {tMin : } {t₀ : } {tMax : } {x₀ : E} {L : NNReal} {R : } {C : } (self : IsPicardLindelof v tMin t₀ tMax x₀ L R C) (t : ) :
    t Set.Icc tMin tMaxxMetric.closedBall x₀ R, v t x C
    theorem IsPicardLindelof.C_mul_le_R {E : Type u_2} [NormedAddCommGroup E] {v : EE} {tMin : } {t₀ : } {tMax : } {x₀ : E} {L : NNReal} {R : } {C : } (self : IsPicardLindelof v tMin t₀ tMax x₀ L R C) :
    C * max (tMax - t₀) (t₀ - tMin) R
    structure PicardLindelof (E : Type u_2) [NormedAddCommGroup E] [NormedSpace E] :
    Type u_2

    This structure holds arguments of the Picard-Lipschitz (Cauchy-Lipschitz) theorem. It is part of the internal API for convenience, so as not to constantly invoke choice. Unless you want to use one of the auxiliary lemmas, use IsPicardLindelof.exists_forall_hasDerivWithinAt_Icc_eq instead of using this structure.

    The similarly named IsPicardLindelof is a bundled Prop holding the long hypotheses of the Picard-Lindelöf theorem as named arguments. It is used as part of the public API.

    Instances For
      theorem PicardLindelof.isPicardLindelof {E : Type u_2} [NormedAddCommGroup E] [NormedSpace E] (self : PicardLindelof E) :
      IsPicardLindelof self.toFun self.tMin (↑self.t₀) self.tMax self.x₀ self.L self.R self.C
      Equations
      • PicardLindelof.instCoeFunForallRealForall = { coe := PicardLindelof.toFun }
      Equations
      • One or more equations did not get rendered due to their size.
      theorem PicardLindelof.nonempty_Icc {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] (v : PicardLindelof E) :
      (Set.Icc v.tMin v.tMax).Nonempty
      theorem PicardLindelof.lipschitzOnWith {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] (v : PicardLindelof E) {t : } (ht : t Set.Icc v.tMin v.tMax) :
      LipschitzOnWith v.L (v.toFun t) (Metric.closedBall v.x₀ v.R)
      theorem PicardLindelof.norm_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] (v : PicardLindelof E) {t : } (ht : t Set.Icc v.tMin v.tMax) {x : E} (hx : x Metric.closedBall v.x₀ v.R) :
      v.toFun t x v.C

      The maximum of distances from t₀ to the endpoints of [tMin, tMax].

      Equations
      • v.tDist = max (v.tMax - v.t₀) (v.t₀ - v.tMin)
      Instances For
        theorem PicardLindelof.dist_t₀_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] (v : PicardLindelof E) (t : (Set.Icc v.tMin v.tMax)) :
        dist t v.t₀ v.tDist
        def PicardLindelof.proj {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] (v : PicardLindelof E) :
        (Set.Icc v.tMin v.tMax)

        Projection $ℝ → [t_{\min}, t_{\max}]$ sending $(-∞, t_{\min}]$ to $t_{\min}$ and $[t_{\max}, ∞)$ to $t_{\max}$.

        Equations
        Instances For
          theorem PicardLindelof.proj_coe {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] (v : PicardLindelof E) (t : (Set.Icc v.tMin v.tMax)) :
          v.proj t = t
          theorem PicardLindelof.proj_of_mem {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] (v : PicardLindelof E) {t : } (ht : t Set.Icc v.tMin v.tMax) :
          (v.proj t) = t

          The space of curves $γ \colon [t_{\min}, t_{\max}] \to E$ such that $γ(t₀) = x₀$ and $γ$ is Lipschitz continuous with constant $C$. The map sending $γ$ to $\mathbf Pγ(t)=x₀ + ∫_{t₀}^{t} v(τ, γ(τ))\,dτ$ is a contracting map on this space, and its fixed point is a solution of the ODE $\dot x=v(t, x)$.

          • toFun : (Set.Icc v.tMin v.tMax)E
          • map_t₀' : self.toFun v.t₀ = v.x₀
          • lipschitz' : LipschitzWith v.C self.toFun
          Instances For
            theorem PicardLindelof.FunSpace.map_t₀' {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {v : PicardLindelof E} (self : v.FunSpace) :
            self.toFun v.t₀ = v.x₀
            theorem PicardLindelof.FunSpace.lipschitz' {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {v : PicardLindelof E} (self : v.FunSpace) :
            LipschitzWith v.C self.toFun
            instance PicardLindelof.FunSpace.instCoeFunForallElemRealIccTMinTMax {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {v : PicardLindelof E} :
            CoeFun v.FunSpace fun (x : v.FunSpace) => (Set.Icc v.tMin v.tMax)E
            Equations
            • PicardLindelof.FunSpace.instCoeFunForallElemRealIccTMinTMax = { coe := PicardLindelof.FunSpace.toFun }
            Equations
            • PicardLindelof.FunSpace.instInhabited = { default := { toFun := fun (x : (Set.Icc v.tMin v.tMax)) => v.x₀, map_t₀' := , lipschitz' := } }
            theorem PicardLindelof.FunSpace.lipschitz {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {v : PicardLindelof E} (f : v.FunSpace) :
            LipschitzWith v.C f.toFun
            def PicardLindelof.FunSpace.toContinuousMap {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {v : PicardLindelof E} :
            v.FunSpace C((Set.Icc v.tMin v.tMax), E)

            Each curve in PicardLindelof.FunSpace is continuous.

            Equations
            • PicardLindelof.FunSpace.toContinuousMap = { toFun := fun (f : v.FunSpace) => { toFun := f.toFun, continuous_toFun := }, inj' := }
            Instances For
              Equations
              • PicardLindelof.FunSpace.instMetricSpace = MetricSpace.induced PicardLindelof.FunSpace.toContinuousMap inferInstance
              @[deprecated PicardLindelof.FunSpace.isUniformInducing_toContinuousMap]
              theorem PicardLindelof.FunSpace.uniformInducing_toContinuousMap {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {v : PicardLindelof E} :
              IsUniformInducing PicardLindelof.FunSpace.toContinuousMap

              Alias of PicardLindelof.FunSpace.isUniformInducing_toContinuousMap.

              theorem PicardLindelof.FunSpace.range_toContinuousMap {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {v : PicardLindelof E} :
              Set.range PicardLindelof.FunSpace.toContinuousMap = {f : C((Set.Icc v.tMin v.tMax), E) | f v.t₀ = v.x₀ LipschitzWith v.C f}
              theorem PicardLindelof.FunSpace.map_t₀ {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {v : PicardLindelof E} (f : v.FunSpace) :
              f.toFun v.t₀ = v.x₀
              theorem PicardLindelof.FunSpace.mem_closedBall {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {v : PicardLindelof E} (f : v.FunSpace) (t : (Set.Icc v.tMin v.tMax)) :
              f.toFun t Metric.closedBall v.x₀ v.R
              def PicardLindelof.FunSpace.vComp {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {v : PicardLindelof E} (f : v.FunSpace) (t : ) :
              E

              Given a curve $γ \colon [t_{\min}, t_{\max}] → E$, PicardLindelof.vComp is the function $F(t)=v(π t, γ(π t))$, where π is the projection $ℝ → [t_{\min}, t_{\max}]$. The integral of this function is the image of γ under the contracting map we are going to define below.

              Equations
              • f.vComp t = v.toFun (↑(v.proj t)) (f.toFun (v.proj t))
              Instances For
                theorem PicardLindelof.FunSpace.vComp_apply_coe {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {v : PicardLindelof E} (f : v.FunSpace) (t : (Set.Icc v.tMin v.tMax)) :
                f.vComp t = v.toFun (↑t) (f.toFun t)
                theorem PicardLindelof.FunSpace.norm_vComp_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {v : PicardLindelof E} (f : v.FunSpace) (t : ) :
                f.vComp t v.C
                theorem PicardLindelof.FunSpace.dist_apply_le_dist {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {v : PicardLindelof E} (f₁ : v.FunSpace) (f₂ : v.FunSpace) (t : (Set.Icc v.tMin v.tMax)) :
                dist (f₁.toFun t) (f₂.toFun t) dist f₁ f₂
                theorem PicardLindelof.FunSpace.dist_le_of_forall {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {v : PicardLindelof E} {f₁ : v.FunSpace} {f₂ : v.FunSpace} {d : } (h : ∀ (t : (Set.Icc v.tMin v.tMax)), dist (f₁.toFun t) (f₂.toFun t) d) :
                dist f₁ f₂ d
                theorem PicardLindelof.FunSpace.intervalIntegrable_vComp {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {v : PicardLindelof E} (f : v.FunSpace) (t₁ : ) (t₂ : ) :
                IntervalIntegrable f.vComp MeasureTheory.volume t₁ t₂
                def PicardLindelof.FunSpace.next {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {v : PicardLindelof E} (f : v.FunSpace) :
                v.FunSpace

                The Picard-Lindelöf operator. This is a contracting map on PicardLindelof.FunSpace v such that the fixed point of this map is the solution of the corresponding ODE.

                More precisely, some iteration of this map is a contracting map.

                Equations
                • f.next = { toFun := fun (t : (Set.Icc v.tMin v.tMax)) => v.x₀ + ∫ (τ : ) in v.t₀..t, f.vComp τ, map_t₀' := , lipschitz' := }
                Instances For
                  theorem PicardLindelof.FunSpace.next_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {v : PicardLindelof E} (f : v.FunSpace) (t : (Set.Icc v.tMin v.tMax)) :
                  f.next.toFun t = v.x₀ + ∫ (τ : ) in v.t₀..t, f.vComp τ
                  theorem PicardLindelof.FunSpace.dist_next_apply_le_of_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {v : PicardLindelof E} {f₁ : v.FunSpace} {f₂ : v.FunSpace} {n : } {d : } (h : ∀ (t : (Set.Icc v.tMin v.tMax)), dist (f₁.toFun t) (f₂.toFun t) (v.L * |t - v.t₀|) ^ n / n.factorial * d) (t : (Set.Icc v.tMin v.tMax)) :
                  dist (f₁.next.toFun t) (f₂.next.toFun t) (v.L * |t - v.t₀|) ^ (n + 1) / (n + 1).factorial * d
                  theorem PicardLindelof.FunSpace.dist_iterate_next_apply_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {v : PicardLindelof E} (f₁ : v.FunSpace) (f₂ : v.FunSpace) (n : ) (t : (Set.Icc v.tMin v.tMax)) :
                  dist ((PicardLindelof.FunSpace.next^[n] f₁).toFun t) ((PicardLindelof.FunSpace.next^[n] f₂).toFun t) (v.L * |t - v.t₀|) ^ n / n.factorial * dist f₁ f₂
                  theorem PicardLindelof.FunSpace.dist_iterate_next_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {v : PicardLindelof E} (f₁ : v.FunSpace) (f₂ : v.FunSpace) (n : ) :
                  dist (PicardLindelof.FunSpace.next^[n] f₁) (PicardLindelof.FunSpace.next^[n] f₂) (v.L * v.tDist) ^ n / n.factorial * dist f₁ f₂
                  theorem PicardLindelof.FunSpace.hasDerivWithinAt_next {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {v : PicardLindelof E} (f : v.FunSpace) [CompleteSpace E] (t : (Set.Icc v.tMin v.tMax)) :
                  HasDerivWithinAt (f.next.toFun v.proj) (v.toFun (↑t) (f.toFun t)) (Set.Icc v.tMin v.tMax) t
                  theorem PicardLindelof.exists_contracting_iterate {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] (v : PicardLindelof E) :
                  ∃ (N : ) (K : NNReal), ContractingWith K PicardLindelof.FunSpace.next^[N]
                  theorem PicardLindelof.exists_fixed {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] (v : PicardLindelof E) [CompleteSpace E] :
                  ∃ (f : v.FunSpace), f.next = f
                  theorem PicardLindelof.exists_solution {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] (v : PicardLindelof E) [CompleteSpace E] :
                  ∃ (f : E), f v.t₀ = v.x₀ tSet.Icc v.tMin v.tMax, HasDerivWithinAt f (v.toFun t (f t)) (Set.Icc v.tMin v.tMax) t

                  Picard-Lindelöf (Cauchy-Lipschitz) theorem. Use IsPicardLindelof.exists_forall_hasDerivWithinAt_Icc_eq instead for the public API.

                  theorem IsPicardLindelof.norm_le₀ {E : Type u_2} [NormedAddCommGroup E] {v : EE} {tMin : } {t₀ : } {tMax : } {x₀ : E} {C : } {R : } {L : NNReal} (hpl : IsPicardLindelof v tMin t₀ tMax x₀ L R C) :
                  v t₀ x₀ C
                  theorem IsPicardLindelof.exists_forall_hasDerivWithinAt_Icc_eq {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E] {v : EE} {tMin : } {t₀ : } {tMax : } (x₀ : E) {C : } {R : } {L : NNReal} (hpl : IsPicardLindelof v tMin t₀ tMax x₀ L R C) :
                  ∃ (f : E), f t₀ = x₀ tSet.Icc tMin tMax, HasDerivWithinAt f (v t (f t)) (Set.Icc tMin tMax) t

                  Picard-Lindelöf (Cauchy-Lipschitz) theorem.

                  theorem exists_isPicardLindelof_const_of_contDiffAt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {v : EE} (t₀ : ) {x₀ : E} (hv : ContDiffAt 1 v x₀) :
                  ε > 0, ∃ (L : NNReal) (R : ) (C : ), IsPicardLindelof (fun (x : ) => v) (t₀ - ε) t₀ (t₀ + ε) x₀ L R C

                  A time-independent, continuously differentiable ODE satisfies the hypotheses of the Picard-Lindelöf theorem.

                  theorem exists_forall_hasDerivAt_Ioo_eq_of_contDiffAt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {v : EE} (t₀ : ) {x₀ : E} [CompleteSpace E] (hv : ContDiffAt 1 v x₀) :
                  ∃ (f : E), f t₀ = x₀ ε > 0, tSet.Ioo (t₀ - ε) (t₀ + ε), HasDerivAt f (v (f t)) t

                  A time-independent, continuously differentiable ODE admits a solution in some open interval.

                  theorem exists_forall_hasDerivAt_Ioo_eq_of_contDiff {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {v : EE} (t₀ : ) {x₀ : E} [CompleteSpace E] (hv : ContDiff 1 v) :
                  ∃ (f : E), f t₀ = x₀ ε > 0, tSet.Ioo (t₀ - ε) (t₀ + ε), HasDerivAt f (v (f t)) t

                  A time-independent, continuously differentiable ODE admits a solution in some open interval.