OAI/Analysis/LipschitzHilbert/Trees/SourceSlottedConcentration.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Concentration for the original finite labeled top families. Slotting is used only inside the local concentration theorem. The conclusion is indexed by the original tops, before any witness or direction-counting argument, and the fixed slot factor is absorbed explicitly.

  1. structure OAI.LipschitzHilbert.SourceLabeledTopGeometry line 17
  2. theorem OAI.LipschitzHilbert.SourceLabeledLattice.slotted_topGeometry line 33
  3. theorem OAI.LipschitzHilbert.SourceLabeledLattice.slot_decay line 50
  4. theorem OAI.LipschitzHilbert.SourceLabeledLattice.sum_joint_norm_le line 58
  5. theorem OAI.LipschitzHilbert.SourceLabeledLattice.source_labeled_concentration line 69