Genuine time-continuous transport operators at the H¹→L² metric-energy level.

@[instance_reducible]

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

A named local normed-group instance for the actual Sobolev scale.

Equations

• EulerTransportL2Time.transportL2Group period q = inferInstance

@[instance_reducible]

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

A named local real normed-space instance for the actual Sobolev scale.

Equations

• EulerTransportL2Time.transportL2Space period q = inferInstance

noncomputable def EulerTransportL2Time.transportL2Bilinear (period : ℝ) [Fact (0 < period)] {q : ℕ} (hq : 3 ≤ q) (κ : ℝ) (m : EulerLiftedGradientSpace.Vector3) : ↥(EulerCylinderSobolevSpace.SobolevSpace period q) →L[ℝ] ↥(EulerCylinderSobolevSpace.SobolevSpace period 1) →L[ℝ] ↥(EulerLiftedGradientSpace.LiftL2 period)

Actual lifted transport as a bounded bilinear map Hq×H¹→L² for q≥3.

Equations

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

theorem EulerTransportL2Time.transportL2Bilinear_apply (period : ℝ) [Fact (0 < period)] {q : ℕ} (hq : 3 ≤ q) (κ : ℝ) (m : EulerLiftedGradientSpace.Vector3) (z : ↥(EulerCylinderSobolevSpace.SobolevSpace period q)) : (transportL2Bilinear period hq κ m) z = EulerSobolevMetricTransport.transportOperator period hq κ m z

This actual bilinear map is exactly the transport operator used in the proved metric cancellation.

noncomputable def EulerTransportL2Time.transportL2Path (period : ℝ) [Fact (0 < period)] {q : ℕ} (hq : 3 ≤ q) (κ : ℝ) (m : EulerLiftedGradientSpace.Vector3) (T : ℝ) (z : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period q))) : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period 1) →L[ℝ] ↥(EulerLiftedGradientSpace.LiftL2 period))

A continuous actual velocity determines the time-continuous H¹→L² transport operator path.

Equations

• EulerTransportL2Time.transportL2Path period hq κ m T z = (ContinuousLinearMap.compLeftContinuous ℝ (↑(Set.Icc 0 T)) (EulerTransportL2Time.transportL2Bilinear period hq κ m)) z

theorem EulerTransportL2Time.transportL2Path_apply (period : ℝ) [Fact (0 < period)] {q : ℕ} (hq : 3 ≤ q) (κ : ℝ) (m : EulerLiftedGradientSpace.Vector3) (T : ℝ) (z : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period q))) (t : ↑(Set.Icc 0 T)) : (transportL2Path period hq κ m T z) t = EulerSobolevMetricTransport.transportOperator period hq κ m (z t)

The actual transport path has exactly the pointwise metric-energy operator.