OAI/MathematicalPhysics/Transonic/Shooting/RegularGlobalRange.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SepticProfile.IntegerPolynomial.stepTime_zero line 10
2. lemma OAI.SepticProfile.IntegerPolynomial.stepTime_one line 12
3. lemma OAI.SepticProfile.IntegerPolynomial.start_eq_stop line 14
4. theorem OAI.SepticProfile.IntegerPolynomial.global_step_range line 19

   Source documentation

   The same integer certificate also certifies that the clamp is inactive at every point, not only the mesh endpoints.

   theorem global_step_range {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)) :
       ∀ t ∈ Icc (startTime R a) (stopTime R a), u t ∈ Icc (0:ℝ) (999/1000) := 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

5. lemma OAI.SepticProfile.IntegerPolynomial.unclamped_derivative line 42