CoordinateTensorPullback.lean`

16 declarations, 0 contain sorry, 0 declared as axioms

Pullback of finite tensor expressions under fixed coordinate changes. The Jacobian factors, coefficient substitution, and higher jet atoms are all constructed, so the evaluation identity assumes no tensor covariance.

abbrev OAI.ClosedSurfaceR4.JetPolynomial.TensorExpression line 16
def OAI.ClosedSurfaceR4.JetPolynomial.tensorCoordinateDerivative line 20
Source documentation
The derivative of the coordinate map in the real pair coordinates used by the three-component tensor representation.
```
def tensorCoordinateDerivative (T : Base → Base) (x : Base) :
    SmallModes.Base →L[ℝ] SmallModes.Base :=
…
```
Mentions: OAI.ClosedSurfaceR4.JetPolynomial.Base, OAI.ClosedSurfaceR4.SmallModes.Base
def OAI.ClosedSurfaceR4.JetPolynomial.tensorCoordinatePullbackValue line 27
Source documentation
Covariant pullback of a symmetric tensor by the actual derivative.
```
def tensorCoordinatePullbackValue (T : Base → Base) (x : Base) :
    PhaseMean.Tensor →L[ℝ] PhaseMean.Tensor :=
…
```
Mentions: OAI.ClosedSurfaceR4.JetPolynomial.Base, OAI.ClosedSurfaceR4.PhaseMean.Tensor
def OAI.ClosedSurfaceR4.JetPolynomial.tensorCoordinateJacobian line 32
Source documentation
The three Jacobian coefficients of one pulled-back tensor component.
```
def tensorCoordinateJacobian (T : Base → Base) (k l : Fin 3) (x : Base) : ℝ :=
…
```
Mentions: OAI.ClosedSurfaceR4.JetPolynomial.Base
lemma OAI.ClosedSurfaceR4.JetPolynomial.tensorCoordinateJacobian_smooth line 37
lemma OAI.ClosedSurfaceR4.JetPolynomial.tensorCoordinateJacobian_sum line 46
def OAI.ClosedSurfaceR4.JetPolynomial.tensorJacobianCoefficient line 58
Source documentation
Store a Jacobian factor as an actual smooth positional coefficient.
```
def tensorJacobianCoefficient (T : Base → Base) (k l : Fin 3) : LowJet × ℝ → ℝ :=
…
```
Mentions: OAI.ClosedSurfaceR4.JetPolynomial.Base, OAI.ClosedSurfaceR4.JetPolynomial.LowJet
lemma OAI.ClosedSurfaceR4.JetPolynomial.tensorJacobianCoefficient_smooth line 61
def OAI.ClosedSurfaceR4.JetPolynomial.TensorExpression.eval line 68
Source documentation
Evaluation in the original coordinate chart.
```
def eval (E : TensorExpression) (G : Base → Space) (z : Base × ℝ) : PhaseMean.Tensor :=
…
```
Mentions: OAI.ClosedSurfaceR4.JetPolynomial.TensorExpression, OAI.ClosedSurfaceR4.JetPolynomial.Base, OAI.ClosedSurfaceR4.JetPolynomial.Space, OAI.ClosedSurfaceR4.PhaseMean.Tensor
def OAI.ClosedSurfaceR4.JetPolynomial.TensorExpression.coordinatePullback line 72
Source documentation
Pull back both the scalar jet expressions and their tensor basis.
```
def coordinatePullback (E : TensorExpression) (T S : Base → Base) : TensorExpression :=
…
```
Mentions: OAI.ClosedSurfaceR4.JetPolynomial.TensorExpression, OAI.ClosedSurfaceR4.JetPolynomial.Base
lemma OAI.ClosedSurfaceR4.JetPolynomial.TensorExpression.coordinatePullback_smooth line 76

theorem OAI.ClosedSurfaceR4.JetPolynomial.TensorExpression.coordinatePullback_eval line 87

Source documentation

An exact tensor evaluation identity from genuine local inverse germs and the actual map relation.

theorem coordinatePullback_eval {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)
    (hrel : ∀ x ∈ U, H x = G (T x))
    (E : TensorExpression) (t : ℝ) {x : Base} (hx : x ∈ U) :
    eval (coordinatePullback E T S) H (x,t) =
      tensorCoordinatePullbackValue T x (eval E G (T x,t)) := by
…

Mentions: OAI.ClosedSurfaceR4.JetPolynomial.Base, OAI.ClosedSurfaceR4.JetPolynomial.Space, OAI.ClosedSurfaceR4.JetPolynomial.TensorExpression, OAI.ClosedSurfaceR4.JetPolynomial.TensorExpression.eval, OAI.ClosedSurfaceR4.JetPolynomial.TensorExpression.coordinatePullback, OAI.ClosedSurfaceR4.JetPolynomial.tensorCoordinatePullbackValue

def OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.tensorPolynomialCoordinatePullback line 113
Source documentation
Apply the tensor coordinate transformation coefficient by coefficient to a finite polynomial in the perturbation parameter.
```
def tensorPolynomialCoordinatePullback {n : ℕ} (P : Fin 3 → Fin n → Expression)
    (T S : Base → Base) : Fin 3 → Fin n → Expression :=
…
```
Mentions: OAI.ClosedSurfaceR4.JetPolynomial.Expression, OAI.ClosedSurfaceR4.JetPolynomial.Base
lemma OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.tensorPolynomialCoordinatePullback_smooth line 117
lemma OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.coordinatePolynomialValue_eq_tensor_sum line 124

theorem OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.tensorPolynomialCoordinatePullback_eval line 134

Source documentation

The three-component finite polynomial transforms covariantly under smooth coordinate changes.

theorem tensorPolynomialCoordinatePullback_eval {n : ℕ}
    (P : Fin 3 → Fin n → Expression) {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)
    (hrel : ∀ x ∈ U, H x = G (T x))
    (ε t : ℝ) {x : Base} (hx : x ∈ U) :
    coordinatePolynomialValue (tensorPolynomialCoordinatePullback P T S) ε H t
        (planeCoordinateIsometry x) =
      tensorCoordinatePullbackValue T x
…

Mentions: OAI.ClosedSurfaceR4.JetPolynomial.Expression, OAI.ClosedSurfaceR4.JetPolynomial.Base, OAI.ClosedSurfaceR4.JetPolynomial.Space, OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.coordinatePolynomialValue, OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.tensorPolynomialCoordinatePullback, OAI.ClosedSurfaceR4.JetPolynomial.planeCoordinateIsometry, OAI.ClosedSurfaceR4.JetPolynomial.tensorCoordinatePullbackValue