OAI/Analysis/LipschitzHilbert/Estimates/TopDilatedTesting.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Summing the dilation costs in the popular-top testing estimate. The exponent three comes from the two-dimensional dilation and the weak-L2 layer-cake estimate; degree four already makes the series summable.

  1. theorem OAI.LipschitzHilbert.dyadic_cubic_decay line 16
  2. theorem OAI.LipschitzHilbert.top_lintegral_of_dilated_testing line 30