Kernel Membership from Orthogonality to the Operator Range

Proved

FunctionalInequalities.Analysis.Semigroup.Generated.exists_mem_adjointComp_domain_of_inner_eq_zero_readable

by Lazyfill · Oct 26, 2026 · Mathlib 0df444a (Lean v4.33.1)

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This is a self-adjointness lemma for $A=T^\dagger T$ .

Let $H_0,H_1$ be complete real Hilbert spaces, let $T:H_0\to H_1$ be closed, and assume $D(T)$ is dense in $H_0$ . For $q\in H_0$ , suppose

\langle q,Ay\rangle=0\quad\text{for every }y\in D(A),

where $A=\operatorname{adjointComp}(T)$ . Then there exists a domain witness showing that $q\in D(A)$ and

Aq=0.

This technical result identifies vectors orthogonal to the range of the self-adjoint operator with its kernel.

Original Lean declaration header

Within namespace FunctionalInequalities.Analysis.Semigroup.Generated. Shown in its original module context. Proof omitted.

theorem exists_mem_adjointComp_domain_of_inner_eq_zero (q : H₀)
    (hq : ∀ y : (adjointComp T).domain, ⟪q, adjointComp T y⟫ = 0) :
    ∃ h : q ∈ (adjointComp T).domain, adjointComp T ⟨q, h⟩ = 0

Module navigation

Module: Analysis/Semigroup/Generated/Convergence.

Definition modules: Analysis/Semigroup/AdjointComp.

Next: mem_closure_range_of_inner_eq_zero.

Source excerpt, lines 64–66 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_Semigroup_Generated_Convergence

open scoped RealInnerProductSpace LinearPMap
variable {H₀ H₁ : Type*} [NormedAddCommGroup H₀] [InnerProductSpace ℝ H₀] [CompleteSpace H₀]
  [NormedAddCommGroup H₁] [InnerProductSpace ℝ H₁] [CompleteSpace H₁]
  (T : H₀ →ₗ.[ℝ] H₁) (hT : T.IsClosed) (hd : Dense (T.domain : Set H₀))
include hT hd

Formal statement


theorem FunctionalInequalities.Analysis.Semigroup.Generated.exists_mem_adjointComp_domain_of_inner_eq_zero_readable (q : H₀)
    (hq : ∀ y : (adjointComp T).domain, ⟪q, adjointComp T y⟫ = 0) :
    ∃ h : q ∈ (adjointComp T).domain, adjointComp T ⟨q, h⟩ = 0 := by sorry

Source

Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/Analysis/Semigroup/Generated/Convergence.lean#L62-L98 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.Analysis.Semigroup.Generated.Convergence`, declaration `FunctionalInequalities.Analysis.Semigroup.Generated.exists_mem_adjointComp_domain_of_inner_eq_zero`; the repository is private at upload time).

View graph