OAI/Analysis/LipschitzHilbert/Phase/AngularGeometry.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.LipschitzHilbert.AngularGrid.width line 11
2. def OAI.LipschitzHilbert.AngularGrid.left line 13
3. def OAI.LipschitzHilbert.AngularGrid.center line 16
4. theorem OAI.LipschitzHilbert.AngularGrid.width_pos line 19
5. theorem OAI.LipschitzHilbert.AngularGrid.slope_mem_cell line 25

   Source documentation

   The floor assignment is exactly the half-open translated interval.

   theorem slope_mem_cell (g : AngularGrid) (level : ℕ) (slope : ℝ) :
       g.left level (g.index level slope) ≤ slope ∧
         slope < g.left level (g.index level slope) + g.width level := by
   …

   Mentions: OAI.LipschitzHilbert.AngularGrid

6. theorem OAI.LipschitzHilbert.AngularGrid.slope_dist_center_le line 43
7. theorem OAI.LipschitzHilbert.AngularGrid.same_cell_diameter line 49
8. theorem OAI.LipschitzHilbert.AngularGrid.eligible_iff_precision_le line 56
9. def OAI.LipschitzHilbert.AngularGrid.neighbors line 62
10. theorem OAI.LipschitzHilbert.AngularGrid.neighbors_symmetric line 65
11. theorem OAI.LipschitzHilbert.AngularGrid.slopes_separated_of_not_neighbors line 71

    Source documentation

    Non-neighboring cells separate every pair of slopes they contain.

    theorem slopes_separated_of_not_neighbors (g : AngularGrid) (level : ℕ)
        (gap s t : ℝ) (hfar : ¬g.neighbors level gap (g.index level s) (g.index level t)) :
        gap ≤ |s - t| := by
    …

    Mentions: OAI.LipschitzHilbert.AngularGrid

12. theorem OAI.LipschitzHilbert.AngularGrid.centers_separated_of_not_neighbors line 93
13. theorem OAI.LipschitzHilbert.AngularGrid.carrier_frequency_separated line 102

    Source documentation

    The actual carrier frequencies inherit separation in each Hilbert component from non-neighboring angular cells.

    theorem carrier_frequency_separated (g : AngularGrid) (level : ℕ)
        {gap ηmin η s : ℝ} (hηmin : 0 ≤ ηmin) (hη : ηmin ≤ |η|)
        {i j : ℤ} (hfar : ¬g.neighbors level gap i j) :
        gap * ηmin ≤ |(s - g.center level i) * η - (s - g.center level j) * η| := by
    …

    Mentions: OAI.LipschitzHilbert.AngularGrid