OAI/Analysis/LipschitzHilbert/Trees/SourcePhysicalNormalizedMotion.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The two normalized prediction-motion estimates for the original physical packet family, with actual angular masses and transition products.

  1. theorem OAI.LipschitzHilbert.AngularGrid.source_physical_normalized_motion line 16