Theorems · Definition · ordinary differential equations

ODE.FunSpace.next

{E : Type u_1} →
  [inst : NormedAddCommGroup E] →
    [NormedSpace ℝ E] →
      {f : ℝ → E → E} →
        {tmin tmax : ℝ} →
          {t₀ : ↑(Set.Icc tmin tmax)} →
            {x₀ x : E} →
              {a r L K : NNReal} →
                IsPicardLindelof f t₀ x₀ a r L K →
                  x ∈ Metric.closedBall x₀ ↑r → ODE.FunSpace t₀ x₀ r L → ODE.FunSpace t₀ x₀ r L

The map on FunSpace defined by picard, some n-th iterate of which will be a contracting map

Defined in

Mathlib.Analysis.ODE.PicardLindelof

Cited by

16 results in Mathlib

Foundations

Depth 263 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupNormedSpace