OAI/Analysis/LipschitzHilbert/Estimates/SimplexBarycenter.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The shift-simplex vertices give the identical bound at the diagonal parameter μ/K. The estimate has no factor depending on the number of shifts.

  1. theorem OAI.LipschitzHilbert.phaseTubeBound_barycenter line 14