rs_implies_global_regularity_2d_stokesMildCoeffBound

formal source

 102  assuming each approximant satisfies the same identity modewise for `t ≥ 0`.
 103
 104This avoids providing a separate `IdentificationHypothesis`. -/
 105theorem rs_implies_global_regularity_2d_stokesMildCoeffBound
 106    (Hbounds : UniformBoundsHypothesis)
 107    (Hconv : ConvergenceHypothesis Hbounds)
 108    (ν : ℝ)
 109    (hMild :
 110      ∀ N : ℕ, ∀ t ≥ 0, ∀ k : Mode2,
 111        (extendByZero (Hbounds.uN N t) k) =
 112          (heatFactor ν t k) • (extendByZero (Hbounds.uN N 0) k)) :
 113    ∃ u : ℝ → FourierState2D,
 114      (∀ t : ℝ, ∀ k : Mode2,
 115        Filter.Tendsto (fun N : ℕ => (extendByZero (Hbounds.uN N t)) k) Filter.atTop
 116          (nhds ((u t) k)))
 117        ∧ (∀ t ≥ 0, ∀ k : Mode2, ‖(u t) k‖ ≤ Hbounds.B)
 118        ∧ IsStokesMildTraj ν u := by
 119  refine ⟨Hconv.u, ?_, ?_, ?_⟩
 120  · simpa using Hconv.converges
 121  · intro t ht k
 122    simpa using (ConvergenceHypothesis.coeff_bound_of_uniformBounds (HC := Hconv) t ht k)
 123  · exact ConvergenceHypothesis.stokesMild_of_forall (HC := Hconv) (ν := ν) hMild
 124
 125/-- Same as `rs_implies_global_regularity_2d_stokesMildCoeffBound`, but returns the **differential**
 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) =