Samplinglib
Lean gate passed 2026-08-19T05:09:39.794721+00:00 · 644be936998e
Chapter 2 · Book pp. 48–95 · August 9, 2026 edition

Functional Inequalities

Develop Poincaré, log-Sobolev, transport, and isoperimetric tools, including semigroup proofs and preservation operations.

Begin with 2.1 Open this chapter in the canonical August 9 source ↗

Chapter route

This chapter develops Poincaré inequality, log-Sobolev inequality, transport inequalities, Cheeger inequality. Its main destination is to connect the definitions below to the results that later chapters consume.

Core definitions

  • Poincaré inequality: variance is controlled by Dirichlet energy; the compiled local interface records probability normalization, its test class, and all three integrability requirements explicitly.
  • Log-Sobolev inequality: relative entropy is controlled by Fisher information.
  • Talagrand transport inequalities compare relative entropy with Wasserstein distance.
  • Isoperimetric and concentration profiles quantify boundary expansion and tail decay.

Main results

  • Markov-semigroup interpolation proves functional inequalities from curvature and dissipation.
  • Tensorization, bounded perturbation, Lipschitz pushforward, and other operations preserve selected inequalities with tracked constants.
  • Functional inequalities imply concentration and isoperimetric estimates.
  • The framework extends, with changed analytic interfaces, to manifolds and discrete chains.

Contents

  1. 2.1Overview of the InequalitiesBook p. 48
  2. 2.2Proofs via Markov Semigroup TheoryBook p. 50
  3. 2.3Operations Preserving Functional InequalitiesBook p. 60
  4. 2.4Concentration of Measure and IsoperimetryBook p. 68
  5. 2.5Riemannian ManifoldsBook p. 77
  6. 2.6Discrete Space and TimeBook p. 84
  7. 2.bibBibliographical NotesBook p. 85
  8. 2.exExercisesBook p. 87
Why is this chapter route valid?

Analytic contracts

  • State whether Hessian inequalities hold everywhere, almost everywhere, or in a weak convex-analytic sense.
  • Track normalization and absolute continuity whenever a potential is used to define a probability law.
  • Keep localization inputs separate from the one-dimensional inequality they reduce to.

Open boundaries

  • Bakry–Émery Poincaré criterion, pending a concrete semigroup/generator domain
  • Full localization theorem
  • Dimension-sharp log-concave isoperimetry
  • Complete perturbation hierarchy
View Lean formalization

These mappings are evidence links, not a claim that the entire chapter is formalized.