OAI/Analysis/LipschitzHilbert/Estimates/SynthesisPolarization.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Exact polarization of the actual finite analyzing/synthesizing sum.

  1. def OAI.LipschitzHilbert.addScaledPacket line 13
  2. def OAI.LipschitzHilbert.selfPacketSynthesis line 16
  3. theorem OAI.LipschitzHilbert.synthesis_cross_polarization line 20