Temperate Functions Belong To The Closed Gradient Domain

This is a classical-to-$L^2$ domain bridge for the closed weighted gradient.

Let $V$ be a finite-dimensional real inner-product space with the stated topological and measurable structures. Let $\nu$ be log-concave, let $m$ be an additive Haar measure, and assume that the interior of the support of $\nu$ is nonempty. Assume every exponential moment of $\nu$ is integrable. For every function $f:V\to\mathbb R$ of temperate growth, there exist

1. a proof that $f\in L^2(\nu)$;
2. a proof that its gradient $\nabla f\in L^2(\nu)$; and
3. a proof that the $L^2$ class of $f$ lies in the domain of the closed weighted operator.

If these objects are denoted by $[f]$ and $[\nabla f]$, then

This result supplies operator-domain membership for temperate test functions and is useful for transferring classical differential identities to $L^2$ classes.

Formalization Note. The witnesses are MemLp proofs and a domain-membership proof; toLp denotes the corresponding $L^2(\nu)$ representatives.

Original Lean declaration header

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

theorem exists_toLp_mem_closedWeightedOperator_domain_of_hasTemperateGrowth {f : V → ℝ}
    (hf : f.HasTemperateGrowth) :
    ∃ (hf2 : MemLp f 2 (ν : Measure V)) (hg2 : MemLp (gradient f) 2 (ν : Measure V))
      (hmem : hf2.toLp f ∈ (hν.closedWeightedOperator m (ContinuousLinearMap.id ℝ V) hi).domain),
      hν.closedWeightedOperator m (ContinuousLinearMap.id ℝ V) hi ⟨_, hmem⟩ = hg2.toLp (gradient f)

Module navigation

Module: KLS/LogConcave/HeatSemigroup/Temperate.

Definition modules: KLS/LogConcave/WeightedGradient/Closure, Probability/LogConcave.

Supporting theorems: cutoff_eq_one, hasCompactSupport_cutoff, integrable_of_norm_le_pow, norm_iteratedFDeriv_cutoff_le.

Source excerpt, lines 124–128 · Frozen source 408915f.