AngularBins.lean`

20 declarations, 0 contain sorry, 0 declared as axioms

The actual angular annulus bins

The positive and negative dyadic annuli about a reference slope are each partitioned into M equal half-open bins, as in §6 of the manuscript. Enlargement is concentric. No choice of a significant list enters these definitions.

abbrev OAI.LipschitzHilbert.AngularBins.Bin line 22
def OAI.LipschitzHilbert.AngularBins.radialCoordinate line 24
def OAI.LipschitzHilbert.AngularBins.width line 27
def OAI.LipschitzHilbert.AngularBins.radialStart line 29
def OAI.LipschitzHilbert.AngularBins.radialMidpoint line 32
def OAI.LipschitzHilbert.AngularBins.baseBin line 35
def OAI.LipschitzHilbert.AngularBins.enlargedBin line 39
theorem OAI.LipschitzHilbert.AngularBins.radialCoordinate_abs line 43
theorem OAI.LipschitzHilbert.AngularBins.radialCoordinate_sub_abs line 47
theorem OAI.LipschitzHilbert.AngularBins.width_pos line 55
theorem OAI.LipschitzHilbert.AngularBins.width_mul line 58
theorem OAI.LipschitzHilbert.AngularBins.continuous_radialCoordinate line 63
theorem OAI.LipschitzHilbert.AngularBins.measurableSet_baseBin line 71
theorem OAI.LipschitzHilbert.AngularBins.measurableSet_enlargedBin line 76
theorem OAI.LipschitzHilbert.AngularBins.baseBin_subset_enlargedBin line 81
theorem OAI.LipschitzHilbert.AngularBins.exists_baseBin line 94
Source documentation
Every slope other than the reference belongs to an actual angular bin.
```
theorem exists_baseBin (s : ℝ) {M : ℕ} (hM : 0 < M) {a : ℝ} (ha : a ≠ s) :
    ∃ b : Bin M, a ∈ baseBin s b := by
…
```
Mentions: OAI.LipschitzHilbert.AngularBins.Bin, OAI.LipschitzHilbert.AngularBins.baseBin
theorem OAI.LipschitzHilbert.AngularBins.baseBin_radial_bounds line 125
theorem OAI.LipschitzHilbert.AngularBins.baseBin_diameter_lt line 146
theorem OAI.LipschitzHilbert.AngularBins.nearby_mem_enlargedBin line 154
Source documentation
A perturbation of a base-bin slope by at most (c-1)/2 bin widths lies in its concentric enlargement.
```
theorem nearby_mem_enlargedBin (s : ℝ) {M : ℕ} (b : Bin M) {c a a' : ℝ}
    (ha : a ∈ baseBin s b)
    (hnear : |a' - a| ≤ (c - 1) * width M b.2.1 / 2) :
    a' ∈ enlargedBin s c b := by
…
```
Mentions: OAI.LipschitzHilbert.AngularBins.Bin, OAI.LipschitzHilbert.AngularBins.baseBin, OAI.LipschitzHilbert.AngularBins.width, OAI.LipschitzHilbert.AngularBins.enlargedBin
theorem OAI.LipschitzHilbert.AngularBins.assigned_bins_injective line 170
Source documentation
A separated list occupies distinct bins whenever those bins are strictly narrower than the separation scale.
```
theorem assigned_bins_injective {ι : Type*} (s : ℝ) {M : ℕ}
    (frequency : ι → ℝ) (bin : ι → Bin M) {rho : ℝ}
    (hsep : PhaseCombinatorics.Separated frequency rho)
    (hmem : ∀ i, frequency i ∈ baseBin s (bin i))
    (hwidth : ∀ i, width M (bin i).2.1 < rho) : Function.Injective bin := by
…
```
Mentions: OAI.LipschitzHilbert.AngularBins.Bin, OAI.LipschitzHilbert.PhaseCombinatorics.Separated, OAI.LipschitzHilbert.AngularBins.baseBin, OAI.LipschitzHilbert.AngularBins.width