Semigroup Energy as an Inner Product
ProvedFunctionalInequalities.Analysis.Semigroup.Generated.norm_map_apply_sq_eq_inner_readableThis is an auxiliary energy identity for a generated semigroup.
Let be real complete inner-product spaces, let be closed with dense domain, and write . For and , let be Generated.apply T hT hd r f. Then
The identity rewrites the squared form energy along the flow as an inner product, enabling differentiation and curvature estimates.
Formalization Note. The operator domains are represented by subtypes, and the norm and inner product are real-valued.
Original Lean declaration header
Within namespace FunctionalInequalities.Analysis.Semigroup.Generated. Shown in its original module context. Proof omitted.
theorem norm_map_apply_sq_eq_inner (f : (adjointComp T).domain) {r : ℝ} (hr : 0 ≤ r) :
‖T ⟨apply T hT hd r f, (preserves_domain T hT hd f hr).2⟩‖ ^ 2 =
⟪apply T hT hd r (adjointComp T f), apply T hT hd r f⟫
Module navigation
Module: Analysis/Semigroup/Generated/Curvature.
Definition modules: Analysis/Semigroup/AdjointComp, Analysis/Semigroup/Generated/Domain, Analysis/Semigroup/Generated/Basic.
Next: hasDerivAt_inner_apply.
Source excerpt, lines 34–36 · Frozen source 408915f.
import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_Semigroup_Generated_Curvature
open scoped RealInnerProductSpace
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₀))
theorem FunctionalInequalities.Analysis.Semigroup.Generated.norm_map_apply_sq_eq_inner_readable (f : (adjointComp T).domain) {r : ℝ} (hr : 0 ≤ r) :
‖T ⟨apply T hT hd r f, (preserves_domain T hT hd f hr).2⟩‖ ^ 2 =
⟪apply T hT hd r (adjointComp T f), apply T hT hd r f⟫ := by sorry