OAI/Analysis/LipschitzHilbert/Estimates/SmoothedCommutatorDecomposition.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Exact decomposition of a smoothed coefficient against finitely many input bands into the three already bounded commutator interactions.

  1. theorem OAI.LipschitzHilbert.PacketRepresentation.lineSchwartzCommutator_zero_right line 15
  2. theorem OAI.LipschitzHilbert.PacketRepresentation.schwartzDerivative_sum line 20
  3. theorem OAI.LipschitzHilbert.PacketRepresentation.schwartzDerivative_zero line 24
  4. theorem OAI.LipschitzHilbert.PacketRepresentation.scale_add_four line 27
  5. theorem OAI.LipschitzHilbert.PacketRepresentation.lineCommutator_nearbyInput line 32
  6. theorem OAI.LipschitzHilbert.PacketRepresentation.split_dyadic_interaction line 44
  7. theorem OAI.LipschitzHilbert.PacketRepresentation.smoothedCommutator_decomposition line 57