Near-Optimal Centered Unit Vector

This auxiliary statement extracts an almost optimal centered unit vector from equality of the Poincaré constant.

Let $V$, $\nu$, and $m$ satisfy the finite-dimensional heat-model assumptions, and let $C>0$ satisfy

$$C_P(\nu)=C.$$

For every $\varepsilon>0$, there exists $y$ in the domain of the closed weighted gradient such that

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

and

$$\|\overline{\nabla}y\|^2\le C^{-1}(1+\varepsilon).$$

This lemma is an approximation interface for the construction of centered approximate eigenfunctions; it asserts existence, not attainment of an exact minimizer.

Formalization Note. The equality for $C_P(\nu)$ is in ENNReal, while the norm and energy inequality use the real coercion of $C$.

Original Lean declaration header

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

private theorem exists_centered_unit_near_optimal {C : NNReal} (hC : 0 < C)
    (hCP : Poincare.LocalSlope.Intrinsic.constant ν = (C : ENNReal)) {ε : ℝ} (hε : 0 < ε) :
    ∃ y : (hν.closedWeightedOperator m (ContinuousLinearMap.id ℝ V) hi).domain,
      L2.mean ν (y : Lp ℝ 2 (ν : Measure V)) = 0 ∧ ‖(y : Lp ℝ 2 (ν : Measure V))‖ = 1 ∧
      ‖hν.closedWeightedOperator m (ContinuousLinearMap.id ℝ V) hi y‖ ^ 2 ≤
        (C : ℝ)⁻¹ * (1 + ε)

Module navigation

Module: KLS/LogConcave/HeatSemigroup/ApproximateEigenfunction.

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

Supporting theorems: closedWeightedOperator_center, literatureConstant_le_of_gap.

Next: exists_centered_approx_eigenfunction.

Source excerpt, lines 43–48 · Frozen source 408915f.

import Definitions.Def_KLSModular_FunctionalInequalities_KLS_LogConcave_HeatSemigroup_ApproximateEigenfunction

open MeasureTheory
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)

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