The weak form of the forced frequency representative

Integrating the one-frequency weak form over all frequencies, against a family of tests with square-integrable transforms, gives the frequency form of eq:reg-momentum-forced: for the time derivative Φₜ and the damped symbol λΦ of the test, -∫∫ Re⟨Y, Φₜ⟩ + ∫∫ Re⟨Y, λΦ⟩ equals the pairing of the divergence source and the force with the Leray projection of the test.

theorem CKN.Leray.norm_lam_smul (ξ : Foundation.Parabolic.L2Vec3) (z : ComplexVec3) : ‖↑(forcedFourierLam ξ) • z‖ = forcedFourierLam ξ * ‖z‖

theorem CKN.Leray.abs_re_inner_divergence_leray_le (ξ : Foundation.Parabolic.L2Vec3) (F : ComplexTensor3) (z : ComplexVec3) : |(inner ℂ (-((2 * ↑Real.pi * Complex.I) • (tensorDivergenceLinear ξ) F)) ((leraySymbol ξ) z)).re| ≤ (‖F‖ ^ 2 + (‖z‖ ^ 2 + (forcedFourierLam ξ * ‖z‖) ^ 2) / 2) / 2

The pairing of the divergence source with the projected test is controlled by the tensor and the test with its damped symbol.

theorem CKN.Leray.abs_re_inner_leray_le (ξ : Foundation.Parabolic.L2Vec3) (h z : ComplexVec3) : |(inner ℂ h ((leraySymbol ξ) z)).re| ≤ (‖h‖ ^ 2 + ‖z‖ ^ 2) / 2

theorem CKN.Leray.integrable_slice_of_sq {E : Type} [NormedAddCommGroup E] [MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E] {T : ℝ} {f : Foundation.Parabolic.L2Vec3 × ℝ → E} (hf : Measurable f) (ξ : Foundation.Parabolic.L2Vec3) (hsq : MeasureTheory.Integrable (fun (s : ℝ) => ‖f (ξ, s)‖ ^ 2) (MeasureTheory.volume.restrict (Set.Ioc 0 T))) : MeasureTheory.Integrable (fun (s : ℝ) => ‖f (ξ, s)‖) (MeasureTheory.volume.restrict (Set.Ioc 0 T))

A time-square-integrable slice on a bounded interval is time-integrable.

theorem CKN.Leray.forcedFourierRep_weak_identity {B : Foundation.Parabolic.L2Vec3 → ComplexVec3} {Fh : Foundation.Parabolic.L2Vec3 × ℝ → ComplexTensor3} {Hh : Foundation.Parabolic.L2Vec3 × ℝ → ComplexVec3} (hBm : Measurable B) (hFh : Measurable Fh) (hHh : Measurable Hh) {T : ℝ} (hT : 0 ≤ T) {Φ Φt : Foundation.Parabolic.L2Vec3 × ℝ → ComplexVec3} (hΦm : Measurable Φ) (hΦtm : Measurable Φt) (hderiv : ∀ (ξ : Foundation.Parabolic.L2Vec3) (t : ℝ), HasDerivAt (fun (s : ℝ) => Φ (ξ, s)) (Φt (ξ, t)) t) (hcont : ∀ (ξ : Foundation.Parabolic.L2Vec3), Continuous fun (t : ℝ) => Φt (ξ, t)) (h0 : ∀ (ξ : Foundation.Parabolic.L2Vec3), Φ (ξ, 0) = 0) (hTz : ∀ (ξ : Foundation.Parabolic.L2Vec3), Φ (ξ, T) = 0) (hY : MeasureTheory.Integrable (fun (p : Foundation.Parabolic.L2Vec3 × ℝ) => ‖forcedFourierRep B Fh Hh p‖ ^ 2) (MeasureTheory.volume.prod (MeasureTheory.volume.restrict (Set.Ioc 0 T)))) (hF2 : MeasureTheory.Integrable (fun (p : Foundation.Parabolic.L2Vec3 × ℝ) => ‖Fh p‖ ^ 2) (MeasureTheory.volume.prod (MeasureTheory.volume.restrict (Set.Ioc 0 T)))) (hH2 : MeasureTheory.Integrable (fun (p : Foundation.Parabolic.L2Vec3 × ℝ) => ‖Hh p‖ ^ 2) (MeasureTheory.volume.prod (MeasureTheory.volume.restrict (Set.Ioc 0 T)))) (hΦ2 : MeasureTheory.Integrable (fun (p : Foundation.Parabolic.L2Vec3 × ℝ) => ‖Φ p‖ ^ 2) (MeasureTheory.volume.prod (MeasureTheory.volume.restrict (Set.Ioc 0 T)))) (hΦt2 : MeasureTheory.Integrable (fun (p : Foundation.Parabolic.L2Vec3 × ℝ) => ‖Φt p‖ ^ 2) (MeasureTheory.volume.prod (MeasureTheory.volume.restrict (Set.Ioc 0 T)))) (hΛ2 : MeasureTheory.Integrable (fun (p : Foundation.Parabolic.L2Vec3 × ℝ) => (forcedFourierLam p.1 * ‖Φ p‖) ^ 2) (MeasureTheory.volume.prod (MeasureTheory.volume.restrict (Set.Ioc 0 T)))) : MeasureTheory.IntegrableOn (fun (t : ℝ) => ∫ (ξ : Foundation.Parabolic.L2Vec3), (inner ℂ (forcedFourierRep B Fh Hh (ξ, t)) (Φt (ξ, t))).re) (Set.Ioc 0 T) MeasureTheory.volume ∧ MeasureTheory.IntegrableOn (fun (t : ℝ) => ∫ (ξ : Foundation.Parabolic.L2Vec3), (inner ℂ (forcedFourierRep B Fh Hh (ξ, t)) (↑(forcedFourierLam ξ) • Φ (ξ, t))).re) (Set.Ioc 0 T) MeasureTheory.volume ∧ MeasureTheory.IntegrableOn (fun (t : ℝ) => ∫ (ξ : Foundation.Parabolic.L2Vec3), (inner ℂ (-((2 * ↑Real.pi * Complex.I) • (tensorDivergenceLinear ξ) (Fh (ξ, t)))) ((leraySymbol ξ) (Φ (ξ, t)))).re) (Set.Ioc 0 T) MeasureTheory.volume ∧ MeasureTheory.IntegrableOn (fun (t : ℝ) => ∫ (ξ : Foundation.Parabolic.L2Vec3), (inner ℂ (Hh (ξ, t)) ((leraySymbol ξ) (Φ (ξ, t)))).re) (Set.Ioc 0 T) MeasureTheory.volume ∧ (-∫ (t : ℝ) in Set.Ioc 0 T, ∫ (ξ : Foundation.Parabolic.L2Vec3), (inner ℂ (forcedFourierRep B Fh Hh (ξ, t)) (Φt (ξ, t))).re) + ∫ (t : ℝ) in Set.Ioc 0 T, ∫ (ξ : Foundation.Parabolic.L2Vec3), (inner ℂ (forcedFourierRep B Fh Hh (ξ, t)) (↑(forcedFourierLam ξ) • Φ (ξ, t))).re = (∫ (t : ℝ) in Set.Ioc 0 T, ∫ (ξ : Foundation.Parabolic.L2Vec3), (inner ℂ (-((2 * ↑Real.pi * Complex.I) • (tensorDivergenceLinear ξ) (Fh (ξ, t)))) ((leraySymbol ξ) (Φ (ξ, t)))).re) + ∫ (t : ℝ) in Set.Ioc 0 T, ∫ (ξ : Foundation.Parabolic.L2Vec3), (inner ℂ (Hh (ξ, t)) ((leraySymbol ξ) (Φ (ξ, t)))).re

The frequency form of eq:reg-momentum-forced.