OAI/Geometry/RCD/Coordinates/RegularizedEntropySecant.lean
1 declarations, 0 contain sorry, 0 declared as axioms
The regularized signed logarithmic variation is bounded by the entropy secant
- theorem
OAI.RegularPointCoordinates.regularized_log_secant_le_entropyline 14