ParametricJets.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

def OAI.SepticProfile.ParametricJets.residualP line 14
Source documentation
The literal normalized source polynomial residual, expanded about z=1.
```
def residualP (sigma kappa c : K) (u : Polynomial K) : Polynomial K :=
…
```
Mentions: OAI.SepticProfile.sigma, OAI.SepticProfile.kappa
theorem OAI.SepticProfile.ParametricJets.coe_residualP line 18
theorem OAI.SepticProfile.ParametricJets.coeff_residual_one line 28
theorem OAI.SepticProfile.ParametricJets.constantCoeff_residual line 41
theorem OAI.SepticProfile.ParametricJets.exists_finite_jet line 51
Source documentation
Construct all required finite sonic jets at a nonresonant weak slope. There is no assumed formal series. The zero multiplier at a resonance is explicitly excluded; this is why the resonant parameter cannot be used as a selected analytic profile parameter.
```
 theorem exists_finite_jet (sigma kappa c s : K)
    (hs : 2*(1-sigma)*s^2-(1-c)*(2*kappa+3)*s+3*(1-c)=0)
    (N : ℕ)
    (hne : ∀ n < N, IsUnit ((1-c)*(2*kappa+3)-2*(1-sigma)*s*(n+3))) :
    ∃ p : Polynomial K, p.coeff 0=1 ∧ p.coeff 1=s ∧
      ∀ i ≤ N+1, (residualP sigma kappa c p).coeff i=0 := by
…
```
Mentions: OAI.SepticProfile.sigma, OAI.SepticProfile.kappa, OAI.SepticProfile.ParametricJets.residualP
theorem OAI.SepticProfile.ParametricJets.exists_finite_jet_divisible line 109