The energy identity of one damped frequency

At a fixed frequency the mild equation of lem:regularised-forced is the damped Duhamel formula y(t) = e^{-λt} y₀ + ∫₀ᵗ e^{-λ(t-s)} g(s) ds with an integrable source. Its squared modulus satisfies the energy identity |y(t)|² + 2λ ∫₀ᵗ |y|² = |y₀|² + 2 ∫₀ᵗ Re ⟨y, g⟩, first for real components through the fundamental theorem of calculus for absolutely continuous functions, then for complex three-vectors.

theorem CKN.Leray.damped_duhamel_sq_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) : a t ^ 2 + 2 * lam * ∫ (s : ℝ) in 0..t, a s ^ 2 = a0 ^ 2 + 2 * ∫ (s : ℝ) in 0..t, a s * g s

The energy identity for a real damped Duhamel formula with integrable source.

theorem CKN.Leray.damped_duhamel_continuousOn (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) : ContinuousOn a (Set.uIcc 0 t)

A real damped Duhamel formula with integrable source is continuous on the time interval.

noncomputable def CKN.Leray.complexVec3RealCoord (k : Fin 3 × Bool) : ComplexVec3 →L[ℝ] ℝ

The real and imaginary parts of the coordinates of a complex three-vector, as real continuous linear functionals.

Equations

• CKN.Leray.complexVec3RealCoord k = (if k.2 = true then Complex.reCLM else Complex.imCLM) ∘SL ContinuousLinearMap.restrictScalars ℝ (PiLp.proj 2 (fun (x : Fin 3) => ℂ) k.1)

theorem CKN.Leray.complexVec3RealCoord_true (i : Fin 3) (x : ComplexVec3) : (complexVec3RealCoord (i, true)) x = (x.ofLp i).re

theorem CKN.Leray.complexVec3RealCoord_false (i : Fin 3) (x : ComplexVec3) : (complexVec3RealCoord (i, false)) x = (x.ofLp i).im

theorem CKN.Leray.complexVec3_norm_sq_eq_sum_realCoord (x : ComplexVec3) : ‖x‖ ^ 2 = ∑ k : Fin 3 × Bool, (complexVec3RealCoord k) x ^ 2

theorem CKN.Leray.complexVec3_inner_re_eq_sum_realCoord (x y : ComplexVec3) : (inner ℂ x y).re = ∑ k : Fin 3 × Bool, (complexVec3RealCoord k) x * (complexVec3RealCoord k) y

theorem CKN.Leray.damped_duhamel_complexVec3_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) : ‖y t‖ ^ 2 + 2 * lam * ∫ (s : ℝ) in 0..t, ‖y s‖ ^ 2 = ‖y0‖ ^ 2 + 2 * ∫ (s : ℝ) in 0..t, (inner ℂ (y s) (g s)).re

The energy identity for a damped Duhamel formula with values in complex three-vectors: ‖y(t)‖² + 2λ ∫₀ᵗ ‖y‖² = ‖y₀‖² + 2 ∫₀ᵗ Re ⟨y, g⟩.