AngularBinOverlap.lean`

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Fixed overlap of the enlarged angular annulus bins from §6.

theorem OAI.LipschitzHilbert.AngularBins.enlargedBin_radial_bounds line 17
theorem OAI.LipschitzHilbert.AngularBins.enlargedBin_levels_near line 44
Source documentation
Any two enlarged annuli covering the same point have levels differing by at most two, uniformly in the number of angular subdivisions.
```
theorem enlargedBin_levels_near (s : ℝ) {M : ℕ} (hM : 0 < M)
    {c : ℝ} (hcM : c ≤ M) {b b' : Bin M} {a : ℝ}
    (ha : a ∈ enlargedBin s c b) (ha' : a ∈ enlargedBin s c b') :
    b'.2.1 - 2 ≤ b.2.1 ∧ b.2.1 ≤ b'.2.1 + 2 := by
…
```
Mentions: OAI.LipschitzHilbert.AngularBins.Bin, OAI.LipschitzHilbert.AngularBins.enlargedBin
theorem OAI.LipschitzHilbert.AngularBins.radialMidpoint_separated line 69
theorem OAI.LipschitzHilbert.AngularBins.finite_level_overlap line 88
theorem OAI.LipschitzHilbert.AngularBins.finite_overlap_card line 120
Source documentation
The enlarged annulus bins have uniformly bounded multiplicity. The constant includes both signs, so no boundary case requires choosing the sign of the evaluation point.
```
theorem finite_overlap_card (s a : ℝ) {M : ℕ} (hM : 0 < M)
    {c : ℝ} (hc : 0 ≤ c) (hcM : c ≤ M) (t : Finset (Bin M))
    (ht : ∀ b ∈ t, a ∈ enlargedBin s c b) :
    (t.card : ℝ) ≤ 10 * (1 + c) := by
…
```
Mentions: OAI.LipschitzHilbert.AngularBins.Bin, OAI.LipschitzHilbert.AngularBins.enlargedBin
theorem OAI.LipschitzHilbert.AngularBins.finite_indicator_overlap line 172
Source documentation
Every finite family of the actual bin indicator functions has the same uniform pointwise bound required by the line-counting lemma.
```
theorem finite_indicator_overlap (s a : ℝ) {M : ℕ} (hM : 0 < M)
    {c : ℝ} (hc : 0 ≤ c) (hcM : c ≤ M) (t : Finset (Bin M)) :
    (∑ b ∈ t, (enlargedBin s c b).indicator (1 : ℝ → ℝ) a) ≤ 10 * (1 + c) := by
…
```
Mentions: OAI.LipschitzHilbert.AngularBins.Bin, OAI.LipschitzHilbert.AngularBins.enlargedBin
def OAI.LipschitzHilbert.AngularBins.binFunction line 187
theorem OAI.LipschitzHilbert.AngularBins.measurable_binFunction line 190
theorem OAI.LipschitzHilbert.AngularBins.binFunction_bounds line 195
theorem OAI.LipschitzHilbert.AngularBins.finite_binFunction_sum line 199