The actual asymmetric Sobolev transport map needed for the parabolic source upgrade.

@[instance_reducible]

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

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

Equations

• EulerAsymmetricTransport.asymmetricGroup period q = inferInstance

@[instance_reducible]

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

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

Equations

• EulerAsymmetricTransport.asymmetricSpace period q = inferInstance

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

Actual transport Hs×H^(s+1)→Hs; the coefficient velocity needs no extra derivative.

Equations

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

theorem EulerAsymmetricTransport.asymmetricTransport_apply (period : ℝ) [Fact (0 < period)] {s : ℕ} (hs : 6 ≤ s) (L : Fin 4 → EulerLiftedGradientSpace.Vector3 →L[ℝ] ℝ) (hL : ∀ (i : Fin 4), ‖L i‖ ≤ 1) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period s)) (v : ↥(EulerCylinderSobolevSpace.SobolevSpace period (s + 1))) : ((asymmetricTransport period hs L hL) u) v = ∑ i : Fin 4, EulerSobolevL2Product.productHq period hs (L i) ⋯ u ((EulerCylinderSobolevSpace.derivativeOperator period s i) v)

The literal scalar-times-derivative formula of asymmetric transport.

theorem EulerAsymmetricTransport.asymmetricTransport_eq (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))) : ((asymmetricTransport period hs L hL) ((EulerCylinderSobolevSpace.truncateOperator period s) u)) v = ((EulerSobolevTransport.transportBilinear period hs L hL) u) v

The asymmetric map agrees with the already constructed genuine transport on common inputs.

theorem EulerAsymmetricTransport.asymmetricTransport_eq_background (period : ℝ) [Fact (0 < period)] {s : ℕ} (hs : 6 ≤ s) (L : Fin 4 → EulerLiftedGradientSpace.Vector3 →L[ℝ] ℝ) (hL : ∀ (i : Fin 4), ‖L i‖ ≤ 1) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period s)) (v : ↥(EulerCylinderSobolevSpace.SobolevSpace period (s + 1))) : ((asymmetricTransport period hs L hL) u) v = EulerGevreyOrderZero.backgroundDrift period hs L hL v u

The background-drift expression is the same actual asymmetric transport operator.

theorem EulerAsymmetricTransport.asymmetricTransport_bound (period : ℝ) [Fact (0 < period)] {s : ℕ} (hs : 6 ≤ s) (L : Fin 4 → EulerLiftedGradientSpace.Vector3 →L[ℝ] ℝ) (hL : ∀ (i : Fin 4), ‖L i‖ ≤ 1) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period s)) (v : ↥(EulerCylinderSobolevSpace.SobolevSpace period (s + 1))) : ‖((asymmetricTransport period hs L hL) u) v‖ ≤ 4 * EulerSobolevL2Product.sobolevProductConstant period s * ‖u‖ * ‖v‖

The genuine asymmetric transport bound needed to multiply a bounded Hs path with an L²-time H^(s+1) path.

theorem EulerAsymmetricTransport.asymmetricTransport_norm (period : ℝ) [Fact (0 < period)] {s : ℕ} (hs : 6 ≤ s) (L : Fin 4 → EulerLiftedGradientSpace.Vector3 →L[ℝ] ℝ) (hL : ∀ (i : Fin 4), ‖L i‖ ≤ 1) : ‖asymmetricTransport period hs L hL‖ ≤ 4 * EulerSobolevL2Product.sobolevProductConstant period s

Operator-norm control of the actual asymmetric transport bilinear map.