OAI/NumberTheory/Ostmann/Construction/PrimeProductMatching.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.prime_dvd_prime_product line 15
2. theorem OAI.Ostmann.prime_product_matching_exists_unique line 21
3. theorem OAI.Ostmann.prime_product_eq_iff_matching line 49
4. theorem OAI.Ostmann.diagonal_prime_matching line 62

   Source documentation

   Prime factors exceed the leaf frequencies, so the zero transfer numerator has a common frequency and a unique matching of its constituent prime slots.

   theorem diagonal_prime_matching {I J : Type*} [Fintype I] [Fintype J]
       (p : I → ℕ) (q : J → ℕ) (hp : ∀ i, (p i).Prime) (hq : ∀ j, (q j).Prime)
       (hinjp : Function.Injective p) (hinjq : Function.Injective q)
       (v w : ℤ) (hv : v ≠ 0) (hw : w ≠ 0)
       (hvp : ∀ i, v.natAbs < p i) (hwq : ∀ j, w.natAbs < q j) :
       v * (∏ j, q j : ℕ) = w * (∏ i, p i : ℕ) ↔
         v = w ∧ ∃! e : I ≃ J, ∀ i, p i = q (e i) := by
   …

5. theorem OAI.Ostmann.prime_product_matching_sum line 81

   Source documentation

   Replacing the equal-product indicator by the sum over actual matchings introduces no multiplicity, because all prime slots are distinct.

   theorem prime_product_matching_sum {I J : Type*} [Fintype I] [Fintype J]
       (p : I → ℕ) (q : J → ℕ) (hp : ∀ i, (p i).Prime) (hq : ∀ j, (q j).Prime)
       (hinjp : Function.Injective p) (hinjq : Function.Injective q) (z : ℂ) :
       (if (∏ i, p i) = ∏ j, q j then z else 0) =
         ∑ e : I ≃ J, if ∀ i, p i = q (e i) then z else 0 := by
   …