Uniform Sobolev bounds and actual L² convergence give strong convergence below the top derivative order.

Actual uniform-in-time interpolation and its Cauchy consequence.

Strong-derivative interpolation on the actual cylinder Sobolev spaces.

theorem EulerSobolevInterpolation.word_square_le_parent (period : ℝ) [Fact (0 < period)] {s n : ℕ} (h : n + 2 ≤ s) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period s)) (w : Fin n → Fin 4) (i : Fin 4) : ‖EulerCylinderSobolevSpace.word period u ⋯ (Fin.cons i w)‖ ^ 2 ≤ ‖EulerCylinderSobolevSpace.word period u ⋯ w‖ * ‖u‖

One genuine derivative is controlled by its parent word and one available higher derivative.

theorem EulerSobolevPathInterpolation.cauchySeq_of_square_bound {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedAddCommGroup F] (f : ℕ → E) (g : ℕ → F) (A : ℝ) (hA : 0 ≤ A) (hf : CauchySeq f) (h : ∀ (m n : ℕ), ‖g m - g n‖ ^ 2 ≤ A * ‖f m - f n‖) : CauchySeq g

A squared difference estimate transfers the Cauchy property without an unproved interpolation premise.

@[instance_reducible]

noncomputable def EulerSobolevPathInterpolation.interpolationGroup (period : ℝ) [Fact (0 < period)] (s : ℕ) : NormedAddCommGroup ↥(EulerCylinderSobolevSpace.SobolevSpace period s)

The inherited normed group on each actual Sobolev space.

Equations

• EulerSobolevPathInterpolation.interpolationGroup period s = inferInstance

@[instance_reducible]

noncomputable def EulerSobolevPathInterpolation.interpolationSpace (period : ℝ) [Fact (0 < period)] (s : ℕ) : NormedSpace ℝ ↥(EulerCylinderSobolevSpace.SobolevSpace period s)

The inherited real normed space on each actual Sobolev space.

Equations

• EulerSobolevPathInterpolation.interpolationSpace period s = inferInstance

noncomputable def EulerSobolevPathInterpolation.wordPathOperator (period : ℝ) [Fact (0 < period)] {s n : ℕ} (h : n ≤ s) (w : Fin n → Fin 4) (T : ℝ) : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period s)) →L[ℝ] C(↑(Set.Icc 0 T), ↥(EulerLiftedGradientSpace.LiftL2 period))

One actual Sobolev derivative coordinate as a continuous time-path operator.

Equations

• EulerSobolevPathInterpolation.wordPathOperator period h w T = ContinuousLinearMap.compLeftContinuous ℝ (↑(Set.Icc 0 T)) (EulerCylinderSobolevSpace.wordOperator period ⟨⟨n, ⋯⟩, w⟩)

theorem EulerSobolevPathInterpolation.wordPathOperator_apply (period : ℝ) [Fact (0 < period)] {s n : ℕ} (h : n ≤ s) (w : Fin n → Fin 4) (T : ℝ) (u : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period s))) (t : ↑(Set.Icc 0 T)) : ((wordPathOperator period h w T) u) t = EulerCylinderSobolevSpace.word period (u t) h w

The derivative path is its literal derivative coordinate at each time.

theorem EulerSobolevPathInterpolation.wordPath_square_bound (period : ℝ) [Fact (0 < period)] {s n : ℕ} (h : n + 2 ≤ s) (w : Fin n → Fin 4) (i : Fin 4) (T : ℝ) (u : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period s))) : ‖(wordPathOperator period ⋯ (Fin.cons i w) T) u‖ ^ 2 ≤ ‖(wordPathOperator period ⋯ w T) u‖ * ‖u‖

The exact strong-derivative interpolation inequality also controls the uniform time-path norm.

theorem EulerSobolevPathInterpolation.wordPath_sub (period : ℝ) [Fact (0 < period)] {s n : ℕ} (h : n ≤ s) (w : Fin n → Fin 4) (T : ℝ) (u v : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period s))) : (wordPathOperator period h w T) (u - v) = (wordPathOperator period h w T) u - (wordPathOperator period h w T) v

Actual derivative-coordinate paths preserve subtraction.

theorem EulerSobolevPathInterpolation.wordPath_difference_square_bound (period : ℝ) [Fact (0 < period)] {s n : ℕ} (h : n + 2 ≤ s) (w : Fin n → Fin 4) (i : Fin 4) (T M : ℝ) (u v : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period s))) (hu : ‖u‖ ≤ M) (hv : ‖v‖ ≤ M) : ‖(wordPathOperator period ⋯ (Fin.cons i w) T) u - (wordPathOperator period ⋯ (Fin.cons i w) T) v‖ ^ 2 ≤ 2 * M * ‖(wordPathOperator period ⋯ w T) u - (wordPathOperator period ⋯ w T) v‖

The actual difference interpolation estimate depends only on the two given uniform state bounds.

theorem EulerSobolevPathInterpolation.wordPath_cauchy_step (period : ℝ) [Fact (0 < period)] {s n : ℕ} (h : n + 2 ≤ s) (w : Fin n → Fin 4) (i : Fin 4) (T M : ℝ) (hM : 0 ≤ M) (u : ℕ → C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period s))) (hu : ∀ (k : ℕ), ‖u k‖ ≤ M) (hw : CauchySeq fun (k : ℕ) => (wordPathOperator period ⋯ w T) (u k)) : CauchySeq fun (k : ℕ) => (wordPathOperator period ⋯ (Fin.cons i w) T) (u k)

Uniformly bounded actual Sobolev paths transfer Cauchy control from a parent word to a derivative.

@[instance_reducible]

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

The inherited normed group on the actual Sobolev state space.

Equations

• EulerSobolevCauchyInterpolation.cauchySobolevGroup period q = inferInstance

@[instance_reducible]

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

The inherited real normed space on the actual Sobolev state space.

Equations

• EulerSobolevCauchyInterpolation.cauchySobolevSpace period q = inferInstance

theorem EulerSobolevCauchyInterpolation.wordPath_cauchy_of_value (period : ℝ) [Fact (0 < period)] {s : ℕ} (T M : ℝ) (hM : 0 ≤ M) (u : ℕ → C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period s))) (hu : ∀ (k : ℕ), ‖u k‖ ≤ M) (h0 : CauchySeq fun (k : ℕ) => (ContinuousLinearMap.compLeftContinuous ℝ (↑(Set.Icc 0 T)) (EulerCylinderSobolevSpace.valueOperator period s)) (u k)) (n : ℕ) (hn : n < s) (w : Fin n → Fin 4) : CauchySeq fun (k : ℕ) => (EulerSobolevPathInterpolation.wordPathOperator period ⋯ w T) (u k)

Every actual derivative coordinate below the top uniformly bounded order is a Cauchy path.

noncomputable def EulerSobolevCauchyInterpolation.pathCoordinates (period : ℝ) [Fact (0 < period)] (q : ℕ) (T : ℝ) : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period q)) →L[ℝ] EulerCylinderSobolevSpace.SobolevWord q → C(↑(Set.Icc 0 T), ↥(EulerLiftedGradientSpace.LiftL2 period))

The complete Sobolev time path expressed by its finitely many literal coordinate paths.

Equations

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

theorem EulerSobolevCauchyInterpolation.pathCoordinates_norm (period : ℝ) [Fact (0 < period)] (q : ℕ) (T : ℝ) (u : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period q))) : ‖(pathCoordinates period q T) u‖ = ‖u‖

The actual finite-coordinate path map preserves the full uniform Sobolev norm exactly.

theorem EulerSobolevCauchyInterpolation.path_cauchy_of_coordinates (period : ℝ) [Fact (0 < period)] (q : ℕ) (T : ℝ) (u : ℕ → C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period q))) (hu : ∀ (w : EulerCylinderSobolevSpace.SobolevWord q), CauchySeq fun (k : ℕ) => (pathCoordinates period q T) (u k) w) : CauchySeq u

Cauchy control of every actual coordinate path gives Cauchy control in the complete Sobolev path space.

theorem EulerSobolevCauchyInterpolation.cauchy_restrict_of_value (period : ℝ) [Fact (0 < period)] {s q : ℕ} (hq : q < s) (T M : ℝ) (hM : 0 ≤ M) (u : ℕ → C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period s))) (hu : ∀ (k : ℕ), ‖u k‖ ≤ M) (h0 : CauchySeq fun (k : ℕ) => (ContinuousLinearMap.compLeftContinuous ℝ (↑(Set.Icc 0 T)) (EulerCylinderSobolevSpace.valueOperator period s)) (u k)) : CauchySeq fun (k : ℕ) => (ContinuousLinearMap.compLeftContinuous ℝ (↑(Set.Icc 0 T)) (EulerCylinderSobolevSpace.restrictOperator period ⋯)) (u k)

A uniformly bounded actual Sobolev sequence that is Cauchy in L² is Cauchy at every strictly lower Sobolev order, uniformly in time.

theorem EulerSobolevCauchyInterpolation.exists_limit_restrict_of_value (period : ℝ) [Fact (0 < period)] {s q : ℕ} (hq : q < s) (T M : ℝ) (hM : 0 ≤ M) (u : ℕ → C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period s))) (hu : ∀ (k : ℕ), ‖u k‖ ≤ M) (h0 : CauchySeq fun (k : ℕ) => (ContinuousLinearMap.compLeftContinuous ℝ (↑(Set.Icc 0 T)) (EulerCylinderSobolevSpace.valueOperator period s)) (u k)) : ∃ (v : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period q))), Filter.Tendsto (fun (k : ℕ) => (ContinuousLinearMap.compLeftContinuous ℝ (↑(Set.Icc 0 T)) (EulerCylinderSobolevSpace.restrictOperator period ⋯)) (u k)) Filter.atTop (nhds v)

Completeness produces the actual strong lower-order Sobolev limit from those concrete bounds.