OAI/Geometry/SurfaceImmersion/Correction/JetPolynomialLinear.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ClosedSurfaceR4.JetPolynomial.Expression.liftOperator line 12
2. lemma OAI.ClosedSurfaceR4.JetPolynomial.Expression.smoothCoeffs_liftOperator line 15
3. lemma OAI.ClosedSurfaceR4.JetPolynomial.Expression.order_liftOperator line 21
4. lemma OAI.ClosedSurfaceR4.JetPolynomial.Expression.loss_liftOperator line 24
5. lemma OAI.ClosedSurfaceR4.JetPolynomial.Expression.eval_liftOperator line 28

   Source documentation

   This uses actual operator linearity, not an assumed polynomial representation.

   lemma eval_liftOperator {O : Set LowJet} (hO : IsOpen O)
       (T : LowJet → (ℝ → ℝ) → ℝ → ℝ)
       (hadd : ∀ Q ∈ O, ∀ f g : ℝ → ℝ, Continuous f → Continuous g → ∀ t,
         T Q (fun s => f s + g s) t = T Q f t + T Q g t)
       (hsmul : ∀ Q ∈ O, ∀ a : ℝ, ∀ f : ℝ → ℝ, ∀ t,
         T Q (fun s => a * f s) t = a * T Q f t)
       {e : Expression} (he : e.SmoothCoeffs O) (G : Base → Space)
       {p : Base} (hp : lowJet G p ∈ O) (t : ℝ) :
       (e.liftOperator T).eval G (p, t) = T (lowJet G p) (fun s => e.eval G (p, s)) t := by
   …

   Mentions: OAI.ClosedSurfaceR4.JetPolynomial.LowJet, OAI.ClosedSurfaceR4.JetPolynomial.Expression, OAI.ClosedSurfaceR4.JetPolynomial.Base, OAI.ClosedSurfaceR4.JetPolynomial.Space, OAI.ClosedSurfaceR4.JetPolynomial.lowJet, OAI.ClosedSurfaceR4.JetPolynomial.Expression.eval