rs_implies_global_regularity_2d_stokesODECoeffBound

formal source

 126(within `t ≥ 0`) Stokes/heat equation per mode.
 127
 128This is derived from the mild identity via `IsStokesMildTraj.stokesODE`. -/
 129theorem rs_implies_global_regularity_2d_stokesODECoeffBound
 130    (Hbounds : UniformBoundsHypothesis)
 131    (Hconv : ConvergenceHypothesis Hbounds)
 132    (ν : ℝ)
 133    (hMild :
 134      ∀ N : ℕ, ∀ t ≥ 0, ∀ k : Mode2,
 135        (extendByZero (Hbounds.uN N t) k) =
 136          (heatFactor ν t k) • (extendByZero (Hbounds.uN N 0) k)) :
 137    ∃ u : ℝ → FourierState2D,
 138      (∀ t : ℝ, ∀ k : Mode2,
 139        Filter.Tendsto (fun N : ℕ => (extendByZero (Hbounds.uN N t)) k) Filter.atTop
 140          (nhds ((u t) k)))
 141        ∧ (∀ t ≥ 0, ∀ k : Mode2, ‖(u t) k‖ ≤ Hbounds.B)
 142        ∧ IsStokesODETraj ν u := by
 143  refine ⟨Hconv.u, ?_, ?_, ?_⟩
 144  · simpa using Hconv.converges
 145  · intro t ht k
 146    simpa using (ConvergenceHypothesis.coeff_bound_of_uniformBounds (HC := Hconv) t ht k)
 147  ·
 148    have hm : IsStokesMildTraj ν Hconv.u :=
 149      ConvergenceHypothesis.stokesMild_of_forall (HC := Hconv) (ν := ν) hMild
 150    exact IsStokesMildTraj.stokesODE hm
 151
 152/-- Variant of the top-level theorem returning a first nonlinear (Duhamel-style) remainder identity.
 153
 154This uses `ConvergenceHypothesis.nsDuhamel_of_forall` to pass the identity to the limit,
 155assuming the approximants satisfy the identity with remainders `D_N` that converge modewise. -/
 156theorem rs_implies_global_regularity_2d_nsDuhamelCoeffBound
 157    (Hbounds : UniformBoundsHypothesis)
 158    (Hconv : ConvergenceHypothesis Hbounds)
 159    (ν : ℝ)