OAI/Analysis/LipschitzHilbert/Phase/DampedSimplexInterpolation.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The damped scalar simplex estimate gives the undamped estimate at its real barycenter. These are precisely the interpolation and damping operations used for the source family in manuscript §11.

  1. theorem OAI.LipschitzHilbert.gaussianPhaseDamping_real_ge_one line 16
  2. theorem OAI.LipschitzHilbert.gaussian_undamp_real line 22
  3. theorem OAI.LipschitzHilbert.damped_simplex_barycenter line 34