OAI/NumberTheory/Ostmann/Arithmetic/MovingCoprimeDescent.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.moving_pivot_inherited_coprime line 20

   Source documentation

   The compensation product and reconstructed giant inherit every old coprimality test directly from the integer relation.

   theorem moving_pivot_inherited_coprime (L R u p : ℕ) (s v w : ℤ)
       (hLR : L.Coprime R) (hv : IsCoprime v (L : ℤ)) (hw : IsCoprime w (R : ℤ))
       (hrel : v * R - w * L = s * ((u * p : ℕ) : ℤ)) :
       u.Coprime (L * R) ∧ p.Coprime (L * R) := by
   …

2. theorem OAI.Ostmann.pairwise_append_of_products line 31
3. theorem OAI.Ostmann.coprime_products_of_pairwise_append line 40
4. theorem OAI.Ostmann.moving_children_pairwise_iff line 52

   Source documentation

   The two actual child lists have precisely one new coprimality condition: the inserted giant must be coprime to its own compensation list. All inherited cross-list conditions follow from the numerator equation.

   theorem moving_children_pairwise_iff (L R U : List ℕ) (p : ℕ) (s v w : ℤ)
       (hold : (L ++ R).Pairwise Nat.Coprime)
       (hv : IsCoprime v (L.prod : ℤ)) (hw : IsCoprime w (R.prod : ℤ))
       (hrel : v * R.prod - w * L.prod = s * ((U.prod * p : ℕ) : ℤ)) :
       ((p :: (U ++ L)).Pairwise Nat.Coprime ∧ (p :: (U ++ R)).Pairwise Nat.Coprime) ↔
         U.Pairwise Nat.Coprime ∧ p.Coprime U.prod := by
   …

5. theorem OAI.Ostmann.compensation_product_squarefree line 80
6. theorem OAI.Ostmann.moving_compensation_square_tests line 93

   Source documentation

   The own-compensation unit test is exactly the nonvanishing numerator condition modulo the square of each distinct sampled compensation prime.

   theorem moving_compensation_square_tests (U : List ℕ) (p : ℕ) (s : ℤ)
       (hprime : ∀ b ∈ U, b.Prime) (hpair : U.Pairwise Nat.Coprime)
       (hs : ∀ b ∈ U, ¬ b ∣ s.natAbs) :
       p.Coprime U.prod ↔ ∀ b ∈ U, ¬ (b : ℤ) ^ 2 ∣ s * ((U.prod * p : ℕ) : ℤ) := by
   …