Actual ordinary L² convergence upgrades to convergence in every fixed Sobolev norm under uniform higher-order bounds.

theorem EulerOrdinarySobolev.instOrdinaryCauchyInterpolation1 : Fact (0 < 1)

theorem EulerOrdinarySobolev.wordMaximum_zero (A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) : wordMaximum 0 A = ‖A.toLp‖

theorem EulerOrdinarySobolev.tensorNorm_interpolate_zero (A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (q : ℕ) (N : ℝ) (hN : WordBound (2 * q) N A) : tensorNorm q A ≤ wordCount q * √(‖A.toLp‖ * N)

theorem EulerOrdinarySobolev.ordinarySobolev_norm_le_tensor (A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (q : ℕ) : ‖EulerMeanSmoothRepresentative.ordinarySobolev q A.toLp ⋯‖ ≤ tensorNorm q A

noncomputable def EulerOrdinarySobolev.fieldPath {T : ℝ} (A : ↑(Set.Icc 0 T) → EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (hA : ∀ (n : ℕ), Continuous fun (t : ↑(Set.Icc 0 T)) => (A t).jetLp n) : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2)

Field path, given by ⟨fun t => (A t).toLp,continuous_toLp A (hA 0)⟩.

Equations

• EulerOrdinarySobolev.fieldPath A hA = { toFun := fun (t : ↑(Set.Icc 0 T)) => (A t).toLp, continuous_toFun := ⋯ }

theorem EulerOrdinarySobolev.sobolevPath_norm_le_tensor {T : ℝ} (A : ↑(Set.Icc 0 T) → EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (hA : ∀ (n : ℕ), Continuous fun (t : ↑(Set.Icc 0 T)) => (A t).jetLp n) (q : ℕ) (M : ℝ) (hM : 0 ≤ M) (hb : ∀ (t : ↑(Set.Icc 0 T)), tensorNorm q (A t) ≤ M) : ‖EulerSmoothFieldSobolevTime.sobolevPath A hA q‖ ≤ M

theorem EulerOrdinarySobolev.sobolevPath_cauchy_of_l2 {T : ℝ} (hT : 0 ≤ T) (A : ℕ → ↑(Set.Icc 0 T) → EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (hA : ∀ (k n : ℕ), Continuous fun (t : ↑(Set.Icc 0 T)) => (A k t).jetLp n) (hb : ∀ (q : ℕ), ∃ (M : ℝ), ∀ (k : ℕ) (t : ↑(Set.Icc 0 T)), tensorNorm q (A k t) ≤ M) (h0 : CauchySeq fun (k : ℕ) => fieldPath (A k) ⋯) (q : ℕ) : CauchySeq fun (k : ℕ) => EulerSmoothFieldSobolevTime.sobolevPath (A k) ⋯ q

theorem EulerOrdinarySobolev.exists_sobolevPath_limit {T : ℝ} (hT : 0 ≤ T) (A : ℕ → ↑(Set.Icc 0 T) → EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (hA : ∀ (k n : ℕ), Continuous fun (t : ↑(Set.Icc 0 T)) => (A k t).jetLp n) (hb : ∀ (q : ℕ), ∃ (M : ℝ), ∀ (k : ℕ) (t : ↑(Set.Icc 0 T)), tensorNorm q (A k t) ≤ M) (h0 : CauchySeq fun (k : ℕ) => fieldPath (A k) ⋯) (q : ℕ) : ∃ (p : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace 1 q))), Filter.Tendsto (fun (k : ℕ) => EulerSmoothFieldSobolevTime.sobolevPath (A k) ⋯ q) Filter.atTop (nhds p)