OAI/Analysis/LipschitzHilbert/Trees/SourcePlanarPolynomial.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Transverse polynomial localization of actual planar vector packets. Both coordinate frequency cutoffs are retained.

  1. theorem OAI.LipschitzHilbert.transversePolynomial_temperate line 12
  2. def OAI.LipschitzHilbert.planarPolynomialLocalization line 20
  3. theorem OAI.LipschitzHilbert.planarPolynomialLocalization_apply line 26
  4. theorem OAI.LipschitzHilbert.planarPolynomialLocalization_norm line 31
  5. theorem OAI.LipschitzHilbert.planarPolynomialLocalization_horizontal line 37
  6. theorem OAI.LipschitzHilbert.planarPolynomialLocalization_vertical line 44
  7. theorem OAI.LipschitzHilbert.planarPolynomialLocalization_horizontal_band line 51
  8. theorem OAI.LipschitzHilbert.planarPolynomialLocalization_vertical_band line 63