OAI/Analysis/LipschitzHilbert/Estimates/SlopeTopNeighborhood.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Transfer the global lattice neighborhood bound to physical slope coordinates and the exact top weight, with an exponential area bound.

  1. def OAI.LipschitzHilbert.topAreaPrefactor line 15
  2. theorem OAI.LipschitzHilbert.topAreaPrefactor_pos line 17
  3. theorem OAI.LipschitzHilbert.slope_top_neighborhood line 21