OAI/Analysis/LipschitzHilbert/Phase/SourcePredictablePacketMotion.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Predictable-length motion of the actual masked physical packet intervals, expressed in the carrier common to one angular child.

  1. theorem OAI.LipschitzHilbert.SourceLabeledLattice.source_predictable_masked_interval_motion line 15