The frequency representative of the forced regularized solution #
On a bounded time interval the forced regularized solution of
lem:regularised-forced has a jointly measurable frequency representative
given by the Duhamel formula of eq:reg-mild-forced: its slices are the
transforms of complex fields whose real parts are the solution, the tensor
and force representatives are the transforms of the regularized tensor and of
the force, and all three are square integrable in frequency and time.
theorem
CKN.Leray.forcedMild_fourier_representation
(b : ↥RealVectorL2)
(hb : RegularizedMildJData b)
{F : ℝ → ↥RealTensorL2}
(hF : MeasureTheory.StronglyMeasurable F)
{h : ℝ → ↥RealVectorL2}
(hh : MeasureTheory.StronglyMeasurable h)
{T C : ℝ}
(hC : 0 ≤ C)
(hFC : ∀ s ∈ Set.Ioc 0 T, ‖F s‖ ≤ C)
(hH2 : MeasureTheory.IntegrableOn (fun (s : ℝ) => ‖h s‖ ^ 2) (Set.Ioc 0 T) MeasureTheory.volume)
:
∃ (B : Foundation.Parabolic.L2Vec3 → ComplexVec3) (Fh : Foundation.Parabolic.L2Vec3 × ℝ → ComplexTensor3) (Hh :
Foundation.Parabolic.L2Vec3 × ℝ → ComplexVec3),
Measurable B ∧ Measurable Fh ∧ Measurable Hh ∧ MeasureTheory.Integrable (fun (p : Foundation.Parabolic.L2Vec3 × ℝ) => ‖forcedFourierRep B Fh Hh p‖ ^ 2)
(MeasureTheory.volume.prod (MeasureTheory.volume.restrict (Set.Ioc 0 T))) ∧ MeasureTheory.Integrable (fun (p : Foundation.Parabolic.L2Vec3 × ℝ) => ‖Fh p‖ ^ 2)
(MeasureTheory.volume.prod (MeasureTheory.volume.restrict (Set.Ioc 0 T))) ∧ MeasureTheory.Integrable (fun (p : Foundation.Parabolic.L2Vec3 × ℝ) => ‖Hh p‖ ^ 2)
(MeasureTheory.volume.prod (MeasureTheory.volume.restrict (Set.Ioc 0 T))) ∧ (∀ s ∈ Set.Ioc 0 T,
(fun (ξ : Foundation.Parabolic.L2Vec3) => forcedFourierRep B Fh Hh (ξ, s)) =ᵐ[MeasureTheory.volume]
↑↑((MeasureTheory.Lp.fourierTransformₗᵢ Foundation.Parabolic.L2Vec3 ComplexVec3)
(forcedComplexCurve b F h s))) ∧ (∀ (s : ℝ),
(fun (ξ : Foundation.Parabolic.L2Vec3) => Fh (ξ, s)) =ᵐ[MeasureTheory.volume]
↑↑(forcedFourierTensorCurve F s)) ∧ ∀ (s : ℝ),
(fun (ξ : Foundation.Parabolic.L2Vec3) => Hh (ξ, s)) =ᵐ[MeasureTheory.volume]
↑↑(forcedFourierForceCurve h s)
A jointly measurable frequency representative of the forced mild curve.
theorem
CKN.Leray.forcedReg_fourier_representation
(ρ : RegMollifierProfile)
(ε : ℝ)
(hε : 0 < ε)
{a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3}
(ha : IsInJ a)
{f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}
(hf : IsLocallySquareIntegrableForce f)
{T : ℝ}
(hT : 0 ≤ T)
:
∃ (B : Foundation.Parabolic.L2Vec3 → ComplexVec3) (Fh : Foundation.Parabolic.L2Vec3 × ℝ → ComplexTensor3) (Hh :
Foundation.Parabolic.L2Vec3 × ℝ → ComplexVec3),
Measurable B ∧ Measurable Fh ∧ Measurable Hh ∧ MeasureTheory.Integrable (fun (p : Foundation.Parabolic.L2Vec3 × ℝ) => ‖forcedFourierRep B Fh Hh p‖ ^ 2)
(MeasureTheory.volume.prod (MeasureTheory.volume.restrict (Set.Ioc 0 T))) ∧ MeasureTheory.Integrable (fun (p : Foundation.Parabolic.L2Vec3 × ℝ) => ‖Fh p‖ ^ 2)
(MeasureTheory.volume.prod (MeasureTheory.volume.restrict (Set.Ioc 0 T))) ∧ MeasureTheory.Integrable (fun (p : Foundation.Parabolic.L2Vec3 × ℝ) => ‖Hh p‖ ^ 2)
(MeasureTheory.volume.prod (MeasureTheory.volume.restrict (Set.Ioc 0 T))) ∧ (∀ s ∈ Set.Ioc 0 T,
∃ (Z : ↥ComplexVectorL2),
realPartVectorL2 Z = forcedRegCurve ρ ε hε ha hf s ∧ (fun (ξ : Foundation.Parabolic.L2Vec3) =>
forcedFourierRep B Fh Hh (ξ, s)) =ᵐ[MeasureTheory.volume]
↑↑((MeasureTheory.Lp.fourierTransformₗᵢ Foundation.Parabolic.L2Vec3 ComplexVec3) Z)) ∧ (∀ s ∈ Set.Ioc 0 T,
(fun (ξ : Foundation.Parabolic.L2Vec3) => Fh (ξ, s)) =ᵐ[MeasureTheory.volume]
↑↑((MeasureTheory.Lp.fourierTransformₗᵢ Foundation.Parabolic.L2Vec3 ComplexTensor3)
(complexifyTensorL2 (regularizedMildTensor ρ ε hε (forcedRegCurve ρ ε hε ha hf s))))) ∧ ∀ (s : ℝ),
(fun (ξ : Foundation.Parabolic.L2Vec3) => Hh (ξ, s)) =ᵐ[MeasureTheory.volume]
↑↑((MeasureTheory.Lp.fourierTransformₗᵢ Foundation.Parabolic.L2Vec3 ComplexVec3)
(complexifyVectorL2 (forcedForceSlice (forcedForceMod f hf) s)))
The frequency representative of the forced regularized solution on
(0, T].