OAI/MathematicalPhysics/Transonic/Shooting/ClampedFamily.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SepticProfile.RegularContinuation.exists_continuous_clamped_family line 15

   Source documentation

   Parameter dependence for the regular portion of the shooting construction. We use the actual scalar vector field with explicit clamping, and freeze the parameter as a second ODE coordinate. Clamping is removed only after comparison.

   theorem exists_continuous_clamped_family {A : Type*} [TopologicalSpace A] [CompactSpace A]
       {a b p q c d : ℝ} (hab : a≤b) (hpq : p≤q) (hcd : c≤d)
       {f : ℝ × (ℝ×ℝ) → ℝ}
       (hf : ContDiffOn ℝ 1 f (Icc a b ×ˢ (Icc p q ×ˢ Icc c d)))
       (parameter initial : A → ℝ) (hpar : Continuous parameter) (hini : Continuous initial)
       (hparmem : ∀ x, parameter x ∈ Icc p q) :
       ∃ u : A → ℝ → ℝ,
         Continuous (fun v : A × ↥(Icc a b) => u v.1 v.2) ∧
         (∀ x, u x a=initial x) ∧
         ∀ x t, t ∈ Icc a b → HasDerivWithinAt (u x)
           (f (t,parameter x,clamp c d (u x t))) (Icc a b) t := by
   …

   Mentions: OAI.SepticProfile.q, OAI.SepticProfile.RegularContinuation.clamp