SourceFamilyStrongSeed.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.SepticProfile.SourceFamily.slope_gt_one line 11

theorem OAI.SepticProfile.SourceFamily.UniformGerm.exists_uniform_strong_seed line 21

Source documentation

A common inward sonic starting point for every parameter in the shooting chart. Its compact margin from the singular value1 is positive, as required before an ordinary ODE (with a proved nonsingular denominator) can be used.

theorem UniformGerm.exists_uniform_strong_seed (G : UniformGerm) (limit : ℝ) (hlimit : 0<limit) :
    ∃ δ : ℝ, 0<δ ∧ δ<G.radius ∧ δ<limit ∧ δ<1/1000 ∧
      Continuous (fun a => (G.U a ((-δ:ℝ):ℂ)).re) ∧
      (∀ a, 0<(G.U a ((-δ:ℝ):ℂ)).re ∧ (G.U a ((-δ:ℝ):ℂ)).re<1-δ/2) ∧
      ∀ a x, |x|≤δ → 0<(G.U a (x:ℂ)).re ∧ 1/2<(G.V a (x:ℂ)).re := by
…