OAI/MathematicalPhysics/Transonic/Shooting/FuchsianParametric.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SepticProfile.Fuchsian.continuous_coordinateMul line 11
2. lemma OAI.SepticProfile.Fuchsian.continuous_radialIntegral_shift line 21

   Source documentation

   The regular-singular inverse varies continuously with the positive indicial shift. Restricting the displayed global extension by max c 1 incurs no change for the shifts 76-rho>2 used in the selected source family.

   lemma continuous_radialIntegral_shift (f : analyticDisk) :
       Continuous (fun c : ℝ => radialIntegral (max c 1) f) := by
   …

   Mentions: OAI.SepticProfile.Fuchsian.analyticDisk, OAI.SepticProfile.Fuchsian.radialIntegral

3. lemma OAI.SepticProfile.Fuchsian.continuous_inverse_shift line 35
4. lemma OAI.SepticProfile.Fuchsian.inverse_lipschitz line 39
5. lemma OAI.SepticProfile.Fuchsian.continuous_inverse_family line 45
6. lemma OAI.SepticProfile.Fuchsian.continuous_fixedPoint_family line 69

   Source documentation

   Stability of fixed-point selection, used below for the parameterized sonic analytic family. The conclusion is derived, not a continuity assumption on the selected germs.

   lemma continuous_fixedPoint_family {A E : Type*} [TopologicalSpace A]
       [MetricSpace E] (T : A → E → E) (f : A → E)
       (hT : ∀ a, ContractingWith (1/2 : ℝ≥0) (T a))
       (hfix : ∀ a, Function.IsFixedPt (T a) (f a))
       (hcont : ∀ x, Continuous (fun a => T a x)) : Continuous f := by
   …