An actual ordinary L² path with coherent Sobolev realizations has genuine smooth spatial representatives and continuous L² tensor jets. The unit-cylinder lift is only a realization in an already complete Sobolev space; the resulting ordinary field equals the prescribed L² path.

theorem EulerOrdinarySobolev.instOrdinarySobolevTower1 : Fact (0 < 1)

structure EulerOrdinarySobolev.SobolevTower (T : ℝ) : Type

Sobolev tower data, collecting field, realization, value_eq.

• field : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2)

  Underlying field of SobolevTower, of type C(Icc (0 : ℝ) T,EulerMeanSolenoidal.L2).

• realization (q : ℕ) : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace 1 q))

  Realization of SobolevTower, of type ∀ q, C(Icc (0 : ℝ) T,SobolevSpace 1 q).

• value_eq (q : ℕ) (t : ↑(Set.Icc 0 T)) : EulerCylinderSobolevSpace.value 1 ((self.realization q) t) = EulerMeanOrdinaryLift.ordinaryLift (self.field t)

noncomputable def EulerOrdinarySobolev.SobolevTower.cylinder {T : ℝ} (A : SobolevTower T) : EulerAllOrderCorrectionData.FieldTower 1 T

Cylinder, bundling field, realization, value_eq.

Equations

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

noncomputable def EulerOrdinarySobolev.SobolevTower.smoothField {T : ℝ} (A : SobolevTower T) (t : ↑(Set.Icc 0 T)) : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space

Smooth field, given by A.cylinder.zeroGraphField t.

Equations

• A.smoothField t = A.cylinder.zeroGraphField t

theorem EulerOrdinarySobolev.SobolevTower.smoothField_toLp {T : ℝ} (A : SobolevTower T) (t : ↑(Set.Icc 0 T)) : (A.smoothField t).toLp = A.field t

theorem EulerOrdinarySobolev.SobolevTower.smoothField_jet_continuous {T : ℝ} (A : SobolevTower T) (n : ℕ) : Continuous fun (t : ↑(Set.Icc 0 T)) => (A.smoothField t).jetLp n

theorem EulerOrdinarySobolev.SobolevTower.smoothField_realization {T : ℝ} (A : SobolevTower T) (q : ℕ) (t : ↑(Set.Icc 0 T)) : EulerMeanSmoothRepresentative.ordinarySobolev q (A.smoothField t).toLp ⋯ = (A.realization q) t

theorem EulerOrdinarySobolev.SobolevTower.smoothField_path {T : ℝ} (A : SobolevTower T) (q : ℕ) : EulerSmoothFieldSobolevTime.sobolevPath A.smoothField ⋯ q = A.realization q

noncomputable def EulerOrdinarySobolev.ordinaryTensorOperator (q : ℕ) : ↥(EulerCylinderSobolevSpace.SobolevSpace 1 q) →L[ℝ] ↥(MeasureTheory.Lp (EulerSmoothLimit.Space [×q]→L[ℝ] EulerSmoothLimit.Space) 2 MeasureTheory.volume)

Ordinary tensor operator as an element of SobolevSpace 1 q →L[ℝ] Lp (Space [×q]→L[ℝ] Space) 2 (volume : Measure Space).

Equations

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

theorem EulerOrdinarySobolev.ordinaryTensorOperator_apply (A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (q : ℕ) : (ordinaryTensorOperator q) (EulerMeanSmoothRepresentative.ordinarySobolev q A.toLp ⋯) = A.jetLp q

theorem EulerOrdinarySobolev.SobolevTower.tensorOperator_realization {T : ℝ} (A : SobolevTower T) (q : ℕ) (t : ↑(Set.Icc 0 T)) : (ordinaryTensorOperator q) ((A.realization q) t) = (A.smoothField t).jetLp q