OAI/Analysis/LipschitzHilbert/Packets/SourceSupportedSelectorMotion.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Source motion only requires shortness for actual packet items. Empty long bands have unchanged amplitude when their formal stops are clipped. The original coefficients, scale parameters and conclusions are retained.

  1. theorem OAI.LipschitzHilbert.AngularGrid.source_supported_selector_amplitude_motion line 19
  2. theorem OAI.LipschitzHilbert.AngularGrid.source_supported_selector_amplitude_power_gain line 164
  3. theorem OAI.LipschitzHilbert.AngularGrid.source_supported_selector_normalized_motion line 256