The actual lifted velocity retains the small normal component in its coefficient estimates. No division by the packet amplitude is used.

The four-dimensional transport velocity associated with a lifted solenoidal field has zero ordinary trace on the real covering space.

noncomputable def EulerLiftedTransportTrace.transportLinear (κ : ℝ) (m : EulerLiftedGradientSpace.Vector3) : EulerLiftedGradientSpace.Vector3 →L[ℝ] EulerLiftedGradientSpace.LiftTangent

Transport linear, given by (κ • ContinuousLinearMap.id ℝ Vector3).prod (toDual ℝ Vector3 m).

Equations

• EulerLiftedTransportTrace.transportLinear κ m = (κ • ContinuousLinearMap.id ℝ EulerLiftedGradientSpace.Vector3).prod ((InnerProductSpace.toDual ℝ EulerLiftedGradientSpace.Vector3) m)

@[simp]

theorem EulerLiftedTransportTrace.transportLinear_apply (κ : ℝ) (m v : EulerLiftedGradientSpace.Vector3) : (transportLinear κ m) v = EulerMetricTransport.transportDirection κ m v

theorem EulerLiftedTransportTrace.transportLinear_single (κ : ℝ) (m : EulerLiftedGradientSpace.Vector3) (i : Fin 3) : (transportLinear κ m) (EuclideanSpace.single i 1) = EulerMetricTransport.coordinateDirection κ m i

theorem EulerLiftedTransportTrace.trace_transportLinear (κ : ℝ) (m : EulerLiftedGradientSpace.Vector3) (L : EulerLiftedGradientSpace.LiftTangent →L[ℝ] EulerLiftedGradientSpace.Vector3) : (LinearMap.trace ℝ EulerLiftedGradientSpace.LiftTangent) ↑(transportLinear κ m ∘SL L) = ∑ i : Fin 3, (L (EulerMetricTransport.coordinateDirection κ m i)).ofLp i

noncomputable def EulerLiftedTransportTrace.coverVelocity (P κ : ℝ) (m : EulerLiftedGradientSpace.Vector3) (g : EulerLiftedGradientSpace.LiftDomain P → EulerLiftedGradientSpace.Vector3) (z : EulerLiftedGradientSpace.LiftTangent) : EulerLiftedGradientSpace.LiftTangent

Cover velocity, given by transportDirection κ m (g (coveringMap P z)).

Equations

• EulerLiftedTransportTrace.coverVelocity P κ m g z = EulerMetricTransport.transportDirection κ m (g (EulerLiftedGradientSpace.coveringMap P z))

theorem EulerLiftedTransportTrace.coverVelocity_trace (P κ : ℝ) (m : EulerLiftedGradientSpace.Vector3) (g : EulerLiftedGradientSpace.LiftDomain P → EulerLiftedGradientSpace.Vector3) (hg : ∀ (q : EulerLiftedGradientSpace.LiftDomain P), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift P g q)) (z : EulerLiftedGradientSpace.LiftTangent) : (LinearMap.trace ℝ EulerLiftedGradientSpace.LiftTangent) ↑(fderiv ℝ (coverVelocity P κ m g) z) = ∑ i : Fin 3, (EulerTransportDerivatives.fieldDerivative P (EulerMetricTransport.coordinateDirection κ m i) g (EulerLiftedGradientSpace.coveringMap P z)).ofLp i

theorem EulerLiftedTransportTrace.coverVelocity_trace_zero (P κ : ℝ) (m : EulerLiftedGradientSpace.Vector3) (g : EulerLiftedGradientSpace.LiftDomain P → EulerLiftedGradientSpace.Vector3) [Fact (0 < P)] (u : ↥(EulerLiftedGradientSpace.LiftL2 P)) (hu : u ∈ EulerLiftedGradientSpace.divergenceFreeSpace P κ m) (hrep : ↑↑u =ᵐ[EulerLiftedGradientSpace.liftMeasure P] g) (hg : ∀ (q : EulerLiftedGradientSpace.LiftDomain P), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift P g q)) (z : EulerLiftedGradientSpace.LiftTangent) : (LinearMap.trace ℝ EulerLiftedGradientSpace.LiftTangent) ↑(fderiv ℝ (coverVelocity P κ m g) z) = 0

noncomputable def EulerLiftedSmoothTimeField.angularInjection : EulerSmoothLimit.Space →L[ℝ] EulerLiftedGradientSpace.LiftTangent

Angular injection, given by (ContinuousLinearMap.inr ℝ Space ℝ).comp scalarProject.

Equations

• EulerLiftedSmoothTimeField.angularInjection = ContinuousLinearMap.inr ℝ EulerSmoothLimit.Space ℝ ∘SL EulerCylinderScalarPrimitive.scalarProject

theorem EulerLiftedSmoothTimeField.angularInjection_norm : ‖angularInjection‖ ≤ 1

theorem EulerLiftedSmoothTimeField.spatialInjection_norm : ‖ContinuousLinearMap.inl ℝ EulerSmoothLimit.Space ℝ‖ ≤ 1

theorem EulerLiftedSmoothTimeField.transportLinear_split (κ : ℝ) (m : EulerSmoothLimit.Space) : EulerLiftedTransportTrace.transportLinear κ m = κ • ContinuousLinearMap.inl ℝ EulerSmoothLimit.Space ℝ + angularInjection ∘SL EulerPacketCylinderField.normalComponentMap m

theorem EulerLiftedSmoothTimeField.transport_tensor_norm {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (κ : ℝ) (m : EulerSmoothLimit.Space) {n : ℕ} (A : E [×n]→L[ℝ] EulerSmoothLimit.Space) : ‖(EulerLiftedTransportTrace.transportLinear κ m).compContinuousMultilinearMap A‖ ≤ |κ| * ‖A‖ + ‖(EulerPacketCylinderField.normalComponentMap m).compContinuousMultilinearMap A‖

@[instance_reducible]

noncomputable def EulerLiftedSmoothTimeField.instLiftedSmoothTimeField1 {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (n : ℕ) : NormedAddCommGroup (E [×n]→L[ℝ] EulerSmoothLimit.Space)

Cache the standard NormedAddCommGroup (E [×n]→L[ℝ] Space) instance to shorten typeclass synthesis.

Equations

• EulerLiftedSmoothTimeField.instLiftedSmoothTimeField1 n = inferInstance

@[instance_reducible]

noncomputable def EulerLiftedSmoothTimeField.instLiftedSmoothTimeField2 {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (n : ℕ) : NormedSpace ℝ (E [×n]→L[ℝ] EulerSmoothLimit.Space)

Cache the standard NormedSpace ℝ (E [×n]→L[ℝ] Space) instance to shorten typeclass synthesis.

Equations

• EulerLiftedSmoothTimeField.instLiftedSmoothTimeField2 n = inferInstance

@[instance_reducible]

noncomputable def EulerLiftedSmoothTimeField.instLiftedSmoothTimeField3 {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (n : ℕ) : NormedAddCommGroup (E [×n]→L[ℝ] EulerLiftedGradientSpace.LiftTangent)

Cache the standard NormedAddCommGroup (E [×n]→L[ℝ] LiftTangent) instance to shorten typeclass synthesis.

Equations

• EulerLiftedSmoothTimeField.instLiftedSmoothTimeField3 n = inferInstance

@[instance_reducible]

noncomputable def EulerLiftedSmoothTimeField.instLiftedSmoothTimeField4 {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (n : ℕ) : NormedSpace ℝ (E [×n]→L[ℝ] EulerLiftedGradientSpace.LiftTangent)

Cache the standard NormedSpace ℝ (E [×n]→L[ℝ] LiftTangent) instance to shorten typeclass synthesis.

Equations

• EulerLiftedSmoothTimeField.instLiftedSmoothTimeField4 n = inferInstance

@[instance_reducible]

noncomputable def EulerLiftedSmoothTimeField.instLiftedSmoothTimeField5 {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (n : ℕ) : NormedAddCommGroup (BoundedContinuousFunction E (E [×n]→L[ℝ] EulerSmoothLimit.Space))

Cache the standard NormedAddCommGroup (E →ᵇ (E [×n]→L[ℝ] Space)) instance to shorten typeclass synthesis.

Equations

• EulerLiftedSmoothTimeField.instLiftedSmoothTimeField5 n = inferInstance

@[instance_reducible]

noncomputable def EulerLiftedSmoothTimeField.instLiftedSmoothTimeField6 {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (n : ℕ) : NormedSpace ℝ (BoundedContinuousFunction E (E [×n]→L[ℝ] EulerSmoothLimit.Space))

Cache the standard NormedSpace ℝ (E →ᵇ (E [×n]→L[ℝ] Space)) instance to shorten typeclass synthesis.

Equations

• EulerLiftedSmoothTimeField.instLiftedSmoothTimeField6 n = inferInstance

@[instance_reducible]

noncomputable def EulerLiftedSmoothTimeField.instLiftedSmoothTimeField7 {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (n : ℕ) : NormedAddCommGroup (BoundedContinuousFunction E (E [×n]→L[ℝ] EulerLiftedGradientSpace.LiftTangent))

Cache the standard NormedAddCommGroup (E →ᵇ (E [×n]→L[ℝ] LiftTangent)) instance to shorten typeclass synthesis.

Equations

• EulerLiftedSmoothTimeField.instLiftedSmoothTimeField7 n = inferInstance

@[instance_reducible]

noncomputable def EulerLiftedSmoothTimeField.instLiftedSmoothTimeField8 {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (n : ℕ) : NormedSpace ℝ (BoundedContinuousFunction E (E [×n]→L[ℝ] EulerLiftedGradientSpace.LiftTangent))

Cache the standard NormedSpace ℝ (E →ᵇ (E [×n]→L[ℝ] LiftTangent)) instance to shorten typeclass synthesis.

Equations

• EulerLiftedSmoothTimeField.instLiftedSmoothTimeField8 n = inferInstance

noncomputable def EulerLiftedSmoothTimeField.lift {K E : Type} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup E] [NormedSpace ℝ E] (A : SmoothTimeField K E EulerSmoothLimit.Space) (κ : ℝ) (m : EulerSmoothLimit.Space) : SmoothTimeField K E EulerLiftedGradientSpace.LiftTangent

Lift, given by A.map (transportLinear κ m).

Equations

• EulerLiftedSmoothTimeField.lift A κ m = SmoothTimeField.map (EulerLiftedTransportTrace.transportLinear κ m) A

@[simp]

theorem EulerLiftedSmoothTimeField.lift_apply {K E : Type} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup E] [NormedSpace ℝ E] (A : SmoothTimeField K E EulerSmoothLimit.Space) (κ : ℝ) (m : EulerSmoothLimit.Space) (t : K) (x : E) : ((lift A κ m).field t) x = (κ • (A.field t) x, inner ℝ m ((A.field t) x))

theorem EulerLiftedSmoothTimeField.lift_jet_norm_le {K E : Type} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup E] [NormedSpace ℝ E] (A : SmoothTimeField K E EulerSmoothLimit.Space) (κ : ℝ) (m : EulerSmoothLimit.Space) (n : ℕ) : ‖(lift A κ m).jet n‖ ≤ |κ| * ‖A.jet n‖ + ‖(SmoothTimeField.map (EulerPacketCylinderField.normalComponentMap m) A).jet n‖

theorem EulerLiftedSmoothTimeField.lift_jet_norm_le_full {K E : Type} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup E] [NormedSpace ℝ E] (A : SmoothTimeField K E EulerSmoothLimit.Space) (κ : ℝ) (m : EulerSmoothLimit.Space) (n : ℕ) : ‖(lift A κ m).jet n‖ ≤ (|κ| + ‖m‖) * ‖A.jet n‖