A Cauchy sequence of genuine smooth L² paths with uniform bounds at every Sobolev order has a single genuine smooth limit path. All its tensor jets are continuous in time and are the strong limits of the corresponding jets of the sequence.

theorem EulerOrdinarySobolev.instOrdinarySmoothLimit1 : Fact (0 < 1)

noncomputable def EulerOrdinarySobolev.jetPath {T : ℝ} (A : ↑(Set.Icc 0 T) → EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (hA : ∀ (n : ℕ), Continuous fun (t : ↑(Set.Icc 0 T)) => (A t).jetLp n) (n : ℕ) : C(↑(Set.Icc 0 T), ↥(MeasureTheory.Lp (EulerSmoothLimit.Space [×n]→L[ℝ] EulerSmoothLimit.Space) 2 MeasureTheory.volume))

Jet path, given by ⟨fun t => (A t).jetLp n,hA n⟩.

Equations

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

structure EulerOrdinarySobolev.SmoothLimitData {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) : Type

Smooth limit data, collecting tower, value_convergence, sobolev_convergence.

• tower : SobolevTower T

  Tower of SmoothLimitData, of type SobolevTower T.

• value_convergence : Filter.Tendsto (fun (k : ℕ) => fieldPath (A k) ⋯) Filter.atTop (nhds self.tower.field)
• sobolev_convergence (q : ℕ) : Filter.Tendsto (fun (k : ℕ) => EulerSmoothFieldSobolevTime.sobolevPath (A k) ⋯ q) Filter.atTop (nhds (self.tower.realization q))

theorem EulerOrdinarySobolev.nonempty_smoothLimitData {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) ⋯) : Nonempty (SmoothLimitData A hA)

noncomputable def EulerOrdinarySobolev.smoothLimitData {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) ⋯) : SmoothLimitData A hA

Smooth limit data, given by Classical.choice (nonempty_smoothLimitData hT A hA hb h0).

Equations

• EulerOrdinarySobolev.smoothLimitData hT A hA hb h0 = Classical.choice ⋯

@[reducible, inline]

noncomputable abbrev EulerOrdinarySobolev.SmoothLimitData.field {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} (L : SmoothLimitData A hA) (t : ↑(Set.Icc 0 T)) : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space

Field: an abbreviation for L.tower.smoothField t.

Equations

• L.field t = L.tower.smoothField t

theorem EulerOrdinarySobolev.SmoothLimitData.field_continuous {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} (L : SmoothLimitData A hA) (n : ℕ) : Continuous fun (t : ↑(Set.Icc 0 T)) => (L.field t).jetLp n

theorem EulerOrdinarySobolev.SmoothLimitData.fieldPath_eq {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} (L : SmoothLimitData A hA) : fieldPath L.field ⋯ = L.tower.field

theorem EulerOrdinarySobolev.SmoothLimitData.fieldPath_convergence {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} (L : SmoothLimitData A hA) : Filter.Tendsto (fun (k : ℕ) => fieldPath (A k) ⋯) Filter.atTop (nhds (fieldPath L.field ⋯))

theorem EulerOrdinarySobolev.SmoothLimitData.jetPath_convergence {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} (L : SmoothLimitData A hA) (n : ℕ) : Filter.Tendsto (fun (k : ℕ) => jetPath (A k) ⋯ n) Filter.atTop (nhds (jetPath L.field ⋯ n))

theorem EulerOrdinarySobolev.SmoothLimitData.jet_convergence {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} (L : SmoothLimitData A hA) (n : ℕ) (t : ↑(Set.Icc 0 T)) : Filter.Tendsto (fun (k : ℕ) => (A k t).jetLp n) Filter.atTop (nhds ((L.field t).jetLp n))

theorem EulerOrdinarySobolev.SmoothLimitData.toLp_convergence {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} (L : SmoothLimitData A hA) (t : ↑(Set.Icc 0 T)) : Filter.Tendsto (fun (k : ℕ) => (A k t).toLp) Filter.atTop (nhds (L.field t).toLp)

theorem EulerOrdinarySobolev.SmoothLimitData.tensorNorm_convergence {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} (L : SmoothLimitData A hA) (q : ℕ) (t : ↑(Set.Icc 0 T)) : Filter.Tendsto (fun (k : ℕ) => tensorNorm q (A k t)) Filter.atTop (nhds (tensorNorm q (L.field t)))

theorem EulerOrdinarySobolev.SmoothLimitData.tensorNorm_bound {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} (L : SmoothLimitData A hA) (q : ℕ) (M : ℝ) (hb : ∀ (k : ℕ) (t : ↑(Set.Icc 0 T)), tensorNorm q (A k t) ≤ M) (t : ↑(Set.Icc 0 T)) : tensorNorm q (L.field t) ≤ M