OAI/Analysis/LipschitzHilbert/Estimates/GlobalLocalNeighborhood.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Globalize the proved local neighborhood estimates by increasing the natural moment order on distant boxes. The total exceptional area stays exponentially small and the top's polynomial decay is retained.

  1. theorem OAI.LipschitzHilbert.global_top_neighborhood_of_local line 15