OAI/MathematicalPhysics/Elasticity/ODE.lean

GitHub source file

57 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.ElasticityODE.Time line 10
  2. instance OAI.ElasticityODE.(instance at line 11) line 11
  3. def OAI.ElasticityODE.extend line 14
  4. lemma OAI.ElasticityODE.extend_apply line 16
  5. lemma OAI.ElasticityODE.extend_norm_le line 19
  6. lemma OAI.ElasticityODE.weighted_continuous line 22
  7. def OAI.ElasticityODE.weighted line 29
  8. lemma OAI.ElasticityODE.integral_exp_mul line 33
  9. lemma OAI.ElasticityODE.weighted_bound line 41
  10. def OAI.ElasticityODE.weightedCLM line 72

    Source documentation

    The actual exponentially weighted integration operator on the time interval. Its norm is at most 1/k; this supplies a uniform contraction for arbitrary bounded linear ODE coefficients, without an assumed global flow theorem.

    def weightedCLM (k : ℝ) (hk : 0<k) : C(Time,F) →L[ℝ] C(Time,F) :=
…

    Mentions: OAI.ElasticityODE.Time

  11. lemma OAI.ElasticityODE.weightedCLM_apply line 92
  12. lemma OAI.ElasticityODE.weightedCLM_norm line 93
  13. def OAI.ElasticityODE.pointwise line 108
  14. lemma OAI.ElasticityODE.pointwise_bound line 111
  15. def OAI.ElasticityODE.pointwiseLM line 117
  16. def OAI.ElasticityODE.pointwiseCLM line 125
  17. lemma OAI.ElasticityODE.pointwiseCLM_apply line 131
  18. lemma OAI.ElasticityODE.pointwiseCLM_norm line 134
  19. def OAI.ElasticityODE.expScale line 138
  20. lemma OAI.ElasticityODE.expScale_apply line 142
  21. lemma OAI.ElasticityODE.volterra_unit line 145
  22. def OAI.ElasticityODE.evolution line 156

    Source documentation

    Actual continuous evolution, defined by the invertible weighted Volterra operator. The coefficient need only be continuous in time.

    def evolution (k : ℝ) (hk : 0<k) (b : C(Time,F →L[ℝ] F)) (y : F) : C(Time,F) :=
…

    Mentions: OAI.ElasticityODE.Time

  23. lemma OAI.ElasticityODE.evolution_integral line 160
  24. theorem OAI.ElasticityODE.evolution_contDiffAt line 197

    Source documentation

    Strong smooth parameter dependence of the entire continuous trajectory.

    theorem evolution_contDiffAt (k : ℝ) (hk : 0<k)
    (b : P → C(Time,F →L[ℝ] F)) (y : P → F) (p : P)
    (hb : ContDiffAt ℝ (⊤ : ℕ∞) b p) (hy : ContDiffAt ℝ (⊤ : ℕ∞) y p)
    (hsmall : ‖b p‖<k) : ContDiffAt ℝ (⊤ : ℕ∞) (fun p => evolution k hk (b p) (y p)) p := by
…

    Mentions: OAI.ElasticityODE.Time, OAI.ElasticityODE.evolution

  25. lemma OAI.ElasticityODE.evolution_hasDerivWithinAt line 233

    Source documentation

    Integral solutions are genuine classical solutions, including one-sided endpoint derivatives.

    lemma evolution_hasDerivWithinAt (k : ℝ) (hk : 0<k) (b : C(Time,F →L[ℝ] F))
    (hb : ‖b‖<k) (y : F) (t : Time) :
    HasDerivWithinAt (extend (evolution k hk b y)) (b t (evolution k hk b y t)) Time t := by
…

    Mentions: OAI.ElasticityODE.Time, OAI.ElasticityODE.extend, OAI.ElasticityODE.evolution

  26. lemma OAI.ElasticityODE.evolution_initial line 249
  27. lemma OAI.ElasticityODE.linear_ode_unique line 256

    Source documentation

    Uniqueness on the entire time interval, with no smallness hypothesis.

    lemma linear_ode_unique (b : C(Time,F →L[ℝ] F)) (u v : C(Time,F))
    (hu : ∀ t : Time, HasDerivWithinAt (extend u) (b t (u t)) Time t)
    (hv : ∀ t : Time, HasDerivWithinAt (extend v) (b t (v t)) Time t)
    (hzero : u ⟨0,by simp [Time]⟩=v ⟨0,by simp [Time]⟩) : u=v := by
…

    Mentions: OAI.ElasticityODE.Time, OAI.ElasticityODE.extend

  28. def OAI.ElasticityODE.flow line 282

    Source documentation

    A globally defined linear evolution, not restricted to small coefficients.

    def flow (b : C(Time,F →L[ℝ] F)) (y : F) : C(Time,F) :=
…

    Mentions: OAI.ElasticityODE.Time

  29. lemma OAI.ElasticityODE.flow_hasDerivWithinAt line 284
  30. lemma OAI.ElasticityODE.flow_initial line 287
  31. lemma OAI.ElasticityODE.flow_eq_evolution line 289
  32. lemma OAI.ElasticityODE.evolution_contDiff line 295
  33. theorem OAI.ElasticityODE.flow_contDiff line 302
  34. def OAI.ElasticityODE.leftCoeff line 324
  35. def OAI.ElasticityODE.rightCoeff line 327
  36. def OAI.ElasticityODE.fundamental line 330
  37. def OAI.ElasticityODE.reciprocal line 331
  38. lemma OAI.ElasticityODE.fundamental_deriv line 332
  39. lemma OAI.ElasticityODE.reciprocal_deriv line 335
  40. lemma OAI.ElasticityODE.fundamental_initial line 338
  41. lemma OAI.ElasticityODE.reciprocal_initial line 340
  42. lemma OAI.ElasticityODE.reciprocal_mul_fundamental line 342
  43. lemma OAI.ElasticityODE.fundamental_mul_reciprocal line 359
  44. theorem OAI.ElasticityODE.fundamental_isUnit line 386
  45. def OAI.ElasticityODE.integrate line 398
  46. lemma OAI.ElasticityODE.integrate_bound line 402
  47. def OAI.ElasticityODE.integrateCLM line 414
  48. lemma OAI.ElasticityODE.integrateCLM_apply line 429
  49. lemma OAI.ElasticityODE.integral_curve_hasDerivWithinAt line 432
  50. lemma OAI.ElasticityODE.integral_family_variation line 454
  51. lemma OAI.ElasticityODE.integral_family_variation_hasDerivWithinAt line 474
  52. lemma OAI.ElasticityODE.flow_integral_curve line 494
  53. def OAI.ElasticityODE.leftCoeffCLM line 503
  54. lemma OAI.ElasticityODE.leftCoeffCLM_eq line 506
  55. lemma OAI.ElasticityODE.fundamental_contDiff line 507
  56. lemma OAI.ElasticityODE.fundamental_variation_hasDerivWithinAt line 515
  57. lemma OAI.ElasticityODE.fundamental_variation_initial line 534