SonicContinuationLink.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

structure OAI.SepticProfile.SonicContinuation.PolynomialCertificate line 13
Source documentation
Finite arithmetic certificate interface for the actual selected weak sonic Taylor series, retaining the exact normalized septic source equation.
```
structure PolynomialCertificate (sigma kappa s : ℝ) : Prop where
…
```
Mentions: OAI.SepticProfile.sigma, OAI.SepticProfile.kappa

theorem OAI.SepticProfile.SonicContinuation.exists_germ_and_continuation line 36

Source documentation

Supplies a genuine analytic sonic germ and a genuine solution continued to z=.99 (Euler t=5/6). The germ is constructed by the regular-singular inverse; no ordinary Picard assumption is made at the singular point x=0.

theorem exists_germ_and_continuation (sigma kappa s rho : ℝ) (hsig : sigma<1)
    (hs : 2*(1-sigma)*s^2-(1-(3/5:ℝ))*(2*kappa+3)*s+3*(1-(3/5:ℝ))=0)
    (hd : 2*(1-sigma)*s≠0)
    (hrho : rho*(2*(1-sigma)*s)=(1-(3/5:ℝ))*(2*kappa+3)-2*(1-sigma)*s)
    (hnr : ∀ n : ℕ, rho≠(n:ℝ)+2) (hcert : PolynomialCertificate sigma kappa s) :
    ∃ f u : ℝ → ℝ, ∃ a : ℝ, 0<a ∧ a<5/6 ∧
      AnalyticAt ℝ f 0 ∧ f 0=1 ∧ deriv f 0= -s/500 ∧
      (∀ᶠ t in 𝓝 (0:ℝ), SourceEuler.residual sigma kappa (3/5) (1/500) t (f t) (deriv f t)=0) ∧
      u a=f a ∧ ContinuousOn u (Icc a (5/6)) ∧
      (∀ t ∈ Icc a (5/6),
        (EulerPolynomial.barrier (SonicJet.jet f) (-1/1000)).eval t≤u t ∧
        u t≤(EulerPolynomial.barrier (SonicJet.jet f) (1/1000)).eval t) ∧
…

Mentions: OAI.SepticProfile.sigma, OAI.SepticProfile.kappa, OAI.SepticProfile.SonicContinuation.PolynomialCertificate, OAI.SepticProfile.SourceEuler.residual, OAI.SepticProfile.EulerPolynomial.barrier, OAI.SepticProfile.SonicJet.jet