The genuine external transport commutator as a bounded bilinear Sobolev operator.

@[instance_reducible]

noncomputable def EulerSobolevTransportCommutator.commutatorGroup (period : ℝ) [Fact (0 < period)] (q : ℕ) : NormedAddCommGroup ↥(EulerCylinderSobolevSpace.SobolevSpace period q)

Cache the standard NormedAddCommGroup (SobolevSpace period q) instance to shorten typeclass synthesis.

Equations

• EulerSobolevTransportCommutator.commutatorGroup period q = inferInstance

@[instance_reducible]

noncomputable def EulerSobolevTransportCommutator.commutatorSpace (period : ℝ) [Fact (0 < period)] (q : ℕ) : NormedSpace ℝ ↥(EulerCylinderSobolevSpace.SobolevSpace period q)

Cache the standard NormedSpace ℝ (SobolevSpace period q) instance to shorten typeclass synthesis.

Equations

• EulerSobolevTransportCommutator.commutatorSpace period q = inferInstance

@[instance_reducible]

noncomputable def EulerSobolevTransportCommutator.commutatorBilinearGroup (period : ℝ) [Fact (0 < period)] (q r : ℕ) : SeminormedAddCommGroup (↥(EulerCylinderSobolevSpace.SobolevSpace period q) →L[ℝ] ↥(EulerCylinderSobolevSpace.SobolevSpace period q) →L[ℝ] ↥(EulerCylinderSobolevSpace.SobolevSpace period r))

Cache the standard SeminormedAddCommGroup (SobolevSpace period q →L[ℝ] SobolevSpace period q →L[ℝ] SobolevSpace period r) instance to shorten typeclass synthesis.

Equations

• EulerSobolevTransportCommutator.commutatorBilinearGroup period q r = inferInstance

noncomputable def EulerSobolevTransportCommutator.externalCommutator (period : ℝ) [Fact (0 < period)] {s : ℕ} (hs : 6 ≤ s) (n : ℕ) (w : Fin n → Fin 4) (hn : n + 6 ≤ s) (L : Fin 4 → EulerLiftedGradientSpace.Vector3 →L[ℝ] ℝ) (hL : ∀ (i : Fin 4), ‖L i‖ ≤ 1) : ↥(EulerCylinderSobolevSpace.SobolevSpace period (s + 1)) →L[ℝ] ↥(EulerCylinderSobolevSpace.SobolevSpace period (s + 1)) →L[ℝ] ↥(EulerCylinderSobolevSpace.SobolevSpace period 6)

The actual difference D^w(z·D e)−z·D(D^w e), with all operands on their genuine Sobolev domains.

Equations

• One or more equations did not get rendered due to their size.

theorem EulerSobolevTransportCommutator.externalCommutator_apply (period : ℝ) [Fact (0 < period)] {s : ℕ} (hs : 6 ≤ s) (n : ℕ) (w : Fin n → Fin 4) (hn : n + 6 ≤ s) (L : Fin 4 → EulerLiftedGradientSpace.Vector3 →L[ℝ] ℝ) (hL : ∀ (i : Fin 4), ‖L i‖ ≤ 1) (u v : ↥(EulerCylinderSobolevSpace.SobolevSpace period (s + 1))) : ((externalCommutator period hs n w hn L hL) u) v = (EulerSobolevWordLevel.wordAtLevel period 6 n w hn) (((EulerSobolevTransport.transportBilinear period hs L hL) u) v) - ((EulerSobolevTransport.transportBilinear period externalCommutator._proof_1 L hL) ((EulerCylinderSobolevSpace.restrictOperator period ⋯) u)) ((EulerSobolevWordLevel.wordAtLevel period 7 n w ⋯) v)

Explicit actual Sobolev operands of the transport commutator.

theorem EulerSobolevTransportCommutator.transportField_smooth (period : ℝ) (b : EulerLiftedGradientSpace.LiftDomain period → EulerSobolev.Domain 4) (g : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3) (hb : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period b x)) (hg : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period g x)) (x : EulerLiftedGradientSpace.LiftDomain period) : ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period (EulerH6Nonlinear.transportField period 3 b g) x)

Classical transport of smooth cylinder fields is smooth.

theorem EulerSobolevTransportCommutator.transport_ae_velocityMap (period : ℝ) [Fact (0 < period)] {s : ℕ} (hs : 6 ≤ s) (L : Fin 4 → EulerLiftedGradientSpace.Vector3 →L[ℝ] ℝ) (hL : ∀ (i : Fin 4), ‖L i‖ ≤ 1) (u v : ↥(EulerCylinderSobolevSpace.SobolevSpace period (s + 1))) (f g : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3) (hu : ↑↑(EulerCylinderSobolevSpace.value period u) =ᵐ[EulerLiftedGradientSpace.liftMeasure period] f) (hv : ↑↑(EulerCylinderSobolevSpace.value period v) =ᵐ[EulerLiftedGradientSpace.liftMeasure period] g) (hg : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period g x)) : ↑↑(EulerCylinderSobolevSpace.value period (((EulerSobolevTransport.transportBilinear period hs L hL) u) v)) =ᵐ[EulerLiftedGradientSpace.liftMeasure period] EulerH6Nonlinear.transportField period 3 (⇑(EulerFunctionalVelocity.velocityMap L) ∘ f) g

The actual Sobolev transport is the classical transport by its assembled four-dimensional velocity.

theorem EulerSobolevTransportCommutator.externalCommutator_ae (period : ℝ) [Fact (0 < period)] {s : ℕ} (hs : 6 ≤ s) (n : ℕ) (w : Fin n → Fin 4) (hn : n + 6 ≤ s) (L : Fin 4 → EulerLiftedGradientSpace.Vector3 →L[ℝ] ℝ) (hL : ∀ (i : Fin 4), ‖L i‖ ≤ 1) (u v : ↥(EulerCylinderSobolevSpace.SobolevSpace period (s + 1))) (f g : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3) (hu : ↑↑(EulerCylinderSobolevSpace.value period u) =ᵐ[EulerLiftedGradientSpace.liftMeasure period] f) (hv : ↑↑(EulerCylinderSobolevSpace.value period v) =ᵐ[EulerLiftedGradientSpace.liftMeasure period] g) (hf : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period f x)) (hg : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period g x)) : ↑↑(EulerCylinderSobolevSpace.value period (((externalCommutator period hs n w hn L hL) u) v)) =ᵐ[EulerLiftedGradientSpace.liftMeasure period] EulerExternalTransportCommutator.transportCommutator period w (⇑(EulerFunctionalVelocity.velocityMap L) ∘ f) g

On genuine smooth representatives the bounded Sobolev commutator is exactly the classical derivative commutator.

theorem EulerSobolevTransportCommutator.transportCommutator_smooth (period : ℝ) {n : ℕ} (w : Fin n → Fin 4) (b : EulerLiftedGradientSpace.LiftDomain period → EulerSobolev.Domain 4) (g : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3) (hb : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period b x)) (hg : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period g x)) (x : EulerLiftedGradientSpace.LiftDomain period) : ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period (EulerExternalTransportCommutator.transportCommutator period w b g) x)

The classical external transport commutator is smooth for smooth fields.

theorem EulerSobolevTransportCommutator.externalCommutator_sumNorm (period : ℝ) [Fact (0 < period)] {s : ℕ} (hs : 6 ≤ s) (n : ℕ) (w : Fin n → Fin 4) (hn : n + 6 ≤ s) (L : Fin 4 → EulerLiftedGradientSpace.Vector3 →L[ℝ] ℝ) (hL : ∀ (i : Fin 4), ‖L i‖ ≤ 1) (u v : ↥(EulerCylinderSobolevSpace.SobolevSpace period (s + 1))) (f g : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3) (hu : ↑↑(EulerCylinderSobolevSpace.value period u) =ᵐ[EulerLiftedGradientSpace.liftMeasure period] f) (hv : ↑↑(EulerCylinderSobolevSpace.value period v) =ᵐ[EulerLiftedGradientSpace.liftMeasure period] g) (hf : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period f x)) (hg : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period g x)) : EulerCylinderSobolevSpace.sumNorm period (((externalCommutator period hs n w hn L hL) u) v) = EulerCylinderSobolev.liftSobolevNorm period 6 (EulerExternalTransportCommutator.transportCommutator period w (⇑(EulerFunctionalVelocity.velocityMap L) ∘ f) g)

The actual Sobolev commutator norm equals the source's classical H⁶ norm whenever smooth representatives are available.