Strong Convergence on the Closure of the Generator Range

Proved

FunctionalInequalities.Analysis.Semigroup.Generated.tendsto_apply_of_mem_closure_range_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$ . If $g\in H_0$ belongs to the closure of the range of $A$ , then

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

The statement provides the closure-extension step for ergodic convergence of the semigroup.

Formalization Note. Membership is in closure (Set.range fun y => adjointComp T y), and convergence is expressed in the norm topology on $H_0$ .

Original Lean declaration header

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

theorem tendsto_apply_of_mem_closure_range {g : H₀}
    (hg : g ∈ closure (Set.range fun y : (adjointComp T).domain => adjointComp T y)) :
    Tendsto (fun t : ℝ => apply T hT hd t g) atTop (𝓝 0)

Module navigation

Module: Analysis/Semigroup/Generated/Convergence.

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

Supporting theorems: tendsto_apply_adjointComp.

Previous: tendsto_apply_adjointComp.

Source excerpt, lines 167–169 · 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_of_mem_closure_range_readable {g : H₀}
    (hg : g ∈ closure (Set.range fun y : (adjointComp T).domain => adjointComp T y)) :
    Tendsto (fun t : ℝ => apply T hT hd t g) atTop (𝓝 0) := by sorry

Source

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

View graph