Symmetry of the Weak Hessian

This formalizes the symmetry part of the weak Hessian estimate associated with BKL Equation (16), p. 6.

Let $V$ be finite-dimensional, let $\nu=m\mathbin{.}\mathrm{tilted}(-U)$, where $U$ has temperate growth, and assume all exponential moments of $\nu$ are integrable. Let $F\in D(A)$, with $A=\bar T^\dagger\bar T$. Suppose that for every coordinate index $i$, the weak first derivative

$$\partial_iF=\langle e_i,\bar TF\rangle$$

belongs to the domain of $\bar T$. Then for all coordinate indices $i,j$,

$$\langle e_j,\bar T\partial_iF\rangle =\langle e_i,\bar T\partial_jF\rangle$$

as elements of $L^2(\nu)$. Here $e_i,e_j$ are the standard orthonormal basis vectors.

This is the operator-domain symmetry of the weak Hessian used in curvature and defect arguments.

Formalization Note: The equality is equality of compLp $L^2(\nu)$ classes; it does not assert classical pointwise second derivatives of $F$.

Original Lean declaration header

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

theorem compLp_innerSL_closedWeightedOperator_comm
    (hνU : (ν : Measure V) = m.tilted (-U)) (hUt : U.HasTemperateGrowth)
    (hexp : ∀ r : ℝ, Integrable (fun x => Real.exp (r * ‖x‖)) (ν : Measure V))
    (F : (adjointComp (hν.closedWeightedOperator m (ContinuousLinearMap.id ℝ V) hi)).domain)
    (hD : ∀ i, (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)
    (i j : Fin (Module.finrank ℝ V)) :
    (innerSL ℝ (stdOrthonormalBasis ℝ V j)).compLp
        (hν.closedWeightedOperator m (ContinuousLinearMap.id ℝ V) hi ⟨_, hD i⟩) =
      (innerSL ℝ (stdOrthonormalBasis ℝ V i)).compLp
        (hν.closedWeightedOperator m (ContinuousLinearMap.id ℝ V) hi ⟨_, hD j⟩)

Module navigation

Module: KLS/LogConcave/HeatSemigroup/Hessian.

Definition modules: KLS/LogConcave/WeightedGradient/Closure, Analysis/Semigroup/AdjointComp, Probability/LogConcave.

Supporting theorems: convexOn_of_eq_tilted, exists_seq_smooth_tendsto_weakHessian.

Previous: exists_seq_smooth_tendsto_weakHessian.

Source excerpt, lines 365–377 · Frozen source 408915f.

import Definitions.Def_KLSModular_FunctionalInequalities_KLS_LogConcave_HeatSemigroup_Hessian

open MeasureTheory Filter Topology InnerProductSpace
open FunctionalInequalities.Analysis.Semigroup FunctionalInequalities.Analysis.BakryEmery
variable {V : Type*} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V]
  [MeasurableSpace V] [BorelSpace V] [SecondCountableTopology V] [FiniteDimensional ℝ V]
  {ν : MeasureTheory.ProbabilityMeasure V} (m : MeasureTheory.Measure V) [m.IsAddHaarMeasure] (hν : FunctionalInequalities.KLS.LogConcave ν)
  (hi : (interior (ν : MeasureTheory.Measure V).support).Nonempty) {U : V → ℝ}

theorem FunctionalInequalities.KLS.LogConcave.compLp_innerSL_closedWeightedOperator_comm_readable
    (hνU : (ν : Measure V) = m.tilted (-U)) (hUt : U.HasTemperateGrowth)
    (hexp : ∀ r : ℝ, Integrable (fun x => Real.exp (r * ‖x‖)) (ν : Measure V))
    (F : (adjointComp (hν.closedWeightedOperator m (ContinuousLinearMap.id ℝ V) hi)).domain)
    (hD : ∀ i, (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)
    (i j : Fin (Module.finrank ℝ V)) :
    (innerSL ℝ (stdOrthonormalBasis ℝ V j)).compLp
        (hν.closedWeightedOperator m (ContinuousLinearMap.id ℝ V) hi ⟨_, hD i⟩) =
      (innerSL ℝ (stdOrthonormalBasis ℝ V i)).compLp
        (hν.closedWeightedOperator m (ContinuousLinearMap.id ℝ V) hi ⟨_, hD j⟩) := by sorry