def
definition
def or abbrev
heatFactor
show as:
view Lean formalization →
formal statement (Lean)
160noncomputable def heatFactor (ν : ℝ) (t : ℝ) (k : Mode2) : ℝ :=
proof body
Definition body.
161 Real.exp (-ν * kSq k * t)
162
163/-- Mild Stokes/heat solution in Fourier coefficients (modewise, for `t ≥ 0`). -/
used by (31)
-
abs_heatFactor_le_one -
DuhamelKernelDominatedConvergenceAt -
duhamelKernelDominatedConvergenceAt_of_forcing -
duhamelKernelIntegral -
duhamelRemainderOfGalerkin -
duhamelRemainderOfGalerkin_integratingFactor -
duhamelRemainderOfGalerkin_kernel -
ForcingDominatedConvergenceAt -
galerkin_duhamelKernel_identity -
galerkinNS_hasDerivAt_duhamelRemainder_mode -
galerkinNS_hasDerivAt_extendByZero_mode -
IsNSDuhamelTraj -
IsStokesMildTraj -
IsStokesODETraj -
nsDuhamelCoeffBound -
nsDuhamelCoeffBound_galerkinKernel -
nsDuhamelCoeffBound_galerkinKernel_of_forcing -
nsDuhamelCoeffBound_kernelIntegral -
nsDuhamelCoeffBound_kernelIntegral_of_forcing -
nsDuhamel_of_forall -
nsDuhamel_of_forall_kernelIntegral -
nsDuhamel_of_forall_kernelIntegral_of_forcing -
stokesMildCoeffBound -
stokesMild_of_forall -
stokesODE -
tendsto_duhamelKernelIntegral_of_dominated_convergence -
rs_implies_global_regularity_2d_nsDuhamelCoeffBound -
rs_implies_global_regularity_2d_nsDuhamelCoeffBound_galerkinKernel -
rs_implies_global_regularity_2d_nsDuhamelCoeffBound_galerkinKernel_of_forcing -
rs_implies_global_regularity_2d_stokesMildCoeffBound