1489
1490/-- Same as `nsDuhamelCoeffBound_kernelIntegral`, but assumes dominated convergence at the **forcing**
1491level (not the kernel integrand), plus `0 ≤ ν`. -/
1492def nsDuhamelCoeffBound_kernelIntegral_of_forcing {H : UniformBoundsHypothesis} (HC : ConvergenceHypothesis H)
1493    (ν : ℝ) (hν : 0 ≤ ν)
1494    (F_N : ℕ → ℝ → FourierState2D) (F : ℝ → FourierState2D)
1495    (hF :
1496      ∀ t : ℝ, t ≥ 0 → ∀ k : Mode2, ForcingDominatedConvergenceAt (F_N := F_N) (F := F) t k)
1497    (hId :
1498      ∀ N : ℕ, ∀ t ≥ 0, ∀ k : Mode2,
1499        (extendByZero (H.uN N t) k) =
1500          (heatFactor ν t k) • (extendByZero (H.uN N 0) k)
1501            + (duhamelKernelIntegral ν (F_N N) t) k) :
1502    IdentificationHypothesis HC :=
1503  { IsSolution := fun u =>
1504      (∀ t ≥ 0, ∀ k : Mode2, ‖(u t) k‖ ≤ H.B) ∧ IsNSDuhamelTraj ν (duhamelKernelIntegral ν F) u
1505    isSolution := by
1506      refine ⟨?_, ?_⟩
1507      · intro t ht k
1508        simpa using (ConvergenceHypothesis.coeff_bound_of_uniformBounds (HC := HC) t ht k)
1509      · exact
1510          ConvergenceHypothesis.nsDuhamel_of_forall_kernelIntegral_of_forcing (HC := HC)
1511            (ν := ν) hν (F_N := F_N) (F := F) hF hId }
1512
1513/-- Identification constructor: a specialization of `nsDuhamelCoeffBound_kernelIntegral` where the
1514forcing family is the **actual Galerkin nonlinearity** `extendByZero (B(u_N,u_N))`. The Duhamel
1515identity for each approximant is discharged by `galerkin_duhamelKernel_identity`; the remaining
1516analytic ingredient is the dominated-convergence hypothesis `hDC`. -/
1517def nsDuhamelCoeffBound_galerkinKernel {H : UniformBoundsHypothesis} (HC : ConvergenceHypothesis H) (ν : ℝ)
1518    (Bop : (N : ℕ) → ConvectionOp N)
1519    (hu :
1520      ∀ N : ℕ, ∀ s : ℝ,
1521        HasDerivAt (H.uN N) (galerkinNSRHS (N := N) ν (Bop N) (H.uN N s)) s)
1522    (hint :

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.