nsDuhamelCoeffBound

formal source

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 :=
1460  { IsSolution := fun u =>
1461      (∀ t ≥ 0, ∀ k : Mode2, ‖(u t) k‖ ≤ H.B) ∧ IsNSDuhamelTraj ν D u
1462    isSolution := by
1463      refine ⟨?_, ?_⟩
1464      · intro t ht k
1465        simpa using (ConvergenceHypothesis.coeff_bound_of_uniformBounds (HC := HC) t ht k)
1466      · exact ConvergenceHypothesis.nsDuhamel_of_forall (HC := HC) (ν := ν) (D_N := D_N) (D := D) hD hId }
1467
1468/-- Identification constructor: coefficient bound + Duhamel remainder identity where the remainder is
1469defined as a **kernel integral** of a forcing term, and convergence of the kernel integrals is
1470packaged via `DuhamelKernelDominatedConvergenceAt`. -/
1471def nsDuhamelCoeffBound_kernelIntegral {H : UniformBoundsHypothesis} (HC : ConvergenceHypothesis H) (ν : ℝ)
1472    (F_N : ℕ → ℝ → FourierState2D) (F : ℝ → FourierState2D)
1473    (hDC : ∀ t : ℝ, ∀ k : Mode2, DuhamelKernelDominatedConvergenceAt ν F_N F t k)
1474    (hId :
1475      ∀ N : ℕ, ∀ t ≥ 0, ∀ k : Mode2,
1476        (extendByZero (H.uN N t) k) =
1477          (heatFactor ν t k) • (extendByZero (H.uN N 0) k)
1478            + (duhamelKernelIntegral ν (F_N N) t) k) :
1479    IdentificationHypothesis HC :=
1480  { IsSolution := fun u =>
1481      (∀ t ≥ 0, ∀ k : Mode2, ‖(u t) k‖ ≤ H.B) ∧ IsNSDuhamelTraj ν (duhamelKernelIntegral ν F) u