OAI/Analysis/LipschitzHilbert/Trees/SourceVectorSlices.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Actual coordinate restrictions of Hilbert-valued planar Schwartz packets, needed to reproduce non-tensor packet sums.

  1. def OAI.LipschitzHilbert.vectorHorizontalSlice line 13
  2. theorem OAI.LipschitzHilbert.vectorHorizontalSlice_apply line 18
  3. theorem OAI.LipschitzHilbert.verticalLine_temperate line 24
  4. theorem OAI.LipschitzHilbert.verticalLine_antilipschitz line 32
  5. def OAI.LipschitzHilbert.vectorVerticalSlice line 39
  6. theorem OAI.LipschitzHilbert.vectorVerticalSlice_apply line 44