OAI/Analysis/LipschitzHilbert/Trees/SourceTrimInteractions.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Removing noninteracting short packets is an exact equality for the actual vector-valued far Gram sum.

  1. theorem OAI.LipschitzHilbert.SourceLabeledLattice.far_pairing_restrict_to_interacting line 17