OAI/NumberTheory/JointDickman/Amplification/ReducedArcLifts.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Exact enumeration of the lifts of reduced coefficient arcs

  1. theorem OAI.JointDickman.val_finEquiv line 11
  2. def OAI.JointDickman.arcLiftEquiv line 17
  3. theorem OAI.JointDickman.arcLiftEquiv_val line 21
  4. theorem OAI.JointDickman.arcLiftEquiv_coprime line 25
  5. theorem OAI.JointDickman.reducedArc_lift_count line 32

    Source documentation

    Each reduced coefficient fraction has exactly j lifts, without a coprimality assumption between j and q.

    theorem reducedArc_lift_count (j q : ℕ) [NeZero j] [NeZero q] [NeZero (j*q)] :
    (∑ h : ZMod (j*q), if h.val.Coprime q then (1 : ℝ) else 0) = (j : ℝ)*q.totient := by
…
  6. theorem OAI.JointDickman.arcLiftEquiv_location line 50