OAI/Geometry/PinnedDistances/GridBounds.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.WeakPinned.Grid.level line 13
2. def OAI.WeakPinned.Grid.label line 15
3. lemma OAI.WeakPinned.Grid.regular_pair_ae line 19
4. lemma OAI.WeakPinned.Grid.label_eq_iff line 46
5. def OAI.WeakPinned.Grid.side line 59

   Source documentation

   Side length in the original (unrotated) plane, after scaling by exp m.

   def side (ω : FullSample) (r m : ℝ) : ℝ := Real.exp (m+ω.1.1)*(2:ℝ)^level ω r

   Mentions: OAI.WeakPinned.Grid.FullSample, OAI.WeakPinned.Grid.level

6. lemma OAI.WeakPinned.Grid.side_pos line 61
7. lemma OAI.WeakPinned.Grid.log_side line 63
8. lemma OAI.WeakPinned.Grid.side_bounds line 68
9. lemma OAI.WeakPinned.Grid.label_diameter line 84
10. lemma OAI.WeakPinned.Global.arch_label_ae line 107
11. lemma OAI.WeakPinned.Grid.bin_gap line 134
12. lemma OAI.WeakPinned.Grid.scaled_ratio line 148
13. lemma OAI.WeakPinned.Grid.label_gap line 158
14. lemma OAI.WeakPinned.Grid.card_labels_bound line 180

    Source documentation

    A uniform bound on the number of occupied squares meeting the disk. Only the lower bound on the actual side is needed.

    lemma card_labels_bound {P : Type u3} [DecidableEq P] (A : Finset P) (u : P → ℂ)
        (ω : FullSample) (r m : ℝ) (b : ℂ) (R L : ℝ) (M : ℕ)
        (hR : 0≤R) (hL : 0<L) (hside : L ≤ side ω r m)
        (hM : 2*R/L+1≤M)
        (hA : ∀ x∈A, ‖(Real.exp m:ℂ)*u x+b‖≤R) :
        (A.image (fun x => label ω r (u x))).card ≤ (2*M+1)^2 := by
    …

    Mentions: OAI.WeakPinned.Grid.FullSample, OAI.WeakPinned.Grid.side, OAI.WeakPinned.Grid.label