OAI/Geometry/RCD/Transport/EntropicDirectionalBound.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The exact finite-dimensional directional bound from the entropy chord

These are the scalar first-variation calculations in EKS, Lemma 3.20. The separate flat formula avoids division by a vanishing hyperbolic sine.

  1. theorem OAI.RegularPointCoordinates.hasDerivAt_hyperbolicChord_zero line 16
  2. theorem OAI.RegularPointCoordinates.entropic_hyperbolic_directional_bound line 28
  3. theorem OAI.RegularPointCoordinates.entropic_flat_directional_bound line 43