The energy balance of the forced mild equation

For a tensor curve bounded on [0, T] and a square-integrable force curve, the complex solution v(t) of the linear forced mild equation, whose real part is the right-hand side of eq:reg-mild-forced, satisfies ‖v(t)‖² + 2∫₀ᵗ D(v) ≤ ‖b‖² + 2∫₀ᵗ P(v, F) + 2∫₀ᵗ ⟨Re v, f⟩, where D is the frequency dissipation and P the pairing with the tensor. This is the energy computation of lem:regularised-forced before the transport cancellation.

noncomputable def CKN.Leray.forcedComplexCurve (b : ↥RealVectorL2) (F : ℝ → ↥RealTensorL2) (h : ℝ → ↥RealVectorL2) (s : ℝ) : ↥ComplexVectorL2

The complex solution curve of the linear forced mild equation.

Equations

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

noncomputable def CKN.Leray.forcedMildCurve (b : ↥RealVectorL2) (h : ℝ → ↥RealVectorL2) (F : ℝ → ↥RealTensorL2) (s : ℝ) : ↥RealVectorL2

The right-hand side of eq:reg-mild-forced as a curve on the real line, zero at negative times.

Equations

• CKN.Leray.forcedMildCurve b h F s = if hs : 0 ≤ s then CKN.Leray.forcedMildRHS b h F s hs else 0

noncomputable def CKN.Leray.forcedFourierDissipation (v : ↥ComplexVectorL2) : ℝ

The frequency dissipation ∫ 4π²|ξ|² |v̂(ξ)|² of a complex field.

Equations

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

noncomputable def CKN.Leray.forcedStokesPairing (v : ↥ComplexVectorL2) (G : ↥ComplexTensorL2) : ℝ

The frequency pairing of a complex field with the divergence of a complex tensor field.

Equations

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

theorem CKN.Leray.integrable_sq_jointRep_prod {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (Γ : Foundation.Parabolic.L2Vec3 × ℝ → E) (hΓ : MeasureTheory.StronglyMeasurable Γ) (γ : ℝ → ↥(MeasureTheory.Lp E 2 MeasureTheory.volume)) {t : ℝ} (hrep : ∀ s ∈ Set.Ioc 0 t, (fun (ξ : Foundation.Parabolic.L2Vec3) => Γ (ξ, s)) =ᵐ[MeasureTheory.volume] ↑↑(γ s)) (g : ℝ → ℝ) (hg : MeasureTheory.IntegrableOn g (Set.Ioc 0 t) MeasureTheory.volume) (hbound : ∀ s ∈ Set.Ioc 0 t, ‖γ s‖ ^ 2 ≤ g s) : MeasureTheory.Integrable (fun (p : Foundation.Parabolic.L2Vec3 × ℝ) => ‖Γ p‖ ^ 2) (MeasureTheory.volume.prod (MeasureTheory.volume.restrict (Set.Ioc 0 t)))

A jointly measurable representative of a curve of L² classes whose squared norms are dominated by an integrable function is square integrable on the product.

theorem CKN.Leray.forcedComplexCurve_fourier (b : ↥RealVectorL2) (F : ℝ → ↥RealTensorL2) (h : ℝ → ↥RealVectorL2) {s : ℝ} (hs : 0 ≤ s) : (MeasureTheory.Lp.fourierTransformₗᵢ Foundation.Parabolic.L2Vec3 ComplexVec3) (forcedComplexCurve b F h s) = forcedFourierMild ((MeasureTheory.Lp.fourierTransformₗᵢ Foundation.Parabolic.L2Vec3 ComplexVec3) (complexifyVectorL2 b)) (forcedFourierTensorCurve F) (forcedFourierForceCurve h) s hs

theorem CKN.Leray.forcedMildCurve_eq_realPart (b : ↥RealVectorL2) {F : ℝ → ↥RealTensorL2} (hF : MeasureTheory.StronglyMeasurable F) {h : ℝ → ↥RealVectorL2} (hh : MeasureTheory.StronglyMeasurable h) {s C : ℝ} (hs : 0 ≤ s) (hFC : ∀ r ∈ Set.Ioc 0 s, ‖F r‖ ≤ C) (hH : MeasureTheory.IntegrableOn (fun (r : ℝ) => ‖h r‖) (Set.Ioc 0 s) MeasureTheory.volume) : forcedMildCurve b h F s = realPartVectorL2 (forcedComplexCurve b F h s)

The real part of the complex solution curve is the right-hand side of eq:reg-mild-forced.

theorem CKN.Leray.integrableOn_norm_of_sq {h : ℝ → ↥RealVectorL2} (hh : MeasureTheory.StronglyMeasurable h) {T : ℝ} (hH2 : MeasureTheory.IntegrableOn (fun (s : ℝ) => ‖h s‖ ^ 2) (Set.Ioc 0 T) MeasureTheory.volume) : MeasureTheory.IntegrableOn (fun (s : ℝ) => ‖h s‖) (Set.Ioc 0 T) MeasureTheory.volume

A square-integrable function whose square is integrable over a bounded interval is integrable there.

theorem CKN.Leray.forcedMild_energy_balance (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) {t : ℝ} (ht : 0 ≤ t) (htT : t ≤ T) : (∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc 0 t), MeasureTheory.Integrable (fun (ξ : Foundation.Parabolic.L2Vec3) => forcedFourierLam ξ * ‖↑↑((MeasureTheory.Lp.fourierTransformₗᵢ Foundation.Parabolic.L2Vec3 ComplexVec3) (forcedComplexCurve b F h s)) ξ‖ ^ 2) MeasureTheory.volume) ∧ MeasureTheory.IntegrableOn (fun (s : ℝ) => forcedFourierDissipation (forcedComplexCurve b F h s)) (Set.Ioc 0 t) MeasureTheory.volume ∧ ‖forcedComplexCurve b F h t‖ ^ 2 + 2 * ∫ (s : ℝ) in Set.Ioc 0 t, forcedFourierDissipation (forcedComplexCurve b F h s) ≤ (‖b‖ ^ 2 + 2 * ∫ (s : ℝ) in Set.Ioc 0 t, forcedStokesPairing (forcedComplexCurve b F h s) (complexifyTensorL2 (F s))) + 2 * ∫ (s : ℝ) in Set.Ioc 0 t, inner ℝ (forcedMildCurve b h F s) (h s)

The energy balance of the forced mild equation.