OAI/Analysis/LipschitzHilbert/Trees/SourceCrossConcentration.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The manuscript's cross-profile top concentration estimate follows from the four genuine self-profile families, on one exceptional set.

  1. theorem OAI.LipschitzHilbert.SourceLatticePacket.source_cross_concentration line 13