Pointwise evolution of smooth L² fields upgrades to genuine strong Sobolev evolution when all spatial L² jets of the field and its prescribed time derivative are continuous. The ordinary field is represented by its isometric, angle-independent lift to the unit cylinder.

theorem EulerSmoothFieldSobolevTime.instSmoothFieldSobolevTime1 : Fact (0 < 1)

theorem EulerSmoothFieldSobolevTime.continuous_sobolev {K : Type u_1} [TopologicalSpace K] (A : K → EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (hA : ∀ (n : ℕ), Continuous fun (t : K) => (A t).jetLp n) (q : ℕ) : Continuous fun (t : K) => EulerMeanSmoothRepresentative.ordinarySobolev q (A t).toLp ⋯

noncomputable def EulerSmoothFieldSobolevTime.sobolevPath {K : Type u_1} [TopologicalSpace K] (A : K → EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (hA : ∀ (n : ℕ), Continuous fun (t : K) => (A t).jetLp n) (q : ℕ) : C(K, ↥(EulerCylinderSobolevSpace.SobolevSpace 1 q))

Sobolev path, given by ⟨fun t => ordinarySobolev q (A t).toLp (A t).translation_contDiff,continuous_sobolev A hA q⟩.

Equations

• EulerSmoothFieldSobolevTime.sobolevPath A hA q = { toFun := fun (t : K) => EulerMeanSmoothRepresentative.ordinarySobolev q (A t).toLp ⋯, continuous_toFun := ⋯ }

theorem EulerSmoothFieldSobolevTime.restrict_sobolev {p q : ℕ} (h : q ≤ p) (A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) : (EulerCylinderSobolevSpace.restrictOperator 1 h) (EulerMeanSmoothRepresentative.ordinarySobolev p A.toLp ⋯) = EulerMeanSmoothRepresentative.ordinarySobolev q A.toLp ⋯

noncomputable def EulerSmoothFieldSobolevTime.observation (q : ℕ) (hq : 3 ≤ q) (x : EulerLiftedGradientSpace.LiftDomain 1) : ↥(EulerCylinderSobolevSpace.SobolevSpace 1 q) →L[ℝ] EulerSmoothLimit.Space

Observation, given by (pointEvaluation 1 x).comp (restrictOperator 1 hq).

Equations

• EulerSmoothFieldSobolevTime.observation q hq x = EulerSobolevPointEvaluation.pointEvaluation 1 x ∘SL EulerCylinderSobolevSpace.restrictOperator 1 hq

theorem EulerSmoothFieldSobolevTime.observation_apply (q : ℕ) (hq : 3 ≤ q) (x : EulerLiftedGradientSpace.LiftDomain 1) (A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) : (observation q hq x) (EulerMeanSmoothRepresentative.ordinarySobolev q A.toLp ⋯) = A.field x.1

theorem EulerSmoothFieldSobolevTime.observation_injective (q : ℕ) (hq : 3 ≤ q) : Function.Injective fun (u : ↥(EulerCylinderSobolevSpace.SobolevSpace 1 q)) (x : EulerLiftedGradientSpace.LiftDomain 1) => (observation q hq x) u

theorem EulerSmoothFieldSobolevTime.sobolevPath_hasDerivWithinAt_of_three_le (T : ℝ) (hT : 0 ≤ T) (A B : ↑(Set.Icc 0 T) → EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (hA : ∀ (n : ℕ), Continuous fun (t : ↑(Set.Icc 0 T)) => (A t).jetLp n) (hB : ∀ (n : ℕ), Continuous fun (t : ↑(Set.Icc 0 T)) => (B t).jetLp n) (hd : ∀ (t : ℝ) (ht : t ∈ Set.Ioo 0 T) (x : EulerSmoothLimit.Space), HasDerivAt (fun (r : ℝ) => (A (Set.projIcc 0 T hT r)).field x) ((B ⟨t, ⋯⟩).field x) t) (q : ℕ) (hq : 3 ≤ q) (t : ↑(Set.Icc 0 T)) : HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT (sobolevPath A hA q)) ((sobolevPath B hB q) t) (Set.Icc 0 T) ↑t

theorem EulerSmoothFieldSobolevTime.sobolevPath_hasDerivWithinAt (T : ℝ) (hT : 0 ≤ T) (A B : ↑(Set.Icc 0 T) → EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (hA : ∀ (n : ℕ), Continuous fun (t : ↑(Set.Icc 0 T)) => (A t).jetLp n) (hB : ∀ (n : ℕ), Continuous fun (t : ↑(Set.Icc 0 T)) => (B t).jetLp n) (hd : ∀ (t : ℝ) (ht : t ∈ Set.Ioo 0 T) (x : EulerSmoothLimit.Space), HasDerivAt (fun (r : ℝ) => (A (Set.projIcc 0 T hT r)).field x) ((B ⟨t, ⋯⟩).field x) t) (q : ℕ) (t : ↑(Set.Icc 0 T)) : HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT (sobolevPath A hA q)) ((sobolevPath B hB q) t) (Set.Icc 0 T) ↑t

theorem EulerSmoothFieldSobolevTime.sobolevPath_hasDerivAt (T : ℝ) (hT : 0 ≤ T) (A B : ↑(Set.Icc 0 T) → EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (hA : ∀ (n : ℕ), Continuous fun (t : ↑(Set.Icc 0 T)) => (A t).jetLp n) (hB : ∀ (n : ℕ), Continuous fun (t : ↑(Set.Icc 0 T)) => (B t).jetLp n) (hd : ∀ (t : ℝ) (ht : t ∈ Set.Ioo 0 T) (x : EulerSmoothLimit.Space), HasDerivAt (fun (r : ℝ) => (A (Set.projIcc 0 T hT r)).field x) ((B ⟨t, ⋯⟩).field x) t) (q : ℕ) (t : ℝ) (ht : t ∈ Set.Ioo 0 T) : HasDerivAt (EulerVolterraConvolution.extendPath T hT (sobolevPath A hA q)) ((sobolevPath B hB q) ⟨t, ⋯⟩) t