Smooth Approximation for the Weak Hessian

This technical statement constructs a smooth compactly supported approximation for a generator-domain element.

Let $V$ be finite-dimensional, let $\nu=m\mathbin{.}\mathrm{tilted}(-U)$ with nonempty interior support, and assume that $U$ has temperate growth, is $C^1$, and that every exponential moment of $\nu$ is integrable. Let $\rho\in\mathbb R$ satisfy the pointwise curvature inequality

For every $F\in D(A)$, where $A=\bar T^\dagger\bar T$, there are functions $f_n\in C_c^\infty(V)$ such that:

1. $\bar T[f_n]\to\bar T F$ in $L^2(\nu)$.
2. $A[f_n]\to AF$ in $L^2(\nu)$.
3. For every standard basis vector $e_i$, the weak derivative $\langle e_i,\bar TF\rangle$ lies in the domain of $\bar T$, and $\bar T[\partial_i f_n]$ converges to $\bar T\langle e_i,\bar TF\rangle$.

This approximation lemma is used to extend smooth Hessian identities to the operator domain.

Original Lean declaration header

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

private theorem exists_seq_smooth_tendsto_weakHessian (hνU : (ν : Measure V) = m.tilted (-U))
    (hUt : U.HasTemperateGrowth) (hU : ContDiff ℝ 1 U)
    (hexp : ∀ r : ℝ, Integrable (fun x => Real.exp (r * ‖x‖)) (ν : Measure V)) {ρ : ℝ}
    (hH : ∀ x v, ρ * ‖v‖ ^ 2 ≤ bilinearIteratedFDerivTwo ℝ U x v v)
    (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 => hν.closedWeightedOperator m (ContinuousLinearMap.id ℝ V) hi
          ⟨_, hν.toLp_mem_closedWeightedOperator_domain m hi (hfn n) (hfnc n)⟩) atTop
        (𝓝 (hν.closedWeightedOperator m (ContinuousLinearMap.id ℝ V) hi
          ⟨(F : Lp ℝ 2 (ν : Measure V)), F.2.2⟩)) ∧
      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)⟩) atTop
        (𝓝 (adjointComp (hν.closedWeightedOperator m (ContinuousLinearMap.id ℝ V) hi) F)) ∧
      ∀ i, ∃ h : (innerSL ℝ (stdOrthonormalBasis ℝ V i)).compLp
          (hν.closedWeightedOperator m (ContinuousLinearMap.id ℝ V) hi
            ⟨(F : Lp ℝ 2 (ν : Measure V)), F.2.2⟩) ∈
          (hν.closedWeightedOperator m (ContinuousLinearMap.id ℝ V) hi).domain,
        Tendsto (fun n => hν.closedWeightedOperator m (ContinuousLinearMap.id ℝ V) hi
            ⟨_, hν.toLp_mem_closedWeightedOperator_domain m hi
              (contDiff_fderiv_apply_infty (hfn n) (stdOrthonormalBasis ℝ V i))
              ((hfnc n).fderiv_apply ℝ (stdOrthonormalBasis ℝ V i))⟩) atTop
          (𝓝 (hν.closedWeightedOperator m (ContinuousLinearMap.id ℝ V) hi ⟨_, h⟩))

Module navigation

Module: KLS/LogConcave/HeatSemigroup/Hessian.

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

Supporting theorems: integral_hessianSq_add_le_of_hasTemperateGrowth, tendsto_apply_of_tendsto_adjointComp, exists_seq_smooth_tendsto_adjointComp_of_localRegularity, toLp_mul_mem_closedWeightedOperator_domain_of_orthogonal.

Next: compLp_innerSL_closedWeightedOperator_comm.

Source excerpt, lines 265–287 · Frozen source 408915f.