OAI/Analysis/LipschitzHilbert/Trees/SourceVectorSchwartz.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Finite scalar packet coordinates assemble into an actual vector Schwartz function. Fourier cutoffs pass through the same coordinates.

  1. def OAI.LipschitzHilbert.vectorCoordinate line 15
  2. theorem OAI.LipschitzHilbert.vectorCoordinate_apply line 19
  3. def OAI.LipschitzHilbert.vectorCoordinateInjection line 22
  4. theorem OAI.LipschitzHilbert.vectorCoordinateInjection_apply line 25
  5. def OAI.LipschitzHilbert.vectorSchwartz line 32
  6. theorem OAI.LipschitzHilbert.vectorSchwartz_apply line 36
  7. theorem OAI.LipschitzHilbert.vector_fourier_coordinate line 43
  8. theorem OAI.LipschitzHilbert.vectorSchwartz_fourier_coordinate line 61
  9. theorem OAI.LipschitzHilbert.vectorSchwartz_fourier_zero line 68