§13 (C), Corollary IV₁ — two RKHS norms on the same class are equivalent

Proved

AronszajnRK.Inclusion.equivalent_norms_same_class

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

p2o-batch-pfp1bp2o-gran-per-chapterp2o-plan-paperp2o-v1reproducing-kernelsrkhs

Let $\|\cdot\|$ and $\|\cdot\|_1$ be two norms each giving the same (R.K.)-class $F$ of complex functions on $X$ the structure of a Hilbert space with a reproducing kernel. Then there are constants $m>0$ and $M>0$ such that

m\,\|f\| \ \le\ \|f\|_1 \ \le\ M\,\|f\| \qquad\text{for every } f\in F .

In particular, the Hilbert-space topology of an (R.K.)-class does not depend on the choice of admissible norm.

Preamble

import Mathlib

Formal statement

namespace AronszajnRK.Inclusion

/-- Aronszajn, *Theory of Reproducing Kernels*, Trans. Amer. Math. Soc. 68 (1950), §13 (C),
Corollary IV₁, p. 383 (PDF p. 47). Let `‖ ‖` and `‖ ‖₁` be two norms corresponding to the same
(R.K.)-class `F`. There exist two positive constants `m` and `M` such that
`m‖f‖ ≤ ‖f‖₁ ≤ M‖f‖` for `f ∈ F`. The two norms are those of RKHSs `H` and `H₁` with the same
class of functions. -/
theorem equivalent_norms_same_class {X H H₁ : Type*}
    [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] [RKHS ℂ H X ℂ]
    [NormedAddCommGroup H₁] [InnerProductSpace ℂ H₁] [CompleteSpace H₁] [RKHS ℂ H₁ X ℂ]
    (heq : Set.range (fun f₁ : H₁ => ⇑f₁) = Set.range (fun f : H => ⇑f)) :
    ∃ m M : ℝ, 0 < m ∧ 0 < M ∧
      ∀ (f : H) (f₁ : H₁), ⇑f = ⇑f₁ → m * ‖f‖ ≤ ‖f₁‖ ∧ ‖f₁‖ ≤ M * ‖f‖ := by sorry

end AronszajnRK.Inclusion

Source

Aronszajn, Theory of Reproducing Kernels, Trans. Amer. Math. Soc. 68 (1950), p. 383, §13 (C), Corollary IV₁

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