Existence on finite intervals for the projected tangent equation

We first extend the contracting-iterate Picard argument to all continuous curves on a compact interval. A globally Lipschitz vector field therefore has a solution on the whole prescribed interval, without a small-time assumption. Continuous linear coefficients provide the required bound.

structure NavierStokes.TangentODE.IntervalSystem (E : Type u_2) [NormedAddCommGroup E] : Type u_2

Continuous vector field, globally Lipschitz in its state variable, on a prescribed compact time interval.

• left : ℝ

  Left of IntervalSystem, of type ℝ.

• right : ℝ

  Right of IntervalSystem, of type ℝ.

• ordered : self.left ≤ self.right
• initial : E

  Initial of IntervalSystem, of type E.

• field : ℝ → E → E

  Underlying field of IntervalSystem, of type ℝ → E → E.

• lip : NNReal

  Lip of IntervalSystem, of type ℝ≥0.

• lipschitz (t : ℝ) : t ∈ Set.Icc self.left self.right → LipschitzWith self.lip (self.field t)
• continuous : Continuous fun (p : ↑(Set.Icc self.left self.right) × E) => self.field (↑p.1) p.2

noncomputable def NavierStokes.TangentODE.IntervalSystem.proj {E : Type u_1} [NormedAddCommGroup E] (v : IntervalSystem E) : ℝ → ↑(Set.Icc v.left v.right)

Proj, given by projIcc v.left v.right v.ordered.

Equations

• v.proj = Set.projIcc v.left v.right ⋯

theorem NavierStokes.TangentODE.IntervalSystem.proj_of_mem {E : Type u_1} [NormedAddCommGroup E] (v : IntervalSystem E) {t : ℝ} (ht : t ∈ Set.Icc v.left v.right) : ↑(v.proj t) = t

theorem NavierStokes.TangentODE.IntervalSystem.proj_coe {E : Type u_1} [NormedAddCommGroup E] (v : IntervalSystem E) (t : ↑(Set.Icc v.left v.right)) : v.proj ↑t = t

theorem NavierStokes.TangentODE.IntervalSystem.continuous_proj {E : Type u_1} [NormedAddCommGroup E] (v : IntervalSystem E) : Continuous v.proj

noncomputable def NavierStokes.TangentODE.IntervalSystem.composeField {E : Type u_1} [NormedAddCommGroup E] (v : IntervalSystem E) (f : C(↑(Set.Icc v.left v.right), E)) (t : ℝ) : E

Compose field, given by v.field (v.proj t) (f (v.proj t)).

Equations

• v.composeField f t = v.field (↑(v.proj t)) (f (v.proj t))

theorem NavierStokes.TangentODE.IntervalSystem.continuous_composeField {E : Type u_1} [NormedAddCommGroup E] (v : IntervalSystem E) (f : C(↑(Set.Icc v.left v.right), E)) : Continuous (v.composeField f)

theorem NavierStokes.TangentODE.IntervalSystem.integrable_composeField {E : Type u_1} [NormedAddCommGroup E] (v : IntervalSystem E) (f : C(↑(Set.Icc v.left v.right), E)) (a b : ℝ) : IntervalIntegrable (v.composeField f) MeasureTheory.volume a b

noncomputable def NavierStokes.TangentODE.IntervalSystem.integralCurve {E : Type u_1} [NormedAddCommGroup E] (v : IntervalSystem E) [NormedSpace ℝ E] (f : C(↑(Set.Icc v.left v.right), E)) (t : ℝ) : E

Integral curve, given by v.initial + ∫ s in v.left..t, v.composeField f s.

Equations

• v.integralCurve f t = v.initial + ∫ (s : ℝ) in v.left..t, v.composeField f s

theorem NavierStokes.TangentODE.IntervalSystem.hasDerivAt_integralCurve {E : Type u_1} [NormedAddCommGroup E] (v : IntervalSystem E) [NormedSpace ℝ E] [CompleteSpace E] (f : C(↑(Set.Icc v.left v.right), E)) (t : ℝ) : HasDerivAt (v.integralCurve f) (v.composeField f t) t

noncomputable def NavierStokes.TangentODE.IntervalSystem.next {E : Type u_1} [NormedAddCommGroup E] (v : IntervalSystem E) [NormedSpace ℝ E] [CompleteSpace E] (f : C(↑(Set.Icc v.left v.right), E)) : C(↑(Set.Icc v.left v.right), E)

Next as an element of C(Icc v.left v.right, E).

Equations

• v.next f = { toFun := fun (t : ↑(Set.Icc v.left v.right)) => v.integralCurve f ↑t, continuous_toFun := ⋯ }

theorem NavierStokes.TangentODE.IntervalSystem.next_apply {E : Type u_1} [NormedAddCommGroup E] (v : IntervalSystem E) [NormedSpace ℝ E] [CompleteSpace E] (f : C(↑(Set.Icc v.left v.right), E)) (t : ↑(Set.Icc v.left v.right)) : (v.next f) t = v.initial + ∫ (s : ℝ) in v.left..↑t, v.composeField f s

theorem NavierStokes.TangentODE.IntervalSystem.dist_next_apply_le_of_le {E : Type u_1} [NormedAddCommGroup E] (v : IntervalSystem E) [NormedSpace ℝ E] [CompleteSpace E] {f g : C(↑(Set.Icc v.left v.right), E)} {n : ℕ} {d : ℝ} (h : ∀ (t : ↑(Set.Icc v.left v.right)), dist (f t) (g t) ≤ (↑v.lip * |↑t - v.left|) ^ n / ↑n.factorial * d) (t : ↑(Set.Icc v.left v.right)) : dist ((v.next f) t) ((v.next g) t) ≤ (↑v.lip * |↑t - v.left|) ^ (n + 1) / ↑(n + 1).factorial * d

theorem NavierStokes.TangentODE.IntervalSystem.dist_iterate_next_apply_le {E : Type u_1} [NormedAddCommGroup E] (v : IntervalSystem E) [NormedSpace ℝ E] [CompleteSpace E] (f g : C(↑(Set.Icc v.left v.right), E)) (n : ℕ) (t : ↑(Set.Icc v.left v.right)) : dist ((v.next^[n] f) t) ((v.next^[n] g) t) ≤ (↑v.lip * |↑t - v.left|) ^ n / ↑n.factorial * dist f g

theorem NavierStokes.TangentODE.IntervalSystem.dist_iterate_next_le {E : Type u_1} [NormedAddCommGroup E] (v : IntervalSystem E) [NormedSpace ℝ E] [CompleteSpace E] (f g : C(↑(Set.Icc v.left v.right), E)) (n : ℕ) : dist (v.next^[n] f) (v.next^[n] g) ≤ (↑v.lip * (v.right - v.left)) ^ n / ↑n.factorial * dist f g

theorem NavierStokes.TangentODE.IntervalSystem.exists_contracting_iterate {E : Type u_1} [NormedAddCommGroup E] (v : IntervalSystem E) [NormedSpace ℝ E] [CompleteSpace E] : ∃ (N : ℕ) (K : NNReal), ContractingWith K v.next^[N]

theorem NavierStokes.TangentODE.IntervalSystem.exists_fixed {E : Type u_1} [NormedAddCommGroup E] (v : IntervalSystem E) [NormedSpace ℝ E] [CompleteSpace E] : ∃ (f : C(↑(Set.Icc v.left v.right), E)), v.next f = f

theorem NavierStokes.TangentODE.IntervalSystem.exists_solution {E : Type u_1} [NormedAddCommGroup E] (v : IntervalSystem E) [NormedSpace ℝ E] [CompleteSpace E] : ∃ (u : ℝ → E), u v.left = v.initial ∧ ∀ t ∈ Set.Icc v.left v.right, HasDerivAt u (v.field t (u t)) t

Finite-interval existence with no smallness condition on interval length or Lipschitz constant. The resulting extension is differentiable at the endpoints too.

theorem NavierStokes.TangentODE.linear_uniform_lipschitz {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {a b : ℝ} (hab : a ≤ b) (A : ℝ → E →L[ℝ] E) (g : ℝ → E) (hA : ContinuousOn A (Set.Icc a b)) : ∃ (L : NNReal), ∀ t ∈ Set.Icc a b, LipschitzWith L fun (x : E) => (A t) x + g t

A continuous operator coefficient on a compact interval has a common global Lipschitz bound, including an arbitrary additive forcing.

theorem NavierStokes.TangentODE.exists_linear_solution {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {a b : ℝ} (hab : a ≤ b) (A : ℝ → E →L[ℝ] E) (g : ℝ → E) (hA : ContinuousOn A (Set.Icc a b)) (hg : ContinuousOn g (Set.Icc a b)) (x₀ : E) : ∃ (u : ℝ → E), u a = x₀ ∧ ∀ t ∈ Set.Icc a b, HasDerivAt u ((A t) (u t) + g t) t

Actual existence for a continuous-coefficient inhomogeneous linear ODE on any finite closed interval.

theorem NavierStokes.TangentODE.linear_solution_unique {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {a b : ℝ} (hab : a ≤ b) (A : ℝ → E →L[ℝ] E) (g : ℝ → E) (hA : ContinuousOn A (Set.Icc a b)) {u w : ℝ → E} (hu : ∀ t ∈ Set.Icc a b, HasDerivAt u ((A t) (u t) + g t) t) (hw : ∀ t ∈ Set.Icc a b, HasDerivAt w ((A t) (w t) + g t) t) (hinit : u a = w a) : Set.EqOn u w (Set.Icc a b)

Uniqueness on the complete finite interval follows from Grönwall's inequality.

noncomputable def NavierStokes.TangentODE.projectedOperator {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℝ H] (n n' : H) (K : H →L[ℝ] H) (δ : ℝ) : H →L[ℝ] H

Continuous linear part of equation (27), including the moving-normal term.

Equations

• NavierStokes.TangentODE.projectedOperator n n' K δ = -K + ((innerSL ℝ) n ∘SL K - (innerSL ℝ) n').smulRight ((inner ℝ n n)⁻¹ • n) - δ • ContinuousLinearMap.id ℝ H

theorem NavierStokes.TangentODE.projectedOperator_apply {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℝ H] (n n' x f : H) (K : H →L[ℝ] H) (δ : ℝ) : (projectedOperator n n' K δ) x - TangentProjection.tangentProj n f = TangentProjection.projectedRhs n n' x (K x) f δ

theorem NavierStokes.TangentODE.continuousOn_projectedOperator {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℝ H] {s : Set ℝ} (n n' : ℝ → H) (K : ℝ → H →L[ℝ] H) (δ : ℝ → ℝ) (hn : ContinuousOn n s) (hn' : ContinuousOn n' s) (hK : ContinuousOn K s) (hδ : ContinuousOn δ s) (hn0 : ∀ t ∈ s, n t ≠ 0) : ContinuousOn (fun (t : ℝ) => projectedOperator (n t) (n' t) (K t) (δ t)) s

Continuity of the true linear operator follows from the coefficient hypotheses; division is justified by the nonvanishing normal.

theorem NavierStokes.TangentODE.continuousOn_projectedForcing {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℝ H] {s : Set ℝ} (n f : ℝ → H) (hn : ContinuousOn n s) (hf : ContinuousOn f s) (hn0 : ∀ t ∈ s, n t ≠ 0) : ContinuousOn (fun (t : ℝ) => -TangentProjection.tangentProj (n t) (f t)) s

theorem NavierStokes.TangentODE.exists_projected_solution {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] {a b : ℝ} (hab : a ≤ b) (n n' f : ℝ → H) (K : ℝ → H →L[ℝ] H) (δ : ℝ → ℝ) (hn : ContinuousOn n (Set.Icc a b)) (hn' : ContinuousOn n' (Set.Icc a b)) (hf : ContinuousOn f (Set.Icc a b)) (hK : ContinuousOn K (Set.Icc a b)) (hδ : ContinuousOn δ (Set.Icc a b)) (hn0 : ∀ t ∈ Set.Icc a b, n t ≠ 0) (x₀ : H) : ∃ (u : ℝ → H), u a = x₀ ∧ ∀ t ∈ Set.Icc a b, HasDerivAt u (TangentProjection.projectedRhs (n t) (n' t) (u t) ((K t) (u t)) (f t) (δ t)) t

The actual projected tangent equation has a solution on the entire finite interval when its coefficients are continuous and its normal never vanishes.

theorem NavierStokes.TangentODE.projected_solution_unique {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℝ H] {a b : ℝ} (hab : a ≤ b) (n n' f : ℝ → H) (K : ℝ → H →L[ℝ] H) (δ : ℝ → ℝ) (hn : ContinuousOn n (Set.Icc a b)) (hn' : ContinuousOn n' (Set.Icc a b)) (hK : ContinuousOn K (Set.Icc a b)) (hδ : ContinuousOn δ (Set.Icc a b)) (hn0 : ∀ t ∈ Set.Icc a b, n t ≠ 0) {u w : ℝ → H} (hu : ∀ t ∈ Set.Icc a b, HasDerivAt u (TangentProjection.projectedRhs (n t) (n' t) (u t) ((K t) (u t)) (f t) (δ t)) t) (hw : ∀ t ∈ Set.Icc a b, HasDerivAt w (TangentProjection.projectedRhs (n t) (n' t) (w t) ((K t) (w t)) (f t) (δ t)) t) (hinit : u a = w a) : Set.EqOn u w (Set.Icc a b)

Uniqueness holds for all solutions of equation (27), independent of whether their common initial value is tangent.

theorem NavierStokes.TangentODE.projected_tangency_preserved {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℝ H] {a b : ℝ} (hab : a ≤ b) (n n' f u : ℝ → H) (K : ℝ → H →L[ℝ] H) (δ : ℝ → ℝ) (hδ : ContinuousOn δ (Set.Icc a b)) (hn0 : ∀ t ∈ Set.Icc a b, n t ≠ 0) (hn : ∀ t ∈ Set.Icc a b, HasDerivAt n (n' t) t) (hu : ∀ t ∈ Set.Icc a b, HasDerivAt u (TangentProjection.projectedRhs (n t) (n' t) (u t) ((K t) (u t)) (f t) (δ t)) t) (hinit : inner ℝ (n a) (u a) = 0) (t : ℝ) : t ∈ Set.Icc a b → inner ℝ (n t) (u t) = 0

On the finite interval, tangency propagates from the left endpoint. No primitive or globally defined solution is assumed.

theorem NavierStokes.TangentODE.exists_unique_tangent_solution {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] {a b : ℝ} (hab : a ≤ b) (n n' f : ℝ → H) (K : ℝ → H →L[ℝ] H) (δ : ℝ → ℝ) (hn : ∀ t ∈ Set.Icc a b, HasDerivAt n (n' t) t) (hn' : ContinuousOn n' (Set.Icc a b)) (hf : ContinuousOn f (Set.Icc a b)) (hK : ContinuousOn K (Set.Icc a b)) (hδ : ContinuousOn δ (Set.Icc a b)) (hn0 : ∀ t ∈ Set.Icc a b, n t ≠ 0) (x₀ : H) (hx₀ : inner ℝ (n a) x₀ = 0) : ∃ (u : ℝ → H), u a = x₀ ∧ (∀ t ∈ Set.Icc a b, HasDerivAt u (TangentProjection.projectedRhs (n t) (n' t) (u t) ((K t) (u t)) (f t) (δ t)) t) ∧ (∀ t ∈ Set.Icc a b, inner ℝ (n t) (u t) = 0) ∧ ∀ (w : ℝ → H), w a = x₀ → (∀ t ∈ Set.Icc a b, HasDerivAt w (TangentProjection.projectedRhs (n t) (n' t) (w t) ((K t) (w t)) (f t) (δ t)) t) → Set.EqOn w u (Set.Icc a b)

Combined finite-interval existence, uniqueness, and moving tangency for equation (27). All analytic coefficient hypotheses are explicit.