RationalDivisorLift.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem337.rational_divisor_sum_of_divisible line 10

Source documentation

An integral positive sum divisible by p gives a common-denominator representation of p; products of divisors of P divide P².

theorem rational_divisor_sum_of_divisible {k P p : ℕ} (hk : 0 < k)
    (hp : 0 < p) (a b : Fin k → ℕ)
    (ha : ∀ i, 0 < a i) (hb : ∀ i, 0 < b i)
    (had : ∀ i, a i ∣ P) (hbd : ∀ i, b i ∣ P)
    (hdiv : p ∣ ∑ i, a i * b i) :
    ∃ t : ℕ, 0 < t ∧ (∀ i, 0 < a i * b i ∧ a i * b i ∣ P ^ 2) ∧
      (p : ℚ) = ∑ i, ((a i * b i : ℕ) : ℚ) / t := by
…

theorem OAI.Problem337.rational_divisor_sum_of_zmod_zero line 34

Source documentation

The preceding lifting lemma can take a modular zero-sum directly.

theorem rational_divisor_sum_of_zmod_zero {k P p : ℕ} (hk : 0 < k)
    (hp : 0 < p) (a b : Fin k → ℕ)
    (ha : ∀ i, 0 < a i) (hb : ∀ i, 0 < b i)
    (had : ∀ i, a i ∣ P) (hbd : ∀ i, b i ∣ P)
    (hzero : (∑ i, (a i : ZMod p) * (b i : ZMod p)) = 0) :
    ∃ t : ℕ, 0 < t ∧ (∀ i, 0 < a i * b i ∧ a i * b i ∣ P ^ 2) ∧
      (p : ℚ) = ∑ i, ((a i * b i : ℕ) : ℚ) / t := by
…

theorem OAI.Problem337.rational_divisor_sum_of_residue_products line 46

Source documentation

Lift products of residue classes represented by positive divisors.

theorem rational_divisor_sum_of_residue_products {k P p : ℕ}
    (hk : 0 < k) (hp : 0 < p) (x y : Fin k → ZMod p)
    (hx : ∀ i, x i ∈ P.divisors.image (fun a : ℕ => (a : ZMod p)))
    (hy : ∀ i, y i ∈ P.divisors.image (fun a : ℕ => (a : ZMod p)))
    (hsum : (∑ i, x i * y i) = 0) :
    ∃ e : Fin k → ℕ, ∃ t : ℕ, 0 < t ∧
      (∀ i, 0 < e i ∧ e i ∣ P ^ 2) ∧
      (p : ℚ) = ∑ i, (e i : ℚ) / t := by
…