Local Regularity Gives An Operator Core

This theorem gives an operator-core criterion from local regularity of deficiency elements.

Let $V$ be finite-dimensional and complete, let $m$ be an additive Haar measure, let $\nu$ be log-concave with nonempty interior support, and let $U\in C^1(V)$ satisfy $\nu=m.\operatorname{tilted}(-U)$. Assume that every $u\in L^2(\nu)$ satisfying

for every smooth compactly supported $f$, has the property that $[\chi u]\in D(\overline{T})$ for every smooth compactly supported $\chi$, where $A=\overline{T}^{\dagger}\overline{T}$. Then every $F\in D(A)$ admits smooth compactly supported functions $f_n$ such that

In Lean, the two limits are expressed as convergence of norms to zero and the operator is adjointComp applied to closedWeightedOperator. This is an operator-core statement, not a claim about a semigroup or a curvature inequality.

Original Lean declaration header

Within namespace FunctionalInequalities.KLS.LogConcave. Shown in its original module context. Proof omitted.

theorem exists_seq_smooth_tendsto_adjointComp_of_localRegularity
    (hνU : (ν : Measure V) = m.tilted (-U)) (hU : ContDiff ℝ 1 U)
    (hreg : ∀ u : (Lp ℝ 2 (ν : Measure V)),
      (∀ (f : V → ℝ) (hf : ContDiff ℝ ∞ f) (hfc : HasCompactSupport f),
        ⟪((adjointComp (hν.closedWeightedOperator m (ContinuousLinearMap.id ℝ V) hi))
          ⟨_, hν.toLp_mem_adjointComp_domain m hi hνU hU hf hfc⟩ : (Lp ℝ 2 (ν : Measure V))), u⟫ +
          ⟪((memLp_of_contDiff_hasCompactSupport ν hf hfc).toLp f : (Lp ℝ 2
            (ν : Measure V))), u⟫ = 0) →
      ∀ (χ : V → ℝ) (hχ : ContDiff ℝ ∞ χ) (hχc : HasCompactSupport χ),
        (memLp_mul_of_contDiff_hasCompactSupport (ν := ν) hχ hχc u).toLp _ ∈
          (hν.closedWeightedOperator m (ContinuousLinearMap.id ℝ V) hi).domain)
    (F : ((adjointComp (hν.closedWeightedOperator m (ContinuousLinearMap.id ℝ V) hi))).domain) :
    ∃ (fn : ℕ → V → ℝ) (hfn : ∀ n, ContDiff ℝ ∞ (fn n))
      (hfnc : ∀ n, HasCompactSupport (fn n)),
      Tendsto (fun n => ‖(memLp_of_contDiff_hasCompactSupport ν (hfn n) (hfnc n)).toLp (fn n)
        - (F : (Lp ℝ 2 (ν : Measure V)))‖) atTop (𝓝 0) ∧
      Tendsto (fun n => ‖((adjointComp
        (hν.closedWeightedOperator m (ContinuousLinearMap.id ℝ V) hi))
          ⟨_, hν.toLp_mem_adjointComp_domain m hi hνU hU (hfn n)
          (hfnc n)⟩ : (Lp ℝ 2 (ν : Measure V))) - ((adjointComp
            (hν.closedWeightedOperator m (ContinuousLinearMap.id ℝ V) hi)) F : (Lp ℝ 2
              (ν : Measure V)))‖) atTop (𝓝 0)

Module navigation

Module: KLS/LogConcave/HeatSemigroup/OperatorCore.

Definition modules: KLS/LogConcave/WeightedGradient/Closure, KLS/LogConcave/HeatSemigroup/Generator, Analysis/Semigroup/AdjointComp, Probability/LogConcave, Energy/WeightedGradient/Core, KLS/LogConcave/WeightedGradient/Multiplier.

Supporting theorems: eq_zero_of_localRegularity.

Previous: eq_zero_of_localRegularity.

Source excerpt, lines 716–737 · Frozen source 408915f.