The forced mild equation in frequency variables

The right-hand side of eq:reg-mild-forced is transformed to frequency variables: the heat evolution of the datum, the Stokes Duhamel integral of the tensor, and the heat Duhamel integral of the projected force. The Bochner integral in frequency L² is identified almost everywhere with the pointwise representative forcedFourierRep of lem:regularised-forced.

noncomputable def CKN.Leray.forcedFourierStokesIntegrand (F : ℝ → ↥ComplexTensorL2) (t s : ℝ) : ↥ComplexVectorL2

The frequency-side Stokes Duhamel integrand, zero at and after the evaluation time.

Equations

• CKN.Leray.forcedFourierStokesIntegrand F t s = if hs : s < t then CKN.Leray.stokesFourierMultiplier ⋯ (F s) else 0

noncomputable def CKN.Leray.forcedFourierForceIntegrand (H : ℝ → ↥ComplexVectorL2) (t s : ℝ) : ↥ComplexVectorL2

The frequency-side force Duhamel integrand: the heat multiplier applied to the Leray projection of the transformed force.

Equations

• CKN.Leray.forcedFourierForceIntegrand H t s = if hs : s ≤ t then CKN.Leray.heatMultiplier (t - s) ⋯ • CKN.Leray.lerayFourierMultiplier (H s) else 0

noncomputable def CKN.Leray.forcedFourierMild (b : ↥ComplexVectorL2) (F : ℝ → ↥ComplexTensorL2) (H : ℝ → ↥ComplexVectorL2) (t : ℝ) (ht : 0 ≤ t) : ↥ComplexVectorL2

The frequency-side right-hand side of eq:reg-mild-forced.

Equations

• One or more equations did not get rendered due to their size.

theorem CKN.Leray.measurable_stokesApplyFormula_uncurry : Measurable fun (p : ℝ × Foundation.Parabolic.L2Vec3 × ComplexTensor3) => stokesApplyFormula p.1 p.2.1 p.2.2

The Stokes formula is jointly measurable in time, frequency and tensor.

noncomputable def CKN.Leray.forcedFourierStokesRep (Fh : Foundation.Parabolic.L2Vec3 × ℝ → ComplexTensor3) (t : ℝ) (p : Foundation.Parabolic.L2Vec3 × ℝ) : ComplexVec3

The joint representative of the Stokes Duhamel integrand.

Equations

• CKN.Leray.forcedFourierStokesRep Fh t p = if p.2 < t then CKN.Leray.stokesApplyFormula (t - p.2) p.1 (Fh p) else 0

noncomputable def CKN.Leray.forcedFourierForceRep (Hh : Foundation.Parabolic.L2Vec3 × ℝ → ComplexVec3) (t : ℝ) (p : Foundation.Parabolic.L2Vec3 × ℝ) : ComplexVec3

The joint representative of the force Duhamel integrand.

Equations

• CKN.Leray.forcedFourierForceRep Hh t p = if p.2 ≤ t then CKN.Leray.heatSymbol (t - p.2) p.1 • CKN.Leray.lerayApplyFormula p.1 (Hh p) else 0

theorem CKN.Leray.measurable_forcedFourierStokesRep {Fh : Foundation.Parabolic.L2Vec3 × ℝ → ComplexTensor3} (hFh : Measurable Fh) (t : ℝ) : Measurable (forcedFourierStokesRep Fh t)

theorem CKN.Leray.measurable_forcedFourierForceRep {Hh : Foundation.Parabolic.L2Vec3 × ℝ → ComplexVec3} (hHh : Measurable Hh) (t : ℝ) : Measurable (forcedFourierForceRep Hh t)

theorem CKN.Leray.forcedFourierStokesRep_slice {F : ℝ → ↥ComplexTensorL2} {Fh : Foundation.Parabolic.L2Vec3 × ℝ → ComplexTensor3} (hrep : ∀ (s : ℝ), (fun (ξ : Foundation.Parabolic.L2Vec3) => Fh (ξ, s)) =ᵐ[MeasureTheory.volume] ↑↑(F s)) (t s : ℝ) : (fun (ξ : Foundation.Parabolic.L2Vec3) => forcedFourierStokesRep Fh t (ξ, s)) =ᵐ[MeasureTheory.volume] ↑↑(forcedFourierStokesIntegrand F t s)

Every slice of the Stokes representative represents the Stokes integrand.

theorem CKN.Leray.forcedFourierForceRep_slice {H : ℝ → ↥ComplexVectorL2} {Hh : Foundation.Parabolic.L2Vec3 × ℝ → ComplexVec3} (hrep : ∀ (s : ℝ), (fun (ξ : Foundation.Parabolic.L2Vec3) => Hh (ξ, s)) =ᵐ[MeasureTheory.volume] ↑↑(H s)) (t s : ℝ) : (fun (ξ : Foundation.Parabolic.L2Vec3) => forcedFourierForceRep Hh t (ξ, s)) =ᵐ[MeasureTheory.volume] ↑↑(forcedFourierForceIntegrand H t s)

Every slice of the force representative represents the force integrand.

theorem CKN.Leray.integrableOn_abelKernel (t : ℝ) (ht : 0 ≤ t) : MeasureTheory.IntegrableOn (fun (s : ℝ) => (t - s) ^ (-(1 / 2))) (Set.Ioc 0 t) MeasureTheory.volume

The Abel kernel (t - s)^{-1/2} is integrable on (0, t].

theorem CKN.Leray.stokes_kernel_eq_rpow {τ : ℝ} (hτ : 0 < τ) : 1 / √(2 * Real.exp 1 * τ) = 1 / √(2 * Real.exp 1) * τ ^ (-(1 / 2))

theorem CKN.Leray.integrableOn_forcedFourierStokesIntegrand {F : ℝ → ↥ComplexTensorL2} {Fh : Foundation.Parabolic.L2Vec3 × ℝ → ComplexTensor3} (hFh : Measurable Fh) (hrep : ∀ (s : ℝ), (fun (ξ : Foundation.Parabolic.L2Vec3) => Fh (ξ, s)) =ᵐ[MeasureTheory.volume] ↑↑(F s)) {t C : ℝ} (ht : 0 ≤ t) (hFC : ∀ s ∈ Set.Ioc 0 t, ‖F s‖ ≤ C) : MeasureTheory.IntegrableOn (forcedFourierStokesIntegrand F t) (Set.Ioc 0 t) MeasureTheory.volume

The Stokes Duhamel integrand of a bounded tensor curve is integrable.

theorem CKN.Leray.integrableOn_forcedFourierForceIntegrand {H : ℝ → ↥ComplexVectorL2} {Hh : Foundation.Parabolic.L2Vec3 × ℝ → ComplexVec3} (hHh : Measurable Hh) (hrep : ∀ (s : ℝ), (fun (ξ : Foundation.Parabolic.L2Vec3) => Hh (ξ, s)) =ᵐ[MeasureTheory.volume] ↑↑(H s)) {t : ℝ} (hH : MeasureTheory.IntegrableOn (fun (s : ℝ) => ‖H s‖) (Set.Ioc 0 t) MeasureTheory.volume) : MeasureTheory.IntegrableOn (forcedFourierForceIntegrand H t) (Set.Ioc 0 t) MeasureTheory.volume

The force Duhamel integrand of an integrable force curve is integrable.

theorem CKN.Leray.heatMultiplier_smul_ae_eq (t : ℝ) (ht : 0 ≤ t) (v : ↥ComplexVectorL2) : ↑↑(heatMultiplier t ht • v) =ᵐ[MeasureTheory.volume] fun (ξ : Foundation.Parabolic.L2Vec3) => heatSymbol t ξ • ↑↑v ξ

The heat multiplier acts pointwise by the heat symbol.

theorem CKN.Leray.forcedFourierMild_ae_eq_rep (b : ↥ComplexVectorL2) (hb : ∀ᵐ (ξ : Foundation.Parabolic.L2Vec3), (leraySymbol ξ) (↑↑b ξ) = ↑↑b ξ) {F : ℝ → ↥ComplexTensorL2} {Fh : Foundation.Parabolic.L2Vec3 × ℝ → ComplexTensor3} (hFh : Measurable Fh) (hrepF : ∀ (s : ℝ), (fun (ξ : Foundation.Parabolic.L2Vec3) => Fh (ξ, s)) =ᵐ[MeasureTheory.volume] ↑↑(F s)) {H : ℝ → ↥ComplexVectorL2} {Hh : Foundation.Parabolic.L2Vec3 × ℝ → ComplexVec3} (hHh : Measurable Hh) (hrepH : ∀ (s : ℝ), (fun (ξ : Foundation.Parabolic.L2Vec3) => Hh (ξ, s)) =ᵐ[MeasureTheory.volume] ↑↑(H s)) {t C : ℝ} (ht : 0 ≤ t) (hFC : ∀ s ∈ Set.Ioc 0 t, ‖F s‖ ≤ C) (hH : MeasureTheory.IntegrableOn (fun (s : ℝ) => ‖H s‖) (Set.Ioc 0 t) MeasureTheory.volume) : ↑↑(forcedFourierMild b F H t ht) =ᵐ[MeasureTheory.volume] fun (ξ : Foundation.Parabolic.L2Vec3) => forcedFourierRep (fun (η : Foundation.Parabolic.L2Vec3) => (leraySymbol η) (↑↑b η)) Fh Hh (ξ, t)

The frequency-side right-hand side of eq:reg-mild-forced agrees almost everywhere with the pointwise representative.