OAI/MathematicalPhysics/Transonic/Shooting/ContinuousJets.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SepticProfile.ParametricJets.prefP line 13
2. def OAI.SepticProfile.ParametricJets.denQuotP line 14
3. def OAI.SepticProfile.ParametricJets.transP line 15
4. def OAI.SepticProfile.ParametricJets.linP line 17
5. theorem OAI.SepticProfile.ParametricJets.split_polynomial line 21
6. theorem OAI.SepticProfile.ParametricJets.coeff_denQuotP line 31
7. theorem OAI.SepticProfile.ParametricJets.coeff_linP line 38
8. theorem OAI.SepticProfile.ParametricJets.split_linearization line 48
9. lemma OAI.SepticProfile.ParametricJets.isUnit_continuous line 66

   Source documentation

   Nowhere vanishing continuous scalar coefficients are units in the exact coefficient ring. This avoids choosing unrelated discontinuous finite jets.

   lemma isUnit_continuous {f : C(A,ℝ)} (h : ∀ a, f a ≠ 0) : IsUnit f := by
   …

10. def OAI.SepticProfile.ParametricJets.specialize line 76
11. lemma OAI.SepticProfile.ParametricJets.coeff_specialize line 79
12. lemma OAI.SepticProfile.ParametricJets.specialize_C line 83
13. lemma OAI.SepticProfile.ParametricJets.specialize_derivative line 86
14. lemma OAI.SepticProfile.ParametricJets.specialize_residual line 90
15. lemma OAI.SepticProfile.ParametricJets.continuous_aeval_specialize line 95
16. theorem OAI.SepticProfile.ParametricJets.exists_continuous_jet line 113

    Source documentation

    A single finite jet over the ring of continuous parameter functions yields all members of the family, with the exact source residual divisibility.

    theorem exists_continuous_jet (sigma kappa c s rho : C(A,ℝ))
        (hs : ∀ a, 2*(1-sigma a)*(s a)^2-(1-c a)*(2*kappa a+3)*s a+3*(1-c a)=0)
        (hd : ∀ a, 2*(1-sigma a)*s a ≠ 0)
        (hrho : ∀ a, rho a*(2*(1-sigma a)*s a)=
          (1-c a)*(2*kappa a+3)-2*(1-sigma a)*s a)
        (hnr : ∀ a (n : ℕ), rho a ≠ (n:ℝ)+2) (m : ℕ) :
        ∃ p p1 S E : Polynomial C(A,ℝ),
          p.coeff 0=1 ∧ p.coeff 1=s ∧ p=1+X*p1 ∧ p1.coeff 0=s ∧
          residualP sigma kappa c p=X^(m+3)*S ∧
          C rho*denQuotP sigma p1+linP sigma kappa c p=X*E := by
    …

    Mentions: OAI.SepticProfile.sigma, OAI.SepticProfile.kappa, OAI.SepticProfile.ParametricJets.residualP, OAI.SepticProfile.ParametricJets.denQuotP, OAI.SepticProfile.ParametricJets.linP