OAI/NumberTheory/EgyptianFractions/RationalCommonModulus.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem337.exists_large_common_rational_modulus line 12

   Source documentation

   Finitely many rational points of the unit interval have a common positive modulus, which can be chosen arbitrarily large.

   theorem exists_large_common_rational_modulus {Ω : Type*} [Fintype Ω]
       (x : Ω → ℚ) (hx0 : ∀ ω, 0 ≤ x ω) (hx1 : ∀ ω, x ω < 1) (B : ℕ) :
       ∃ q : ℕ, B ≤ q ∧ 0 < q ∧ ∃ a : Ω → ℕ,
         ∀ ω, a ω < q ∧ (a ω : ℚ) / (q : ℚ) = x ω := by
   …

2. theorem OAI.Problem337.exists_large_common_zmod line 50

   Source documentation

   A finite rational unit-interval family embeds in a cyclic group of an arbitrarily large order with its exact least-residue fractions preserved.

   theorem exists_large_common_zmod {Ω : Type*} [Fintype Ω]
       (x : Ω → ℚ) (hx0 : ∀ ω, 0 ≤ x ω) (hx1 : ∀ ω, x ω < 1) (B : ℕ) :
       ∃ q : ℕ, B ≤ q ∧ 0 < q ∧ ∃ y : Ω → ZMod q,
         ∀ ω, ((y ω).val : ℚ) / (q : ℚ) = x ω := by
   …