§7, p. 354 — $\ll$ is a partial order on positive matrices

Proved

AronszajnRK.Inclusion.dominated_partialOrder

by mikedeng1 · Oct 4, 2026 · Mathlib 0df444a (Lean v4.33.1)

p2o-batch-pfp1bp2o-gran-per-chapterp2o-plan-paperp2o-v1positive-matricesreproducing-kernels

Let $K_1, K_2, K_3 : X\times X\to\mathbb C$ be positive matrices on a set $X$ . Then

if $K_1\ll K_2$ and $K_2\ll K_3$ , then $K_1\ll K_3$ ;
if $K_1\ll K_2$ and $K_2\ll K_1$ , then $K_1 = K_2$ (as functions on $X\times X$ ).

K_1\ll K_2\ll K_3 \implies K_1\ll K_3, \qquad K_1\ll K_2,\ K_2\ll K_1 \implies K_1=K_2 .

Together with reflexivity, which is immediate, this shows that $\ll$ is a partial ordering of the class of positive matrices; the inclusion theorems for reproducing kernel classes are statements about this order.

Preamble

import Mathlib
import Definitions.Def_AronszajnRK_Limits_KernelLE

open scoped ComplexOrder

Formal statement

namespace AronszajnRK.Inclusion

/-- Aronszajn, *Theory of Reproducing Kernels*, Trans. Amer. Math. Soc. 68 (1950), §7, p. 354
(PDF p. 18), unnumbered: on positive matrices, `≪` is a partial ordering. From
`K₁ ≪ K₂ ≪ K₃` it follows that `K₁ ≪ K₃`; if `K₁ ≪ K₂` and `K₂ ≪ K₁`, then `K₁ = K₂`. -/
theorem dominated_partialOrder {X : Type*} (K₁ K₂ K₃ : X → X → ℂ)
    (h₁ : (Matrix.of K₁).PosSemidef) (h₂ : (Matrix.of K₂).PosSemidef)
    (h₃ : (Matrix.of K₃).PosSemidef) :
    (AronszajnRK.Limits.KernelLE K₁ K₂ → AronszajnRK.Limits.KernelLE K₂ K₃ → AronszajnRK.Limits.KernelLE K₁ K₃) ∧
      (AronszajnRK.Limits.KernelLE K₁ K₂ → AronszajnRK.Limits.KernelLE K₂ K₁ → K₁ = K₂) := by sorry

end AronszajnRK.Inclusion

Source

Aronszajn, Theory of Reproducing Kernels, Trans. Amer. Math. Soc. 68 (1950), p. 354, §7 (unnumbered remark after (1))

Human review

Endorsed by Shuze Chen · Oct 5, 2026
Confirmed by the moderator at approval.
Endorsed by mikedeng1 · Oct 5, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

§7, p. 354 — ≪\ll≪ is a partial order on positive matrices

§7, p. 354 — $\ll$ is a partial order on positive matrices