`nsDuhamelCoeffBound_kernelIntegral`

definition

show as: view math explainer →

module: IndisputableMonolith.ClassicalBridge.Fluids.ContinuumLimit2D
domain: ClassicalBridge
line: 1471 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.ClassicalBridge.Fluids.ContinuumLimit2D on GitHub at line 1471.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

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
1482    isSolution := by
1483      refine ⟨?_, ?_⟩
1484      · intro t ht k
1485        simpa using (ConvergenceHypothesis.coeff_bound_of_uniformBounds (HC := HC) t ht k)
1486      · exact
1487          ConvergenceHypothesis.nsDuhamel_of_forall_kernelIntegral (HC := HC) (ν := ν)
1488            (F_N := F_N) (F := F) hDC hId }
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) :

papers checked against this theorem

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