Interior Regularity Of Deficiency Elements

This theorem establishes local form-domain membership for deficiency elements.

Let $V$ be finite-dimensional, 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)$. Let $u\in L^2(\nu)$ satisfy

for every smooth compactly supported $f$, where $A=\overline{T}^{\dagger}\overline{T}$ and $\overline{T}$ is the closed unit-weight gradient. Then for every smooth compactly supported $\chi$, the class of $\chi u$ belongs to $D(\overline{T})$:

The class is formed with memLp_mul_of_contDiff_hasCompactSupport and toLp. This is the local regularity hypothesis used by the operator-core criterion; it does not assert that $u$ itself has a global weak gradient.

Original Lean declaration header

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

theorem toLp_mul_mem_closedWeightedOperator_domain_of_orthogonal
    (hνU : (ν : Measure V) = m.tilted (-U)) (hU : ContDiff ℝ 1 U) (u : Lp ℝ 2 (ν : Measure V))
    (horth : ∀ (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

Module navigation

Module: KLS/LogConcave/HeatSemigroup/InteriorRegularity.

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

Supporting theorems: lintegral_enorm_convolution_sq_le, tendsto_eLpNorm_convolution_sub, integral_laplacian_mul_convolution_eq, integral_laplacian_mul_tiltedDensity_mul, norm_toLp_smul_gradient_le.

Previous: integral_laplacian_mul_tiltedDensity_mul.

Source excerpt, lines 555–563 · Frozen source 408915f.