The Lichnerowicz eigenvalue estimate

On a closed Riemannian manifold of dimension n ≥ 2 with Ric ≥ (n - 1) k g, every nonzero smooth eigenfunction of the nonnegative scalar Laplacian with positive eigenvalue λ satisfies λ ≥ n k. The sign convention here is laplaceBeltrami f = -λ f. The estimate applies to every positive eigenvalue, including the first one.

The proof integrates the Bochner inequality and uses Green's identity. The pointwise Bochner inequality is also available without compactness. Connectedness and a mean-zero hypothesis are unnecessary for this estimate. No existence of eigenfunctions or rigidity of the equality case is asserted here.

References

• P. Petersen, Riemannian Geometry, 3rd ed., Chapter 9 (the Bochner technique and the Lichnerowicz estimate).

theorem TauCeti.Manifold.le_finrank_mul_laplaceBeltrami_norm_sq_mgradient {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] {f : M → ℝ} {k : ℝ} [T2Space M] [IsManifold I (↑⊤) M] [IsContMDiffRiemannianBundle I (↑⊤) E fun (x : M) => TangentSpace I x] (hf : ContMDiff I (modelWithCornersSelf ℝ ℝ) (↑⊤) f) (x : M) (hRic : ∀ (v : TangentSpace I x), (↑(Module.finrank ℝ E) - 1) * k * ‖v‖ ^ 2 ≤ (((CovariantDerivative.leviCivitaConnection I M).ricciTensor x) v) v) : 2 * laplaceBeltrami I f x ^ 2 + 2 * ↑(Module.finrank ℝ E) * (d% (laplaceBeltrami I f) x) (mgradient I f x) + 2 * ↑(Module.finrank ℝ E) * ((↑(Module.finrank ℝ E) - 1) * k) * ‖mgradient I f x‖ ^ 2 ≤ ↑(Module.finrank ℝ E) * laplaceBeltrami I (fun (y : M) => ‖mgradient I f y‖ ^ 2) x

The dimension-weighted Bochner inequality under a Ricci lower bound. It is local, requires no dimension restriction, and uses Δ = div grad rather than Δ⁺.

theorem TauCeti.Manifold.instIsContinuousRiemannianBundleTangentSpaceReal_tauCeti {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsManifold I (↑⊤) M] [IsContMDiffRiemannianBundle I (↑⊤) E fun (x : M) => TangentSpace I x] : IsContinuousRiemannianBundle E fun (x : M) => TangentSpace I x

theorem TauCeti.Manifold.finrank_mul_le_of_laplaceBeltrami_eq_neg_mul {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] {f : M → ℝ} {k lam : ℝ} [T2Space M] [IsManifold I (↑⊤) M] [IsContMDiffRiemannianBundle I (↑⊤) E fun (x : M) => TangentSpace I x] [I.Boundaryless] [CompactSpace M] [MeasurableSpace M] [BorelSpace M] (hn : 2 ≤ Module.finrank ℝ E) (hf : ContMDiff I (modelWithCornersSelf ℝ ℝ) (↑⊤) f) (hlam : 0 < lam) (heig : ∀ (x : M), laplaceBeltrami I f x = -lam * f x) (hne : ∃ (x : M), f x ≠ 0) (hRic : ∀ (x : M) (v : TangentSpace I x), (↑(Module.finrank ℝ E) - 1) * k * ‖v‖ ^ 2 ≤ (((CovariantDerivative.leviCivitaConnection I M).ricciTensor x) v) v) : ↑(Module.finrank ℝ E) * k ≤ lam

The Lichnerowicz estimate. On a closed manifold of dimension n ≥ 2 with Ric ≥ (n - 1) k g, every positive eigenvalue with a nonzero smooth eigenfunction is at least n k. The eigen-equation is stated for the native Δ = div grad. The real lower bound k need not be positive.