Strong Convergence on the Range of the Generator

Proved

FunctionalInequalities.Analysis.Semigroup.Generated.tendsto_apply_adjointComp_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This is an auxiliary strong-convergence statement for the generated semigroup.

Let $H_0,H_1$ be real complete inner-product spaces, let $T:H_0\to H_1$ be closed with dense domain, and write $A=T^\dagger T$ . For every $y\in D(A)$ ,

P_t(Ay)\longrightarrow0\qquad(t\to\infty).

Thus the semigroup converges strongly to zero on vectors in the range of $A$ .

This result is the basic range-level convergence estimate used in extending convergence to the closure of the range.

Formalization Note. The limit is expressed as Tendsto along real t tending to atTop; the semigroup is Generated.apply T hT hd.

Original Lean declaration header

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

theorem tendsto_apply_adjointComp (y : (adjointComp T).domain) :
    Tendsto (fun t : ℝ => apply T hT hd t (adjointComp T y)) atTop (𝓝 0)

Module navigation

Module: Analysis/Semigroup/Generated/Convergence.

Definition modules: Analysis/Semigroup/AdjointComp, Analysis/Semigroup/Generated/Basic.

Previous: mem_closure_range_of_inner_eq_zero · Next: tendsto_apply_of_mem_closure_range.

Source excerpt, lines 144–145 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_Semigroup_Generated_Convergence

open Filter Topology Set
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₀))

Formal statement


theorem FunctionalInequalities.Analysis.Semigroup.Generated.tendsto_apply_adjointComp_readable (y : (adjointComp T).domain) :
    Tendsto (fun t : ℝ => apply T hT hd t (adjointComp T y)) atTop (𝓝 0) := by sorry

Source

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

View graph