OAI/Analysis/LipschitzHilbert/Estimates/TopAreaDiscard.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Convert the exponential total-top-area exception to a small fraction of the testing set, using only the manuscript's area and disparity bounds.

  1. theorem OAI.LipschitzHilbert.eventually_top_area_factor line 14
  2. theorem OAI.LipschitzHilbert.top_area_discard_numeric line 26