OAI/Analysis/LipschitzHilbert/Phase/SourceFullAngularGrid.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A common source grid for every row of a finite collection. Its root is chosen after the row precisions; no extra eligibility hypothesis is needed in the application of the packet recovery theorem.

  1. theorem OAI.LipschitzHilbert.exists_source_full_angular_grid line 13