OAI/MeasureTheory/DyadicAvoidance/GridSeparation.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Problem310.GridSeparation.periodicKey line 12

   Source documentation

   The periodic key of a real point in a grid of mesh 1 / q.

   def periodicKey (q x : ℝ) : ℤ := ⌊q * Int.fract x⌋

2. lemma OAI.Problem310.GridSeparation.periodicKey_add_one line 14
3. lemma OAI.Problem310.GridSeparation.periodicKey_ne_of_separated line 20

   Source documentation

   Points separated by at least one grid mesh in both circular directions cannot have the same periodic key. This includes points on cell boundaries.

   lemma periodicKey_ne_of_separated {q x y : ℝ} (hq : 0 < q)
       (hlo : 1 ≤ q * (y - x)) (hhi : q * (y - x) ≤ q - 1) :
       periodicKey q x ≠ periodicKey q y := by
   …

   Mentions: OAI.Problem310.GridSeparation.periodicKey

4. lemma OAI.Problem310.GridSeparation.periodicKey_ne_of_small_shift line 45
5. lemma OAI.Problem310.GridSeparation.mesh_mul_dyadic line 54
6. lemma OAI.Problem310.GridSeparation.mesh_ge_four line 61
7. lemma OAI.Problem310.GridSeparation.dyadic_shift_le_quarter line 67
8. lemma OAI.Problem310.GridSeparation.mesh_mul_shift_ge_four line 75
9. lemma OAI.Problem310.GridSeparation.periodicKey_dyadic_ne_center line 88

   Source documentation

   Every tested dyadic translate uses a key different from the center's key.

   lemma periodicKey_dyadic_ne_center {b n : ℕ} {x t : ℝ}
       (hnlo : 3 ≤ n) (hnhi : n ≤ b) (htlo : 1 ≤ t) (hthi : t ≤ 2) :
       periodicKey ((2 : ℝ) ^ (b + 2)) x ≠
         periodicKey ((2 : ℝ) ^ (b + 2)) (x + t * (2 : ℝ)⁻¹ ^ n) := by
   …

   Mentions: OAI.Problem310.GridSeparation.periodicKey

10. lemma OAI.Problem310.GridSeparation.dyadic_gap_ge_smaller line 97
11. lemma OAI.Problem310.GridSeparation.periodicKey_dyadic_ne_of_lt line 107

    Source documentation

    Different indices in one window use different periodic keys, uniformly in all normalized scales. No exclusion of grid-boundary centers is needed.

    lemma periodicKey_dyadic_ne_of_lt {b n m : ℕ} {x t : ℝ}
        (hnlo : 3 ≤ n) (hnm : n < m) (hmhi : m ≤ b)
        (htlo : 1 ≤ t) (hthi : t ≤ 2) :
        periodicKey ((2 : ℝ) ^ (b + 2)) (x + t * (2 : ℝ)⁻¹ ^ n) ≠
          periodicKey ((2 : ℝ) ^ (b + 2)) (x + t * (2 : ℝ)⁻¹ ^ m) := by
    …

    Mentions: OAI.Problem310.GridSeparation.periodicKey

12. lemma OAI.Problem310.GridSeparation.periodicKey_dyadic_injOn line 138
13. lemma OAI.Problem310.GridSeparation.periodicKey_dyadic_refine line 152

    Source documentation

    The nesting identity for the periodic dyadic grids.

    lemma periodicKey_dyadic_refine {b B : ℕ} (hb : b ≤ B) (x : ℝ) :
        periodicKey ((2 : ℝ) ^ (b + 2)) x =
          periodicKey ((2 : ℝ) ^ (B + 2)) x / (2 : ℤ) ^ (B - b) := by
    …

    Mentions: OAI.Problem310.GridSeparation.periodicKey

14. lemma OAI.Problem310.GridSeparation.periodicKey_dyadic_eq_of_refine line 168
15. lemma OAI.Problem310.GridSeparation.periodicKey_dyadic_ne_refine line 175
16. lemma OAI.Problem310.GridSeparation.periodicKey_nonneg line 182
17. lemma OAI.Problem310.GridSeparation.periodicKey_lt line 186
18. def OAI.Problem310.GridSeparation.dyadicKey line 194

    Source documentation

    A finite-table address for the periodic dyadic grid.

    def dyadicKey (b : ℕ) (x : ℝ) : Fin (2 ^ (b + 2)) :=
    …

19. lemma OAI.Problem310.GridSeparation.dyadicKey_eq_iff line 199
20. lemma OAI.Problem310.GridSeparation.dyadicKey_ne_center line 217
21. lemma OAI.Problem310.GridSeparation.dyadicKey_injOn line 223
22. lemma OAI.Problem310.GridSeparation.dyadicKey_eq_of_refine line 231
23. lemma OAI.Problem310.GridSeparation.dyadicKey_ne_refine line 236
24. lemma OAI.Problem310.GridSeparation.dyadicKey_add_one line 240
25. lemma OAI.Problem310.GridSeparation.measurable_periodicKey line 244
26. lemma OAI.Problem310.GridSeparation.measurable_dyadicKey line 250
27. lemma OAI.Problem310.GridSeparation.dyadicKey_cell_left line 264

    Source documentation

    The left endpoint of a cell has exactly that finite address.

    lemma dyadicKey_cell_left (b : ℕ) (k : Fin (2 ^ (b + 2))) :
        dyadicKey b ((k.val : ℝ) / (2 : ℝ) ^ (b + 2)) = k := by
    …

    Mentions: OAI.Problem310.GridSeparation.dyadicKey

28. lemma OAI.Problem310.GridSeparation.dyadicKey_surjective line 281
29. lemma OAI.Problem310.GridSeparation.factors_through_dyadicKey line 287

    Source documentation

    Every function determined by the finest address is literally a finite table. The table is obtained by evaluating at the cell's left endpoint.

    lemma factors_through_dyadicKey {α : Type u_α} {b : ℕ} (f : ℝ → α)
        (hf : ∀ x y, dyadicKey b x = dyadicKey b y → f x = f y) :
        ∃ F : Fin (2 ^ (b + 2)) → α, ∀ x, f x = F (dyadicKey b x) := by
    …

    Mentions: OAI.Problem310.GridSeparation.dyadicKey