The forced mild solution is divergence free #
The frequency representative of eq:reg-mild-forced lies in the range of the
Leray symbol at almost every frequency, so its transform is orthogonal to the
frequency and the real part of the solution is weakly divergence free at
every time, as asserted in lem:regularised-forced.
theorem
CKN.Leray.leraySymbol_forcedFourierRep
{B : Foundation.Parabolic.L2Vec3 → ComplexVec3}
{Fh : Foundation.Parabolic.L2Vec3 × ℝ → ComplexTensor3}
{Hh : Foundation.Parabolic.L2Vec3 × ℝ → ComplexVec3}
(hFh : Measurable Fh)
(hHh : Measurable Hh)
(hBP : ∀ (ξ : Foundation.Parabolic.L2Vec3), (leraySymbol ξ) (B ξ) = B ξ)
(ξ : Foundation.Parabolic.L2Vec3)
{s : ℝ}
(hgint :
MeasureTheory.IntegrableOn (fun (r : ℝ) => forcedFourierSource Fh Hh (ξ, r)) (Set.Ioc 0 s) MeasureTheory.volume)
:
At a frequency where the source is integrable, the representative lies in the range of the Leray symbol.
theorem
CKN.Leray.forcedComplexCurve_fourierOrthogonal
(b : ↥RealVectorL2)
(hb : RegularizedMildJData b)
{F : ℝ → ↥RealTensorL2}
(hF : MeasureTheory.StronglyMeasurable F)
{h : ℝ → ↥RealVectorL2}
(hh : MeasureTheory.StronglyMeasurable h)
{T C : ℝ}
(hFC : ∀ s ∈ Set.Ioc 0 T, ‖F s‖ ≤ C)
(hH2 : MeasureTheory.IntegrableOn (fun (s : ℝ) => ‖h s‖ ^ 2) (Set.Ioc 0 T) MeasureTheory.volume)
{s : ℝ}
(hs : 0 ≤ s)
(hsT : s ≤ T)
:
∀ᵐ (ξ : Foundation.Parabolic.L2Vec3), inner ℂ (complexifyFrequency ξ)
(↑↑((MeasureTheory.Lp.fourierTransformₗᵢ Foundation.Parabolic.L2Vec3 ComplexVec3) (forcedComplexCurve b F h s))
ξ) = 0
The transform of the complex solution is orthogonal to the frequency.
theorem
CKN.Leray.forcedMildCurve_mildJData
(b : ↥RealVectorL2)
(hb : RegularizedMildJData b)
{F : ℝ → ↥RealTensorL2}
(hF : MeasureTheory.StronglyMeasurable F)
{h : ℝ → ↥RealVectorL2}
(hh : MeasureTheory.StronglyMeasurable h)
{T C : ℝ}
(hFC : ∀ s ∈ Set.Ioc 0 T, ‖F s‖ ≤ C)
(hH2 : MeasureTheory.IntegrableOn (fun (s : ℝ) => ‖h s‖ ^ 2) (Set.Ioc 0 T) MeasureTheory.volume)
{s : ℝ}
(hs : 0 ≤ s)
(hsT : s ≤ T)
:
RegularizedMildJData (forcedMildCurve b h F s)
The forced mild solution takes values in the divergence-free space J.