Actual directional differentiation of transport and coefficient multiplication. The commutator is derived by the chain rule and symmetry of second derivatives, rather than postulated as a recurrence on a norm sequence.

noncomputable def EulerTransportDerivatives.directionalDerivative {V : Type u_1} {W : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] (a : V) (f : V → W) (x : V) : W

The actual Fréchet directional derivative along a constant vector.

Equations

• EulerTransportDerivatives.directionalDerivative a f x = (fderiv ℝ f x) a

noncomputable def EulerTransportDerivatives.transport {V : Type u_1} {W : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] (b : V → V) (f : V → W) (x : V) : W

Differentiation of a field in the direction of a variable transport field.

Equations

• EulerTransportDerivatives.transport b f x = (fderiv ℝ f x) (b x)

theorem EulerTransportDerivatives.directionalDerivative_smooth {V : Type u_1} {W : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] (a : V) (f : V → W) (hf : ContDiff ℝ (↑⊤) f) : ContDiff ℝ (↑⊤) (directionalDerivative a f)

theorem EulerTransportDerivatives.transport_smooth {V : Type u_1} {W : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] (b : V → V) (f : V → W) (hb : ContDiff ℝ (↑⊤) b) (hf : ContDiff ℝ (↑⊤) f) : ContDiff ℝ (↑⊤) (transport b f)

theorem EulerTransportDerivatives.directional_transport_commutator {V : Type u_1} {W : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] (a : V) (b : V → V) (f : V → W) (hb : ContDiff ℝ (↑⊤) b) (hf : ContDiff ℝ (↑⊤) f) (x : V) : directionalDerivative a (transport b f) x = transport b (directionalDerivative a f) x + (fderiv ℝ f x) (directionalDerivative a b x)

theorem EulerTransportDerivatives.directional_transport_commutator_norm {V : Type u_1} {W : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] (a : V) (b : V → V) (f : V → W) (hb : ContDiff ℝ (↑⊤) b) (hf : ContDiff ℝ (↑⊤) f) (x : V) : ‖directionalDerivative a (transport b f) x - transport b (directionalDerivative a f) x‖ ≤ ‖fderiv ℝ f x‖ * ‖directionalDerivative a b x‖

noncomputable def EulerTransportDerivatives.fieldDerivative (period : ℝ) {W : Type u_1} [NormedAddCommGroup W] [NormedSpace ℝ W] (a : EulerLiftedGradientSpace.LiftTangent) (f : EulerLiftedGradientSpace.LiftDomain period → W) (x : EulerLiftedGradientSpace.LiftDomain period) : W

Directional differentiation in the cylinder covering coordinates.

Equations

• EulerTransportDerivatives.fieldDerivative period a f x = (fderiv ℝ (EulerMetricTransport.localFieldLift period f x) 0) a

noncomputable def EulerTransportDerivatives.fieldTransport (period : ℝ) {W : Type u_1} [NormedAddCommGroup W] [NormedSpace ℝ W] (b : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.LiftTangent) (f : EulerLiftedGradientSpace.LiftDomain period → W) (x : EulerLiftedGradientSpace.LiftDomain period) : W

The actual directional transport operator on a cylinder field.

Equations

• EulerTransportDerivatives.fieldTransport period b f x = (fderiv ℝ (EulerMetricTransport.localFieldLift period f x) 0) (b x)

theorem EulerTransportDerivatives.localFieldLift_shift (period : ℝ) {W : Type u_1} (f : EulerLiftedGradientSpace.LiftDomain period → W) (x : EulerLiftedGradientSpace.LiftDomain period) (h : EulerLiftedGradientSpace.LiftTangent) : EulerMetricTransport.localFieldLift period f (x.1 + h.1, x.2 + ↑h.2) = fun (u : EulerLiftedGradientSpace.LiftTangent) => EulerMetricTransport.localFieldLift period f x (h + u)

theorem EulerTransportDerivatives.fderiv_localFieldLift_shift (period : ℝ) {W : Type u_1} [NormedAddCommGroup W] [NormedSpace ℝ W] (f : EulerLiftedGradientSpace.LiftDomain period → W) (x : EulerLiftedGradientSpace.LiftDomain period) (h : EulerLiftedGradientSpace.LiftTangent) : fderiv ℝ (EulerMetricTransport.localFieldLift period f (x.1 + h.1, x.2 + ↑h.2)) 0 = fderiv ℝ (EulerMetricTransport.localFieldLift period f x) h

theorem EulerTransportDerivatives.localFieldLift_fieldDerivative (period : ℝ) {W : Type u_1} [NormedAddCommGroup W] [NormedSpace ℝ W] (a : EulerLiftedGradientSpace.LiftTangent) (f : EulerLiftedGradientSpace.LiftDomain period → W) (x : EulerLiftedGradientSpace.LiftDomain period) : EulerMetricTransport.localFieldLift period (fieldDerivative period a f) x = directionalDerivative a (EulerMetricTransport.localFieldLift period f x)

theorem EulerTransportDerivatives.localFieldLift_fieldTransport (period : ℝ) {W : Type u_1} [NormedAddCommGroup W] [NormedSpace ℝ W] (b : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.LiftTangent) (f : EulerLiftedGradientSpace.LiftDomain period → W) (x : EulerLiftedGradientSpace.LiftDomain period) : EulerMetricTransport.localFieldLift period (fieldTransport period b f) x = transport (EulerMetricTransport.localFieldLift period b x) (EulerMetricTransport.localFieldLift period f x)

theorem EulerTransportDerivatives.fieldDerivative_smooth (period : ℝ) {W : Type u_1} [NormedAddCommGroup W] [NormedSpace ℝ W] (a : EulerLiftedGradientSpace.LiftTangent) (f : EulerLiftedGradientSpace.LiftDomain period → W) (hf : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period f x)) (x : EulerLiftedGradientSpace.LiftDomain period) : ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period (fieldDerivative period a f) x)

theorem EulerTransportDerivatives.fieldTransport_smooth (period : ℝ) {W : Type u_1} [NormedAddCommGroup W] [NormedSpace ℝ W] (b : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.LiftTangent) (f : EulerLiftedGradientSpace.LiftDomain period → W) (hb : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period b x)) (hf : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period f x)) (x : EulerLiftedGradientSpace.LiftDomain period) : ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period (fieldTransport period b f) x)

theorem EulerTransportDerivatives.field_transport_commutator (period : ℝ) {W : Type u_1} [NormedAddCommGroup W] [NormedSpace ℝ W] (a : EulerLiftedGradientSpace.LiftTangent) (b : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.LiftTangent) (f : EulerLiftedGradientSpace.LiftDomain period → W) (hb : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period b x)) (hf : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period f x)) (x : EulerLiftedGradientSpace.LiftDomain period) : fieldDerivative period a (fieldTransport period b f) x = fieldTransport period b (fieldDerivative period a f) x + (fderiv ℝ (EulerMetricTransport.localFieldLift period f x) 0) (fieldDerivative period a b x)

theorem EulerTransportDerivatives.field_transport_commutator_norm (period : ℝ) {W : Type u_1} [NormedAddCommGroup W] [NormedSpace ℝ W] (a : EulerLiftedGradientSpace.LiftTangent) (b : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.LiftTangent) (f : EulerLiftedGradientSpace.LiftDomain period → W) (hb : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period b x)) (hf : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period f x)) (x : EulerLiftedGradientSpace.LiftDomain period) : ‖fieldDerivative period a (fieldTransport period b f) x - fieldTransport period b (fieldDerivative period a f) x‖ ≤ ‖fderiv ℝ (EulerMetricTransport.localFieldLift period f x) 0‖ * ‖fieldDerivative period a b x‖