Fourier Leray #
Supporting estimates for the Navier–Stokes development.
The real frequency vector represented in the complex velocity space of
sec:regularised.
Equations
- CKN.Leray.complexifyFrequency ξ = WithLp.toLp 2 fun (i : Fin 3) => ↑(ξ.ofLp i)
Instances For
Complexification preserves the Euclidean magnitude of the frequency.
The reciprocal squared frequency magnitude, set to zero at the origin, for the explicit Leray and pressure multiplier formulas.
Instances For
The Leray symbol in coordinates, written in a form suitable for pointwise Fourier multiplication.
Equations
Instances For
The coordinate formula for the Leray symbol is Borel measurable in
frequency and input, as required for its L² multiplier action.
A measurable frequency symbol with a uniform fiber bound acts on spatial
L² by pointwise multiplication in Fourier space.
A measurable frequency symbol with a uniform fiber bound acts on spatial
L² by pointwise multiplication in Fourier space.
Equations
- CKN.Leray.measurableFourierMultiplier m hm C hbound f = MeasureTheory.MemLp.toLp (fun (ξ : CKN.Foundation.Parabolic.L2Vec3) => m (ξ, ↑↑f ξ)) ⋯
Instances For
The L² multiplier agrees almost everywhere with its pointwise symbol
formula.
A measurable Fourier multiplier has the same uniform fiber bound on its
L² operator norm.
The complex line parallel to a frequency vector, used to define the
orthogonal Leray symbol in sec:regularised.
Equations
Instances For
The orthogonal projection onto the complement of the frequency direction,
with the identity value at zero, as in sec:regularised.
Equations
Instances For
The Leray symbol is an L²-fiber contraction, used in
lem:reg-multiplier-bounds.
The orthogonal Leray symbol has the explicit coordinate formula used in
sec:regularised.
The Leray projection acting on frequency-space vector L².
Equations
- One or more equations did not get rendered due to their size.
Instances For
The Leray Fourier multiplier is an L² contraction.
The physical Leray projection on complex velocity fields, obtained by Fourier transformation, pointwise projection, and inverse transformation.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The physical Leray projection is an L² contraction.
The range of the Leray symbol is orthogonal to the frequency direction,
used to verify divergence freedom in lem:reg-multiplier-bounds.
The Leray Fourier projection has divergence-free range almost everywhere in frequency space.
The Fourier symbol for tensor divergence, with the first tensor index
contracted against the frequency vector in sec:regularised.
Equations
- CKN.Leray.tensorDivergenceLinear ξ = { toFun := fun (F : CKN.Leray.ComplexTensor3) => ∑ i : Fin 3, ↑(ξ.ofLp i) • F.ofLp i, map_add' := ⋯, map_smul' := ⋯ }
Instances For
Tensor divergence has fiber norm at most the frequency magnitude, used in
lem:reg-multiplier-bounds.
The bounded continuous-linear-map form of the tensor-divergence symbol.
Equations
Instances For
The double-Riesz pressure symbol, with value zero at zero frequency, as
in sec:regularised.
Equations
Instances For
The pressure symbol is an L²-fiber contraction, hence satisfies the
weaker bound stated in lem:reg-multiplier-bounds.
The pressure multiplier evaluated on one tensor, with the value zero assigned at zero frequency.
Equations
Instances For
Evaluation of the pressure symbol agrees with its coordinate formula.
The pressure multiplier formula is measurable in frequency and tensor.
The pressure multiplier formula is pointwise bounded by the Frobenius norm of its tensor input.
The pressure Fourier multiplier maps tensor L² into scalar L².
Equations
- One or more equations did not get rendered due to their size.
Instances For
The pressure Fourier multiplier is bounded on L² by one, hence by the
constant three in lem:reg-multiplier-bounds.
The physical double-Riesz pressure map on tensor-valued L².
Equations
- One or more equations did not get rendered due to their size.
Instances For
The physical double-Riesz pressure map has the stronger L² bound one.
The pointwise Fourier symbol of the heat-regularized Leray-Stokes map in
sec:regularised.
Equations
Instances For
The Stokes symbol is bounded by the heat-gradient multiplier times the Frobenius norm of the input tensor.
The Leray-regularized Stokes symbol has the Abel-kernel bound in
lem:reg-multiplier-bounds.
The pointwise heat, tensor-divergence, and Leray formula for the Stokes
multiplier in sec:regularised.
Equations
- CKN.Leray.stokesApplyFormula t ξ F = (CKN.Leray.heatSymbol t ξ * (2 * ↑Real.pi * Complex.I)) • CKN.Leray.lerayApplyFormula ξ ((CKN.Leray.tensorDivergenceLinear ξ) F)
Instances For
Evaluation of the Stokes symbol agrees with its coordinate formula.
The Leray--Stokes symbol has divergence-free range at each frequency.
The Stokes multiplier formula is measurable in frequency and tensor.
The Stokes multiplier formula has the integrable Abel-kernel fiber bound
from lem:reg-multiplier-bounds.
The Stokes Fourier multiplier on tensor-valued spatial L².
Equations
- One or more equations did not get rendered due to their size.
Instances For
The Stokes Fourier multiplier has the t^{-1/2} bound in
lem:reg-multiplier-bounds.
The Stokes Fourier multiplier has divergence-free range almost everywhere in frequency space.
The physical heat-regularized Leray-Stokes operator on tensor-valued
spatial L².
Equations
- One or more equations did not get rendered due to their size.
Instances For
The physical Stokes operator has the integrable t^{-1/2} bound.