PolynomialAffineFamily.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Joint smoothness in position and a variation parameter for actual higher-jet polynomial expressions.

lemma OAI.ClosedSurfaceR4.JetPolynomial.jet_affine_joint_smooth line 14
lemma OAI.ClosedSurfaceR4.JetPolynomial.lowJet_affine_joint_smooth line 25
lemma OAI.ClosedSurfaceR4.JetPolynomial.MixedExpression.jet_varyBase_joint_smooth line 38
theorem OAI.ClosedSurfaceR4.JetPolynomial.MixedExpression.eval_varyBase_joint_smooth line 49
Source documentation
Global coefficient smoothness is obtained on the application compact set by Expression.exists_global_extension.
```
theorem eval_varyBase_joint_smooth {G : Fin 4 → Base → Space} {H : Base → Space}
    (hG : ∀ i, ContDiff ℝ ∞ (G i)) (hH : ContDiff ℝ ∞ H)
    {e : MixedExpression} (he : e.SmoothCoeffs Set.univ) (θ : ℝ) :
    ContDiff ℝ ∞ (fun z : Base × ℝ => e.eval (varyBase G H z.2) (z.1, θ)) := by
…
```
Mentions: OAI.ClosedSurfaceR4.JetPolynomial.Base, OAI.ClosedSurfaceR4.JetPolynomial.Space, OAI.ClosedSurfaceR4.JetPolynomial.MixedExpression, OAI.ClosedSurfaceR4.JetPolynomial.MixedExpression.varyBase