pith. machine review for the scientific record. sign in
def definition def or abbrev

nsDuhamelCoeffBound_kernelIntegral

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

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 :=

proof body

Definition body.

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 ≤ ν`. -/

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (22)

Lean names referenced from this declaration's body.