DivisorEdgeReindex.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Exact finite transport from multiplier sums to additive graph endpoints

def OAI.JointDickman.divisorEdgeInverse line 10
def OAI.JointDickman.divisorEdgeOld line 12
def OAI.JointDickman.divisorEdgeNew line 15
theorem OAI.JointDickman.divisorEdgeInverse_eq line 19
theorem OAI.JointDickman.divisorEdge_forward_mem line 26
Source documentation
Membership in the multiplier sum gives an endpoint with exactly the inverse multiplier; the finite endpoints include every original summand.
```
theorem divisorEdge_forward_mem {a b c N : ℕ} {j : ℤ}
    (ha : 0 < a) (hb : 0 < b) (hc : 0 < c)
    (he : (a : ℤ)-b = j*c) {m : ℕ} (hm : m ∈ divisorEdgeOld a b c N) :
    b*((a*m+1)/c) ∈ divisorEdgeNew a b c N j ∧
      divisorEdgeInverse a b c (b*((a*m+1)/c)) = m := by
…
```
Mentions: OAI.JointDickman.divisorEdgeOld, OAI.JointDickman.divisorEdgeNew, OAI.JointDickman.divisorEdgeInverse

theorem OAI.JointDickman.divisorEdge_inverse_mem line 54

Source documentation

Every allowed endpoint reconstructs one old multiplier.

theorem divisorEdge_inverse_mem {a b c N : ℕ} {j : ℤ}
    (ha : 0 < a) (hc : 0 < c) (he : (a : ℤ)-b = j*c)
    (hcop : a.Coprime j.natAbs) {n : ℕ} (hn : n ∈ divisorEdgeNew a b c N j) :
    divisorEdgeInverse a b c n ∈ divisorEdgeOld a b c N ∧
      b*((a*divisorEdgeInverse a b c n+1)/c) = n := by
…

Mentions: OAI.JointDickman.divisorEdgeNew, OAI.JointDickman.divisorEdgeInverse, OAI.JointDickman.divisorEdgeOld

theorem OAI.JointDickman.sum_divisorEdge_reindex line 85

Source documentation

A bijective finite-sum reindexing, with no error term or multiplicity.

theorem sum_divisorEdge_reindex {M : Type*} [AddCommMonoid M]
    {a b c : ℕ} (ha : 0 < a) (hb : 0 < b) (hc : 0 < c)
    {j : ℤ} (he : (a : ℤ)-b = j*c) (hcop : a.Coprime j.natAbs)
    (N : ℕ) (F : ℕ → M) :
    (∑ m ∈ divisorEdgeOld a b c N, F m) =
      ∑ n ∈ divisorEdgeNew a b c N j, F (divisorEdgeInverse a b c n) := by
…

Mentions: OAI.JointDickman.divisorEdgeOld, OAI.JointDickman.divisorEdgeNew, OAI.JointDickman.divisorEdgeInverse