OAI/Analysis/LipschitzHilbert/Trees/SourceTopConcentration.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The source's polynomial top bound for the actual packet sums, with a common exponentially small exceptional set and no scale-count loss.

  1. theorem OAI.LipschitzHilbert.PlanarPacketFamily.source_top_concentration line 14