Actual one-derivative-losing nonlinear transport on the complete cylinder Sobolev spaces.

@[instance_reducible]

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

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

Equations

• EulerSobolevTransport.sobolevGroup period q = inferInstance

@[instance_reducible]

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

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

Equations

• EulerSobolevTransport.sobolevRealSpace period q = inferInstance

noncomputable def EulerSobolevTransport.transportBilinear (period : ℝ) [Fact (0 < period)] {q : ℕ} (hq : 6 ≤ q) (L : Fin 4 → EulerLiftedGradientSpace.Vector3 →L[ℝ] ℝ) (hL : ∀ (i : Fin 4), ‖L i‖ ≤ 1) : ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1)) →L[ℝ] ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1)) →L[ℝ] ↥(EulerCylinderSobolevSpace.SobolevSpace period q)

The genuine transport bilinear map, with one actual coordinate derivative on its second input.

Equations

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

theorem EulerSobolevTransport.transportBilinear_apply (period : ℝ) [Fact (0 < period)] {q : ℕ} (hq : 6 ≤ q) (L : Fin 4 → EulerLiftedGradientSpace.Vector3 →L[ℝ] ℝ) (hL : ∀ (i : Fin 4), ‖L i‖ ≤ 1) (u v : ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1))) : ((transportBilinear period hq L hL) u) v = ∑ i : Fin 4, EulerSobolevL2Product.productHq period hq (L i) ⋯ ((EulerCylinderSobolevSpace.truncateOperator period q) u) ((EulerCylinderSobolevSpace.derivativeOperator period q i) v)

Transport is the finite sum of the actual Sobolev products and strong coordinate derivatives.

theorem EulerSobolevTransport.transportBilinear_bound (period : ℝ) [Fact (0 < period)] {q : ℕ} (hq : 6 ≤ q) (L : Fin 4 → EulerLiftedGradientSpace.Vector3 →L[ℝ] ℝ) (hL : ∀ (i : Fin 4), ‖L i‖ ≤ 1) (u v : ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1))) : ‖((transportBilinear period hq L hL) u) v‖ ≤ 4 * EulerSobolevL2Product.sobolevProductConstant period q * ‖u‖ * ‖v‖

The actual transport loses exactly one derivative, with an explicit fixed-order constant.

theorem EulerSobolevTransport.transportBilinear_norm (period : ℝ) [Fact (0 < period)] {q : ℕ} (hq : 6 ≤ q) (L : Fin 4 → EulerLiftedGradientSpace.Vector3 →L[ℝ] ℝ) (hL : ∀ (i : Fin 4), ‖L i‖ ≤ 1) : ‖transportBilinear period hq L hL‖ ≤ 4 * EulerSobolevL2Product.sobolevProductConstant period q

The transport norm in the derivative-losing operator topology.

theorem EulerSobolevTransport.transportBilinear_value (period : ℝ) [Fact (0 < period)] {q : ℕ} (hq : 6 ≤ q) (L : Fin 4 → EulerLiftedGradientSpace.Vector3 →L[ℝ] ℝ) (hL : ∀ (i : Fin 4), ‖L i‖ ≤ 1) (u v : ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1))) : EulerCylinderSobolevSpace.value period (((transportBilinear period hq L hL) u) v) = ∑ i : Fin 4, EulerSobolevL2Product.scalarProduct period ⋯ (L i) ((EulerCylinderSobolevSpace.truncateOperator period q) u) (EulerCylinderSobolevSpace.value period ((EulerCylinderSobolevSpace.derivativeOperator period q i) v))

The genuine transport is represented by the literal sum of pointwise directional products.

theorem EulerSobolevTransport.transportBilinear_ae (period : ℝ) [Fact (0 < period)] {q : ℕ} (hq : 6 ≤ q) (L : Fin 4 → EulerLiftedGradientSpace.Vector3 →L[ℝ] ℝ) (hL : ∀ (i : Fin 4), ‖L i‖ ≤ 1) (u v : ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 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 (((transportBilinear period hq L hL) u) v)) =ᵐ[EulerLiftedGradientSpace.liftMeasure period] fun (x : EulerLiftedGradientSpace.LiftDomain period) => ∑ i : Fin 4, (L i) (f x) • EulerTransportDerivatives.fieldDerivative period (EulerCylinderSobolev.standardDirection i) g x

On smooth representatives the nonlinear transport is exactly the classical cylinder differential operator.