PacketAngularCover.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Fixed-scale angular cells containing both the packet spectrum and its selector support. The three nested grids are the existing literal alternating one-third grids.

theorem OAI.LipschitzHilbert.PacketRepresentation.exists_scaled_three_grid_cover line 14
theorem OAI.LipschitzHilbert.PacketRepresentation.frequency_margin_subset line 36

theorem OAI.LipschitzHilbert.PacketRepresentation.exists_packet_angular_cell line 49

Source documentation

A single selected angular cell contains the selector support and the entire spectrum with the requested margin.

theorem exists_packet_angular_cell (unit : ℝ) (hu : 0<unit) (k : ℤ)
    (l w theta c C margin radius : ℝ) (hl : 0<l) (hw : 0<w)
    (hc : 0<c) (hC : 0≤C) (hm : 0≤margin) (hr : 0≤radius)
    (hprecision : w/l=unit*DyadicLineGrid.scale k)
    (hsmall : 6*max radius (C/c+margin)<1) :
    ∃ grid∈Finset.Icc (-1) 1, ∃ cell : ℤ,
      (∀ s, |s-theta|≤radius*(w/l) → s∈scaledAngularCell unit grid k cell) ∧
      (∀ xi eta, c≤w*eta → |symbolX l xi eta theta|≤C →
        Icc (-xi/eta-margin*(w/l)) (-xi/eta+margin*(w/l)) ⊆
          scaledAngularCell unit grid k cell) := by
…

Mentions: OAI.LipschitzHilbert.DyadicLineGrid.scale, OAI.LipschitzHilbert.scaledAngularCell, OAI.LipschitzHilbert.PacketRepresentation.symbolX