DivisorEdgeEndpoints.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The actual integer endpoints of a divisor-graph edge

theorem OAI.JointDickman.natural_divisor_edge_endpoints line 14

Source documentation

Forward reindexing at the actual natural quotients, for either sign of the lag. The shifted endpoint is positive automatically.

theorem natural_divisor_edge_endpoints {a b c m : ℕ} {j : ℤ}
    (hc : 0 < c) (ha : c ∣ a*m+1) (hb : c ∣ b*m+1)
    (he : (a : ℤ)-b = j*c) :
    ((b*((a*m+1)/c) : ℕ) : ℤ)+j = ((a*((b*m+1)/c) : ℕ) : ℤ) := by
…

theorem OAI.JointDickman.natural_divisor_edge_inverse line 29

Source documentation

The inverse congruence reconstructs a nonnegative multiplier. It uses only coprimality with the lag and positivity of the endpoint.

theorem natural_divisor_edge_inverse {a b c n : ℕ} {j : ℤ}
    (ha : 0 < a) (hc : 0 < c) (hn : 0 < n) (hb : b ∣ n)
    (he : (a : ℤ)-b = j*c) (hcop : a.Coprime j.natAbs)
    (hdiv : (a : ℤ) ∣ (n : ℤ)+j) :
    ∃! m : ℕ, c*(n/b) = a*m+1 := by
…

theorem OAI.JointDickman.centered_binLabel_graph_endpoints line 63

Source documentation

Fixed-multiplier invariance identifies each original centered label with its new graph endpoint. This holds simultaneously for all coefficients.

theorem centered_binLabel_graph_endpoints {ι : Type*} [Fintype ι]
    (J : ℕ) (hJ : 0 < J) (k : ι → ℕ) (hk : ∀ i, 1 ≤ k i)
    (z : ι → ℂ) (μ : ℂ) (B : ℕ) :
    ∀ᶠ N : ℕ in atTop, ∀ D ∈ (auxiliaryPrimes B).powerset,
      ∀ E ∈ (auxiliaryPrimes B).powerset, ∀ a m : ℕ,
      (∏ p ∈ D, p) ∣ a*m+1 →
      movingBinLabel J k z N (a*m+1)-μ =
        movingBinLabel J k z N ((∏ p ∈ E, p)*((a*m+1)/(∏ p ∈ D, p)))-μ := by
…

Mentions: OAI.JointDickman.auxiliaryPrimes, OAI.JointDickman.movingBinLabel