OAI/Analysis/LipschitzHilbert/Estimates/PopularTopMask.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Mask removal on the actual good testing set, with the weak top-count hypothesis discharged by the geometric witness estimate. Mask parameters are fixed before the top family and the testing set.

  1. theorem OAI.LipschitzHilbert.popular_top_mask_integral line 15