OAI/Analysis/LipschitzHilbert/Trees/SourceFourPolarizedConcentration.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

One exceptional set works for all four self-packet families used in polarization. Their common raw constant doubles, which costs one power of L; the fixed fourfold area cost is absorbed by two additional units in the exponential decay rate.

  1. def OAI.LipschitzHilbert.packetPolarizationPhase line 17
  2. theorem OAI.LipschitzHilbert.packetPolarizationPhase_norm line 20
  3. theorem OAI.LipschitzHilbert.four_exp_decay line 23
  4. theorem OAI.LipschitzHilbert.SourceLatticePacket.polarize_topGeometry line 38
  5. theorem OAI.LipschitzHilbert.SourceLatticePacket.source_four_polarized_concentration line 52