OAI/Analysis/LipschitzHilbert/Estimates/PolynomialEnvelope.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Polynomial growth about a box is absorbed by a slower packet envelope. The integrated envelope has the packet length as its only scale factor.

  1. def OAI.LipschitzHilbert.lineEnvelope line 14
  2. theorem OAI.LipschitzHilbert.lineEnvelope_nonneg line 17
  3. theorem OAI.LipschitzHilbert.polynomial_base_le line 22
  4. theorem OAI.LipschitzHilbert.polynomialWeight_sq_mul_envelope line 38
  5. theorem OAI.LipschitzHilbert.integral_lineEnvelope_one line 60
  6. theorem OAI.LipschitzHilbert.integrable_lineEnvelope_one line 68
  7. theorem OAI.LipschitzHilbert.lineEnvelope_antitone line 74
  8. theorem OAI.LipschitzHilbert.integrable_lineEnvelope line 80
  9. theorem OAI.LipschitzHilbert.integral_lineEnvelope_le line 88
  10. theorem OAI.LipschitzHilbert.polynomialLocalization_energy line 94