Prove2Me

§13 (C), Corollary IV₃ — F1=FF_1 = F iff mK≪K1≪MKmK \ll K_1 \ll MK

Proved
AronszajnRK.Inclusion.eq_class_iff_kernel_two_sided

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

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

Let KK and K1K_1 be positive matrices on a set XX and FF, F1F_1 the corresponding classes of complex functions. Then

F1=F  ⟺  there are constants m>0, M>0 with mK≪K1≪MK.F_1 = F \iff \text{there are constants } m>0,\ M>0 \text{ with } mK \ll K_1 \ll MK .

Two kernels thus define the same function class exactly when each is dominated by a multiple of the other.

Formalization Note As for Corollary IV₂: stated for arbitrary complex RKHS instances HH, H1H_1 with scalar kernels KK, K1K_1; "F1=FF_1 = F" is equality of their sets of functions.

Preamble
import Mathlib
import Definitions.Def_AronszajnRK_Sum_kernelFn
import Definitions.Def_AronszajnRK_Limits_KernelLE
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). Under the hypotheses of Corollary IV₂ (`K`, `K₁` positive
matrices, `F`, `F₁` the corresponding classes), in order that `F₁ = F` it is necessary and
sufficient that there exist two positive constants `m` and `M` such that `mK ≪ K₁ ≪ MK`.
Stated, as Corollary IV₂, for arbitrary complex RKHSs `H`, `H₁` with kernels `K`, `K₁`. -/
theorem eq_class_iff_kernel_two_sided {X H H₁ : Type*}
    [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] [RKHS ℂ H X ℂ]
    [NormedAddCommGroup H₁] [InnerProductSpace ℂ H₁] [CompleteSpace H₁] [RKHS ℂ H₁ X ℂ] :
    Set.range (fun f₁ : H₁ => ⇑f₁) = Set.range (fun f : H => ⇑f) ↔
      ∃ m M : ℝ, 0 < m ∧ 0 < M ∧
        AronszajnRK.Limits.KernelLE (fun x y => (m : ℂ) * AronszajnRK.Sum.kernelFn H x y) (AronszajnRK.Sum.kernelFn H₁) ∧
        AronszajnRK.Limits.KernelLE (AronszajnRK.Sum.kernelFn H₁) (fun x y => (M : ℂ) * AronszajnRK.Sum.kernelFn H x y) := 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