CoordinatePolynomialPullback.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

The coordinate pullback of a finite jet polynomial, with the low-jet substitution and inverse differential proved from the actual local inverse. No compatibility of the polynomial values is assumed.

def OAI.ClosedSurfaceR4.JetPolynomial.coordinateLowJetSubstitution line 15
lemma OAI.ClosedSurfaceR4.JetPolynomial.coordinateLowJetSubstitution_smooth line 18
lemma OAI.ClosedSurfaceR4.JetPolynomial.inverse_differential_of_local_inverse line 24
def OAI.ClosedSurfaceR4.JetPolynomial.Expression.localCoordinatePullback line 37
Source documentation
Transport through a smooth local inverse, including the coefficient dependence on all positional order-two jets.
```
def localCoordinatePullback (e : Expression) (T S : Base → Base) : Expression :=
…
```
Mentions: OAI.ClosedSurfaceR4.JetPolynomial.Expression, OAI.ClosedSurfaceR4.JetPolynomial.Base
lemma OAI.ClosedSurfaceR4.JetPolynomial.Expression.localCoordinatePullback_smooth line 40
lemma OAI.ClosedSurfaceR4.JetPolynomial.Expression.localCoordinatePullback_eval line 46

lemma OAI.ClosedSurfaceR4.JetPolynomial.Expression.localCoordinatePullback_eval_germ line 66

Source documentation

At a boundary of a support it is enough to know the actual map relation as a germ at the point under consideration.

lemma localCoordinatePullback_eval_germ {T S : Base → Base}
    (hT : ContDiff ℝ ∞ T) (hS : ContDiff ℝ ∞ S)
    {U : Set Base} (hU : IsOpen U)
    (hST : ∀ x ∈ U, S (T x) = x)
    (hTS : ∀ x ∈ U, (T ∘ S) =ᶠ[𝓝 (T x)] id)
    {G H : Base → Space} (hG : ContDiff ℝ ∞ G) (hH : ContDiff ℝ ∞ H)
    {x : Base} (hx : x ∈ U) (hrel : H =ᶠ[𝓝 x] (G ∘ T))
    (e : Expression) (t : ℝ) :
    (e.localCoordinatePullback T S).eval H (x,t) = e.eval G (T x,t) := by
…

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