OAI/Analysis/LipschitzHilbert/Estimates/MaskParameters.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Choose the mask exponent after the fixed top bounds. Both the near-region and far-region errors have any prescribed polynomial decay.

  1. theorem OAI.LipschitzHilbert.constant_mul_rpow_le line 13
  2. theorem OAI.LipschitzHilbert.top_mask_error_of_exponents line 21
  3. theorem OAI.LipschitzHilbert.exists_mask_parameters line 48
  4. theorem OAI.LipschitzHilbert.exists_mask_parameters_above line 64