OAI/Analysis/LipschitzHilbert/Trees/SourceRecenteredTreeData.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The packet data of a recentered family is derived from its original packets. The scalar frequency carrier is controlled separately.

  1. structure OAI.LipschitzHilbert.SourceLabeledLattice.ReferenceTreePacketData line 13
  2. theorem OAI.LipschitzHilbert.SourceLabeledLattice.recentered_treeData line 30