stokesMildCoeffBound

formal source

1426
1427The bound part is proved from `UniformBoundsHypothesis` + convergence.
1428The mild Stokes identity is proved from the extra assumption that it holds for every approximant. -/
1429def stokesMildCoeffBound {H : UniformBoundsHypothesis} (HC : ConvergenceHypothesis H) (ν : ℝ)
1430    (hMild :
1431      ∀ N : ℕ, ∀ t ≥ 0, ∀ k : Mode2,
1432        (extendByZero (H.uN N t) k) = (heatFactor ν t k) • (extendByZero (H.uN N 0) k)) :
1433    IdentificationHypothesis HC :=
1434  { IsSolution := fun u =>
1435      (∀ t ≥ 0, ∀ k : Mode2, ‖(u t) k‖ ≤ H.B) ∧ IsStokesMildTraj ν u
1436    isSolution := by
1437      refine ⟨?_, ?_⟩
1438      · intro t ht k
1439        simpa using (ConvergenceHypothesis.coeff_bound_of_uniformBounds (HC := HC) t ht k)
1440      · exact ConvergenceHypothesis.stokesMild_of_forall (HC := HC) (ν := ν) hMild }
1441
1442/-- Identification constructor: coefficient bound + a first nonlinear (Duhamel-style) remainder identity.
1443
1444The coefficient bound part is proved from `UniformBoundsHypothesis` + convergence.
1445The Duhamel-remainder identity is proved from the extra assumptions:
1446
1447- each approximant satisfies `extendByZero uN(t,k) = heatFactor • extendByZero uN(0,k) + D_N(t,k)`, and
1448- `D_N(t,k) → D(t,k)` modewise.
1449
1450In later milestones, `D_N` will be instantiated as an actual time-integrated nonlinear forcing term. -/
1451def nsDuhamelCoeffBound {H : UniformBoundsHypothesis} (HC : ConvergenceHypothesis H) (ν : ℝ)
1452    (D_N : ℕ → ℝ → FourierState2D) (D : ℝ → FourierState2D)
1453    (hD : ∀ t : ℝ, ∀ k : Mode2,
1454      Tendsto (fun N : ℕ => (D_N N t) k) atTop (nhds ((D t) k)))
1455    (hId :
1456      ∀ N : ℕ, ∀ t ≥ 0, ∀ k : Mode2,
1457        (extendByZero (H.uN N t) k) =
1458          (heatFactor ν t k) • (extendByZero (H.uN N 0) k) + (D_N N t) k) :
1459    IdentificationHypothesis HC :=