OAI/GroupTheory/Thompson/DyadicArithmetic.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

Real dyadic arithmetic

Dyadic numbers are represented by an integer numerator and a nonnegative power of two denominator. In particular, the grid denominator below is an actual common denominator, not an assumption about the input finite set.

  1. theorem OAI.ThompsonNonamenability.isDyadic_div_pow line 22
  2. theorem OAI.ThompsonNonamenability.isDyadic_intCast line 26
  3. theorem OAI.ThompsonNonamenability.isDyadic_natCast line 29
  4. theorem OAI.ThompsonNonamenability.isDyadic_zero line 32
  5. theorem OAI.ThompsonNonamenability.isDyadic_one line 35
  6. theorem OAI.ThompsonNonamenability.IsDyadic.neg line 38
  7. theorem OAI.ThompsonNonamenability.IsDyadic.mul line 42
  8. theorem OAI.ThompsonNonamenability.IsDyadic.add line 49
  9. theorem OAI.ThompsonNonamenability.IsDyadic.sub line 58
  10. theorem OAI.ThompsonNonamenability.isDyadic_zpow line 62
  11. theorem OAI.ThompsonNonamenability.IsDyadic.mul_zpow line 70
  12. theorem OAI.ThompsonNonamenability.IsDyadic.zpow_mul line 74
  13. theorem OAI.ThompsonNonamenability.IsDyadic.div_zpow line 78
  14. theorem OAI.ThompsonNonamenability.dyadic_raise_denominator line 83

    Source documentation

    Increasing a dyadic denominator does not change the represented number.

    theorem dyadic_raise_denominator {x : ℝ} {n : ℕ}
    (hx : ∃ k : ℤ, x = (k : ℝ) / (2 : ℝ) ^ n) (m : ℕ) :
    ∃ k : ℤ, x = (k : ℝ) / (2 : ℝ) ^ (n + m) := by
…
  15. theorem OAI.ThompsonNonamenability.dyadic_denominator_mono line 92
  16. theorem OAI.ThompsonNonamenability.dyadic_common_denominator_finset line 99

    Source documentation

    Every finite family of dyadic reals has a single power of two denominator.

    theorem dyadic_common_denominator_finset {α : Type uα} (s : Finset α) (f : α → ℝ)
    (hs : ∀ a ∈ s, IsDyadic (f a)) :
    ∃ n : ℕ, ∀ a ∈ s, ∃ k : ℤ, f a = (k : ℝ) / (2 : ℝ) ^ n := by
…

    Mentions: OAI.ThompsonNonamenability.IsDyadic

  17. theorem OAI.ThompsonNonamenability.dyadic_common_denominator line 115
  18. theorem OAI.ThompsonNonamenability.dyadic_nat_numerator line 121

    Source documentation

    A dyadic representation in the unit interval has a natural grid index.

    theorem dyadic_nat_numerator {x : ℝ} {k : ℤ} {n : ℕ}
    (hx : x = (k : ℝ) / (2 : ℝ) ^ n) (h0 : 0 ≤ x) (h1 : x ≤ 1) :
    ∃ j : ℕ, j ≤ 2 ^ n ∧ x = (j : ℝ) / (2 : ℝ) ^ n := by
…
  19. theorem OAI.ThompsonNonamenability.IsDyadic.exists_nat_grid line 138
  20. theorem OAI.ThompsonNonamenability.dyadic_common_nat_grid line 146

    Source documentation

    One grid simultaneously contains any given finite dyadic family in [0,1].

    theorem dyadic_common_nat_grid {α : Type uα} (s : Finset α) (f : α → ℝ)
    (hd : ∀ a ∈ s, IsDyadic (f a))
    (h0 : ∀ a ∈ s, 0 ≤ f a) (h1 : ∀ a ∈ s, f a ≤ 1) :
    ∃ n : ℕ, ∀ a ∈ s, ∃ j : ℕ, j ≤ 2 ^ n ∧ f a = (j : ℝ) / (2 : ℝ) ^ n := by
…

    Mentions: OAI.ThompsonNonamenability.IsDyadic