OAI/MathematicalPhysics/NavierStokes/ForcedComputation/Flow/FlowPicardSmooth.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Smooth Picard residual on a fixed unit interval. The elapsed time is a parameter, so evaluating the solution at the endpoint is a bounded linear map.

  1. def OAI.ForcedComputation.Flow.picardResidual line 20
  2. theorem OAI.ForcedComputation.Flow.picardResidual_smooth line 24
  3. def OAI.ForcedComputation.Flow.picardPathDerivative line 35
  4. theorem OAI.ForcedComputation.Flow.picardResidual_hasFDerivAt_path line 41
  5. theorem OAI.ForcedComputation.Flow.isInvertible_one_sub_of_norm_lt_one line 51
  6. theorem OAI.ForcedComputation.Flow.picardPathDerivative_invertible line 59
  7. theorem OAI.ForcedComputation.Flow.picardResidual_partial line 82
  8. theorem OAI.ForcedComputation.Flow.exists_local_picard_family line 97

    Source documentation

    A short Picard solution belongs to a smooth local family of Picard solutions. The family is obtained from the library implicit-function theorem.

    theorem exists_local_picard_family (Z : C(E, E))
    (hZ : ContDiff ℝ ∞ (Z : E → E)) {L τ : ℝ}
    (hL : 0 ≤ L) (hbound : ∀ x, ‖fderiv ℝ Z x‖ ≤ L)
    (hτ : |τ| * L < 1) (x : E) (γ : C(UnitTime, E))
    (hγ : picardResidual Z ((τ, x), γ) = 0) :
    ∃ Γ : (ℝ × E) → C(UnitTime, E),
      ContDiffAt ℝ ∞ Γ (τ, x) ∧ Γ (τ, x) = γ ∧
        ∀ᶠ p in 𝓝 (τ, x), picardResidual Z (p, Γ p) = 0 := by
…

    Mentions: OAI.ForcedComputation.Flow.UnitTime, OAI.ForcedComputation.Flow.picardResidual