OAI/MathematicalPhysics/Transonic/Shooting/RegularGlobalControl.lean

GitHub source file

59 declarations, 0 contain sorry, 0 declared as axioms

Exact integer polynomial evaluation and interval control for the regular shooting ODE.

  1. abbrev OAI.SepticProfile.IntegerPolynomial.Poly line 10
  2. def OAI.SepticProfile.IntegerPolynomial.add line 12
  3. def OAI.SepticProfile.IntegerPolynomial.scale line 17
  4. def OAI.SepticProfile.IntegerPolynomial.sub line 20
  5. def OAI.SepticProfile.IntegerPolynomial.mul line 21
  6. def OAI.SepticProfile.IntegerPolynomial.der line 24
  7. def OAI.SepticProfile.IntegerPolynomial.sq line 27
  8. def OAI.SepticProfile.IntegerPolynomial.eval line 29
  9. def OAI.SepticProfile.IntegerPolynomial.norm line 33
  10. def OAI.SepticProfile.IntegerPolynomial.head line 37
  11. def OAI.SepticProfile.IntegerPolynomial.tailNorm line 39
  12. def OAI.SepticProfile.IntegerPolynomial.Positive line 41
  13. instance OAI.SepticProfile.IntegerPolynomial.(instance at line 42) line 42
  14. lemma OAI.SepticProfile.IntegerPolynomial.eval_add line 44
  15. lemma OAI.SepticProfile.IntegerPolynomial.eval_scale line 52
  16. lemma OAI.SepticProfile.IntegerPolynomial.eval_sub line 57
  17. lemma OAI.SepticProfile.IntegerPolynomial.eval_mul line 60
  18. lemma OAI.SepticProfile.IntegerPolynomial.eval_sq line 65
  19. lemma OAI.SepticProfile.IntegerPolynomial.hasDerivAt_eval line 68
  20. lemma OAI.SepticProfile.IntegerPolynomial.contDiff_eval line 79
  21. lemma OAI.SepticProfile.IntegerPolynomial.norm_nonneg line 84
  22. lemma OAI.SepticProfile.IntegerPolynomial.eval_abs_le line 87
  23. lemma OAI.SepticProfile.IntegerPolynomial.eval_deviation line 98
  24. lemma OAI.SepticProfile.IntegerPolynomial.eval_pos line 108
  25. lemma OAI.SepticProfile.IntegerPolynomial.eval_bounds line 113
  26. def OAI.SepticProfile.IntegerPolynomial.residual line 126

    Source documentation

    Numerator after substituting z=(Z-Hs)/R, u=P(s)/Q in the exact normalized source ODE. All arithmetic in certificates is integral.

    def residual (S SN K KN R Q Z H : ℤ) (p : Poly) : Poly :=
…

    Mentions: OAI.SepticProfile.IntegerPolynomial.Poly

  27. def OAI.SepticProfile.IntegerPolynomial.denom line 133
  28. def OAI.SepticProfile.IntegerPolynomial.numer line 134
  29. def OAI.SepticProfile.IntegerPolynomial.coordinate line 136
  30. def OAI.SepticProfile.IntegerPolynomial.velocity line 138
  31. lemma OAI.SepticProfile.IntegerPolynomial.eval_singleton line 140
  32. lemma OAI.SepticProfile.IntegerPolynomial.eval_linear line 141
  33. lemma OAI.SepticProfile.IntegerPolynomial.eval_residual line 143
  34. lemma OAI.SepticProfile.IntegerPolynomial.hasDerivAt_velocity line 159
  35. lemma OAI.SepticProfile.IntegerPolynomial.residual_strict line 163
  36. lemma OAI.SepticProfile.IntegerPolynomial.residual_negative line 177
  37. lemma OAI.SepticProfile.IntegerPolynomial.eval_zero line 200
  38. lemma OAI.SepticProfile.IntegerPolynomial.eval_one line 203
  39. structure OAI.SepticProfile.IntegerPolynomial.Step line 206
  40. def OAI.SepticProfile.IntegerPolynomial.Range line 212
  41. instance OAI.SepticProfile.IntegerPolynomial.(instance at line 214) line 214
  42. def OAI.SepticProfile.IntegerPolynomial.Valid line 217
  43. instance OAI.SepticProfile.IntegerPolynomial.(instance at line 222) line 222
  44. lemma OAI.SepticProfile.IntegerPolynomial.range_velocity line 225
  45. lemma OAI.SepticProfile.IntegerPolynomial.coordinate_bounds line 236
  46. lemma OAI.SepticProfile.IntegerPolynomial.denom_pos line 250
  47. def OAI.SepticProfile.IntegerPolynomial.stepField line 265
  48. theorem OAI.SepticProfile.IntegerPolynomial.step_control line 271

    Source documentation

    Exact signed polynomial residuals control the actual clamped ODE, not an approximate trajectory. The comparison proves the clamp inactive on this step.

    theorem step_control {S SN K KN R Q : ℤ} (hs : 0<S) (hk : 0<K) (hr : 0<R)
    (hq : 0<Q) (hsigma : ((SN:ℝ)/S) ∈ Icc (0:ℝ) 1) {a : Step}
    (ha : Valid S SN K KN R Q a) {w : ℝ → ℝ}
    (hwc : ContinuousOn w (Icc 0 1))
    (hwd : ∀ s ∈ Icc (0:ℝ) 1, HasDerivWithinAt w
      (stepField (SN/S) (KN/K) R a.Z a.H s (w s)) (Icc 0 1) s)
    (hw0 : w 0 ∈ Icc ((head a.lo:ℝ)/Q) ((head a.hi:ℝ)/Q)) :
    ∀ s ∈ Icc (0:ℝ) 1, w s ∈ Icc (velocity Q a.lo s) (velocity Q a.hi s) := by
…

    Mentions: OAI.SepticProfile.IntegerPolynomial.Step, OAI.SepticProfile.IntegerPolynomial.Valid, OAI.SepticProfile.IntegerPolynomial.stepField, OAI.SepticProfile.IntegerPolynomial.head, OAI.SepticProfile.IntegerPolynomial.velocity

  49. def OAI.SepticProfile.IntegerPolynomial.globalField line 332
  50. def OAI.SepticProfile.IntegerPolynomial.stepTime line 335
  51. def OAI.SepticProfile.IntegerPolynomial.startTime line 336
  52. def OAI.SepticProfile.IntegerPolynomial.stopTime line 337
  53. lemma OAI.SepticProfile.IntegerPolynomial.hasDerivAt_stepTime line 339
  54. lemma OAI.SepticProfile.IntegerPolynomial.stepTime_mem line 345
  55. lemma OAI.SepticProfile.IntegerPolynomial.localized_derivative line 352
  56. theorem OAI.SepticProfile.IntegerPolynomial.global_step_endpoint line 371

    Source documentation

    Each integer certificate propagates a rigorous interval for the same single globally constructed clamped solution. No approximate flow is used.

    theorem global_step_endpoint {S SN K KN R Q : ℤ} (hs : 0<S) (hk : 0<K) (hr : 0<R)
    (hq : 0<Q) (hsigma : ((SN:ℝ)/S) ∈ Icc (0:ℝ) 1) {a : Step}
    (ha : Valid S SN K KN R Q a) {u : ℝ → ℝ}
    (hud : ∀ t ∈ Icc (0:ℝ) (9/100), HasDerivWithinAt u (globalField (SN/S) (KN/K) t (u t))
      (Icc 0 (9/100)) t)
    (hu0 : u (startTime R a) ∈ Icc ((head a.lo:ℝ)/Q) ((head a.hi:ℝ)/Q)) :
    u (stopTime R a) ∈ Icc ((a.lo.sum:ℝ)/Q) ((a.hi.sum:ℝ)/Q) := by
…

    Mentions: OAI.SepticProfile.IntegerPolynomial.Step, OAI.SepticProfile.IntegerPolynomial.Valid, OAI.SepticProfile.IntegerPolynomial.globalField, OAI.SepticProfile.IntegerPolynomial.startTime, OAI.SepticProfile.IntegerPolynomial.head, OAI.SepticProfile.IntegerPolynomial.stopTime

  57. lemma OAI.SepticProfile.IntegerPolynomial.join_bound line 386
  58. lemma OAI.SepticProfile.IntegerPolynomial.regular_field_contDiffOn line 401
  59. theorem OAI.SepticProfile.IntegerPolynomial.exists_global_clamped_solution line 415

    Source documentation

    A single exact clamped trajectory exists on the entire regular shooting interval. Step certificates will certify its value, rather than assume a flow.

    theorem exists_global_clamped_solution (sigma kappa : ℝ) (hs : sigma ∈ Icc (0:ℝ) 1)
    (u0 : ℝ) : ∃ u : ℝ → ℝ, u 0=u0 ∧ ContinuousOn u (Icc (0:ℝ) (9/100)) ∧
      ∀ t ∈ Icc (0:ℝ) (9/100), HasDerivWithinAt u (globalField sigma kappa t (u t))
        (Icc 0 (9/100)) t := by
…

    Mentions: OAI.SepticProfile.sigma, OAI.SepticProfile.kappa, OAI.SepticProfile.IntegerPolynomial.globalField