Centered Approximate First Eigenfunction

This statement constructs approximate first eigenfunctions in the heat model.

Let $V$ be a finite-dimensional real inner-product space, let $\nu$ be log-concave with nonempty support interior, and suppose

$$\nu=m.\operatorname{tilted}(-U),$$

where $U$ is twice continuously differentiable. Let $C>0$ satisfy $C_P(\nu)=C$. For every $\eta>0$, there exists an element $f$ in the domain of the adjoint composition of the closed weighted gradient such that

$$\operatorname{mean}_\nu(f)=0,\qquad \|f\|=1,$$

and

$$\|A f-C^{-1}f\|\le C^{-1}\eta,$$

where $A=\overline{\nabla}^{\,\dagger}\overline{\nabla}$ is represented by adjointComp.

The result provides an approximate, rather than exact, first eigenfunction for arguments that do not assume compact resolvent or eigenvalue attainment.

Formalization Note. The equality $C_P(\nu)=C$ is in ENNReal; $C^{-1}$ and the residual norm are real-valued.

Original Lean declaration header

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

theorem exists_centered_approx_eigenfunction {C : NNReal} (hC : 0 < C)
    (hCP : Poincare.LocalSlope.Intrinsic.constant ν = (C : ENNReal)) {η : ℝ} (hη : 0 < η) :
    ∃ f : (adjointComp (hν.closedWeightedOperator m (ContinuousLinearMap.id ℝ V) hi)).domain,
      L2.mean ν (f : Lp ℝ 2 (ν : Measure V)) = 0 ∧ ‖(f : Lp ℝ 2 (ν : Measure V))‖ = 1 ∧
      ‖adjointComp (hν.closedWeightedOperator m (ContinuousLinearMap.id ℝ V) hi) f -
          (C : ℝ)⁻¹ • (f : Lp ℝ 2 (ν : Measure V))‖ ≤ (C : ℝ)⁻¹ * η

Module navigation

Module: KLS/LogConcave/HeatSemigroup/ApproximateEigenfunction.

Definition modules: L2/MeanVariance, KLS/LogConcave/WeightedGradient/Closure, Analysis/Semigroup/AdjointComp, Probability/LogConcave, Poincare/LocalSlope/Basic.

Supporting theorems: exists_approx_eigenvector_of_gap, closedWeightedOperator_id_gap_of_literature_le, orthogonal_ker_iff_mean_eq_zero, exists_centered_unit_near_optimal.

Previous: exists_centered_unit_near_optimal.

Source excerpt, lines 100–105 · Frozen source 408915f.

import Definitions.Def_KLSModular_FunctionalInequalities_KLS_LogConcave_HeatSemigroup_ApproximateEigenfunction

open MeasureTheory
open FunctionalInequalities.Analysis.Semigroup FunctionalInequalities.Analysis.Semigroup.Generated
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)
variable {U : V → ℝ} (hνU : (ν : MeasureTheory.Measure V) = m.tilted (-U)) (hU : ContDiff ℝ 2 U)
include hνU hU

theorem FunctionalInequalities.KLS.LogConcave.exists_centered_approx_eigenfunction_readable {C : NNReal} (hC : 0 < C)
    (hCP : Poincare.LocalSlope.Intrinsic.constant ν = (C : ENNReal)) {η : ℝ} (hη : 0 < η) :
    ∃ f : (adjointComp (hν.closedWeightedOperator m (ContinuousLinearMap.id ℝ V) hi)).domain,
      L2.mean ν (f : Lp ℝ 2 (ν : Measure V)) = 0 ∧ ‖(f : Lp ℝ 2 (ν : Measure V))‖ = 1 ∧
      ‖adjointComp (hν.closedWeightedOperator m (ContinuousLinearMap.id ℝ V) hi) f -
          (C : ℝ)⁻¹ • (f : Lp ℝ 2 (ν : Measure V))‖ ≤ (C : ℝ)⁻¹ * η := by sorry