OAI/Analysis/LipschitzHilbert/Estimates/BoxPolynomialWeight.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The polynomial localization lower bound on a reference interval, with the horizontal box offset retained explicitly.

  1. theorem OAI.LipschitzHilbert.box_polynomial_base line 13
  2. theorem OAI.LipschitzHilbert.box_polynomial_weight line 36
  3. theorem OAI.LipschitzHilbert.box_polynomial_weight_pos line 41