OAI/Analysis/LipschitzHilbert/Phase/AngularStopping.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The actual last eligible angular level exists for every positive precision. Packet stopping precedes the stopping of its assigned top.

  1. theorem OAI.LipschitzHilbert.AngularGrid.exists_ineligible line 14
  2. def OAI.LipschitzHilbert.AngularGrid.lastEligible line 25
  3. theorem OAI.LipschitzHilbert.AngularGrid.eligible_iff_le_lastEligible line 28
  4. theorem OAI.LipschitzHilbert.AngularGrid.eligible_lastEligible line 50
  5. theorem OAI.LipschitzHilbert.AngularGrid.lastEligible_antitone_precision line 55