OAI/MathematicalPhysics/Transonic/Shooting/FamilyQuotient.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SepticProfile.FamilyC1.exists_uniform_quotient_bounds line 16

   Source documentation

   Uniform differentiability and Lipschitz bounds for the actual rational sonic remainder family. Compactness is applied to the constructed finite coefficient family, and only the nonzero sonic divisor is needed.

   theorem exists_uniform_quotient_bounds {n d : A → V → ℂ}
       (N : Data n) (D : Data d) (hn : ∀ a, d a 0 ≠ 0) :
       ∃ R : ℝ, 0 < R ∧ ∃ K : ℝ≥0, ∃ M : ℝ, 0 ≤ M ∧
         (∀ a v, v ∈ closedBall 0 R → d a v ≠ 0) ∧
         (∀ a, DifferentiableOn ℂ (fun v => n a v/d a v) (closedBall 0 R)) ∧
         (∀ a, LipschitzOnWith K (fun v => n a v/d a v) (closedBall 0 R)) ∧
         Continuous (fun p : A × ↥(closedBall (0:V) R) => n p.1 p.2/d p.1 p.2) ∧
         ∀ a, ‖n a 0/d a 0‖ ≤ M := by
   …

   Mentions: OAI.SepticProfile.FamilyC1.V, OAI.SepticProfile.FamilyC1.Data