KineticDissipation: mathematical reading route

Mathematical statement

For every finite-dimensional real inner-product E, kappa≥1, symmetric real linear H with (2kappa)^-1 I≤H≤I and every x,p∈E, D_H(x,p)≥Q_kappa(x,p)/(8kappa), where Q_kappa=(1/(2kappa)+1/2)||x||²+inner(x,p)+||p||² and D_H=inner(x,Hx)+2inner(p,Hx)-kappa^-1 inner(x,p)+||p||². With A_H(x,p)=(p,-Hx-p), M_kappa(x,p)=((alpha+1/2)x+p/2,x/2+p), this is exactly -2 inner(M_kappa(x,p),A_H(x,p))≥Q_kappa/(8kappa), hence the full matrix quadratic inequality (4.15). Product inner here is the sum of the two E inner products.

theorem source_kinetic_dissipation {E : Type*} [NormedAddCommGroup E]
    [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
    {kappa : ℝ} (hkappa : 1 ≤ kappa) (H : E →ₗ[ℝ] E) (hH : H.IsSymmetric)
    (hlower : ∀ v, 1/(2*kappa) * ‖v‖^2 ≤ inner ℝ v (H v))
    (hupper : ∀ v, inner ℝ v (H v) ≤ ‖v‖^2) (x p : E) :
    1/(8*kappa) * ((1/(2*kappa)+1/2)*‖x‖^2 + inner ℝ x p + ‖p‖^2) ≤
      inner ℝ x (H x) + 2*inner ℝ p (H x) - 1/kappa*inner ℝ x p + ‖p‖^2

Proof roadmap

1. 1Retain the actual two block operators

   Put alpha=1/(2kappa)∈(0,1/2]. The real full phase form is Q=(alpha+1/2)||x||²+inner(x,p)+||p||². Direct block multiplication for A_H(x,p)=(p,-Hx-p) and M_kappa gives -2 inner(M_kappa z,A_H z)=D_H. Source operator order is precisely comparison of these forms for every phase vector; no stochastic kernel contraction enters.

2. 2Prove the source scalar determinant lower bound

   For an eigenvalue alpha≤lambda≤1, factor lambda-(lambda-alpha)²-alpha=(lambda-alpha)(1+alpha-lambda)≥0. For t=1-alpha/2>0, det(([[lambda,lambda-alpha],[lambda-alpha,1]])-(alpha/2)I)≥0: its determinant is at least alpha(1-lambda)/2+alpha²/4. This exposes the PSD detail behind the source determinant/trace argument.

3. 3Establish actual scalar coercivity

   Complete the square: t[(lambda-alpha/2)u²+2(lambda-alpha)uv+t v²]=(t v+(lambda-alpha)u)²+det*u²≥0. Hence D_lambda≥alpha(u²+v²)/2. Since alpha≤1/2 and (u-v)²≥0, the source M form is ≤2(u²+v²). Thus D_lambda≥alpha Q_lambda/4, the exact source1/(8kappa) factor.

4. 4Derive rather than assume the eigenvalue bounds

   Pinned Mathlib supplies an orthonormal eigenbasis b_i of the real symmetric H. At a unit basis vector, the actual full-space lower/upper quadratic hypotheses and H b_i=lambda_i b_i give alpha≤lambda_i≤1. The basis is internally obtained; no external certificate is supplied. Symmetry yields inner(b_i,Hx)=inner(Hb_i,x)=lambda_i inner(b_i,x).

5. 5Lift every scalar block to the whole E

   Write u_i=inner(b_i,x),v_i=inner(b_i,p). Parseval and the exact inner-product sum identify sum u_i²=||x||², sum v_i²=||p||², sum u_i v_i=inner(x,p), sum lambda_i u_i²=inner(x,Hx) and sum lambda_i u_i v_i=inner(p,Hx). Sum the scalar inequalities and substitute all identities; this includes dimension zero without a nonempty basis hypothesis.

6. 6Recover the precise source constant

   Use kappa≥1 to derive 0<alpha≤1/2. Substitute alpha=1/(2kappa), alpha/4=1/(8kappa),2alpha=1/kappa into the full-E inequality. Only the public source theorem receives admission; its two private proof helpers remain implementation details.