The weak form of one damped frequency #
At a fixed frequency the forced mild equation of lem:regularised-forced is
the damped Duhamel formula y(t) = e^{-λt} y₀ + ∫₀ᵗ e^{-λ(t-s)} g(s) ds.
Against a continuously differentiable test vanishing at both ends of the time
interval it satisfies ∫ ⟨y, -θ' + λθ⟩ = ∫ ⟨g, θ⟩, by integration by parts for
absolutely continuous functions. This is the frequency form of
eq:reg-momentum-forced.
theorem
CKN.Leray.damped_duhamel_test_identity
(lam a0 : ℝ)
(g a θ θ' : ℝ → ℝ)
{T : ℝ}
(hg : IntervalIntegrable g MeasureTheory.volume 0 T)
(ha : ∀ τ ∈ Set.uIcc 0 T, a τ = Real.exp (-lam * τ) * a0 + ∫ (s : ℝ) in 0..τ, Real.exp (-lam * (τ - s)) * g s)
(hθ : ∀ (t : ℝ), HasDerivAt θ (θ' t) t)
(hθ' : Continuous θ')
(h0 : θ 0 = 0)
(hT : θ T = 0)
:
The weak form of a real damped Duhamel formula with integrable source.
theorem
CKN.Leray.damped_duhamel_complexVec3_test_identity
(lam : ℝ)
(y0 : ComplexVec3)
(g y Θ Θ' : ℝ → ComplexVec3)
{T : ℝ}
(hg : IntervalIntegrable g MeasureTheory.volume 0 T)
(hy : ∀ τ ∈ Set.uIcc 0 T, y τ = ↑(Real.exp (-lam * τ)) • y0 + ∫ (s : ℝ) in 0..τ, ↑(Real.exp (-lam * (τ - s))) • g s)
(hΘ : ∀ (t : ℝ), HasDerivAt Θ (Θ' t) t)
(hΘ' : Continuous Θ')
(h0 : Θ 0 = 0)
(hT : Θ T = 0)
:
The weak form of a damped Duhamel formula with values in complex
three-vectors: ∫ Re ⟨y, -Θ' + λΘ⟩ = ∫ Re ⟨g, Θ⟩.
theorem
CKN.Leray.forcedFourierRep_test_identity
{B : Foundation.Parabolic.L2Vec3 → ComplexVec3}
{Fh : Foundation.Parabolic.L2Vec3 × ℝ → ComplexTensor3}
{Hh : Foundation.Parabolic.L2Vec3 × ℝ → ComplexVec3}
(ξ : Foundation.Parabolic.L2Vec3)
{T : ℝ}
(hT : 0 ≤ T)
(hgint :
MeasureTheory.IntegrableOn (fun (s : ℝ) => forcedFourierSource Fh Hh (ξ, s)) (Set.Ioc 0 T) MeasureTheory.volume)
{Θ Θ' : ℝ → ComplexVec3}
(hΘ : ∀ (t : ℝ), HasDerivAt Θ (Θ' t) t)
(hΘ' : Continuous Θ')
(h0 : Θ 0 = 0)
(hTz : Θ T = 0)
:
The weak form of the forced frequency representative at one frequency:
against a test vanishing at 0 and T, ∫ Re ⟨Y, -Θ' + λΘ⟩ = ∫ Re ⟨ℙ̂ g, Θ⟩
with the unprojected source g.