Linearity of the Fourier Stokes operator

The pointwise multiplier defining K(t) is linear in its tensor input. This API is used to obtain continuity estimates for the Volterra term in lem:reg-local-mild.

theorem CKN.Leray.stokesFourierMultiplier_add {t : ℝ} (ht : 0 < t) (F G : ↥(MeasureTheory.Lp ComplexTensor3 2 MeasureTheory.volume)) : stokesFourierMultiplier ht (F + G) = stokesFourierMultiplier ht F + stokesFourierMultiplier ht G

The Stokes Fourier multiplier preserves addition of tensor inputs.

theorem CKN.Leray.stokesFourierMultiplier_smul {t : ℝ} (ht : 0 < t) (c : ℂ) (F : ↥(MeasureTheory.Lp ComplexTensor3 2 MeasureTheory.volume)) : stokesFourierMultiplier ht (c • F) = c • stokesFourierMultiplier ht F

The Stokes Fourier multiplier preserves complex scalar multiplication.

theorem CKN.Leray.stokesL2Operator_add {t : ℝ} (ht : 0 < t) (F G : ↥(MeasureTheory.Lp ComplexTensor3 2 MeasureTheory.volume)) : stokesL2Operator ht (F + G) = stokesL2Operator ht F + stokesL2Operator ht G

The physical Stokes operator is additive in the tensor field.

theorem CKN.Leray.stokesL2Operator_smul {t : ℝ} (ht : 0 < t) (c : ℂ) (F : ↥(MeasureTheory.Lp ComplexTensor3 2 MeasureTheory.volume)) : stokesL2Operator ht (c • F) = c • stokesL2Operator ht F

The physical Stokes operator commutes with complex scalar multiplication.

theorem CKN.Leray.realStokesOperator_add {t : ℝ} (ht : 0 < t) (F G : ↥RealTensorL2) : realStokesOperator ht (F + G) = realStokesOperator ht F + realStokesOperator ht G

The real Stokes operator preserves addition.

theorem CKN.Leray.realStokesOperator_smul {t : ℝ} (ht : 0 < t) (c : ℝ) (F : ↥RealTensorL2) : realStokesOperator ht (c • F) = c • realStokesOperator ht F

The real Stokes operator commutes with real scalar multiplication.