OAI/MathematicalPhysics/Transonic/Shooting/FiniteExistence.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SepticProfile.SonicShooting.exists_finite_transonic line 11

   Source documentation

   A selected-parameter finite transonic source profile.

   theorem exists_finite_transonic : ∃ (p : Parameter) (w : ℝ) (u : ℝ → ℝ),
       0<w ∧ ContDiffOn ℝ ∞ u (Icc 0 (1+w)) ∧
       (∀ z ∈ Icc (0:ℝ) (1+w), D (sig p) z (u z)*deriv u z=N (kap p) z (u z)) ∧
       (∀ z ∈ Ioo (0:ℝ) 1, u z ∈ Ioo (0:ℝ) 1) ∧
       (∀ z ∈ Ioc (0:ℝ) (1+w), u z=1 ↔ z=1) ∧ 0<deriv u 1 := by
   …