OAI/Analysis/LipschitzHilbert/Packets/SourcePacketMotionBudget.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The explicit packet-motion coefficient at the angular averaging scale. All three spatial ratios are bounded before applying polynomial absorption.

  1. theorem OAI.LipschitzHilbert.AngularGrid.source_packet_displacement_ratios line 11
  2. theorem OAI.LipschitzHilbert.AngularGrid.source_packet_motion_coefficient line 66