OAI/NumberTheory/Ostmann/Arithmetic/ResidueQuotient.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Division by a signed frequency with an explicit loss of precision

The quotient is an actual function on residue classes. It agrees with integer division whenever the frequency divides the represented integer.

  1. theorem OAI.Ostmann.modEq_divide_signed line 14
  2. def OAI.Ostmann.residueQuotient line 25
  3. theorem OAI.Ostmann.residueQuotient_intCast line 29
  4. def OAI.Ostmann.frequencyQuotient line 46
  5. theorem OAI.Ostmann.frequencyQuotient_intCast line 51
  6. theorem OAI.Ostmann.frequencyQuotient_reversal line 59

    Source documentation

    The extra compensation factor is a unit, so it costs no further precision after the signed frequency has been divided out.

    theorem frequencyQuotient_reversal (R M : ℕ) [NeZero M] (s : ℤ)
    (hs : s ≠ 0) (hsR : s.natAbs ∣ R) (u p : ℤ)
    (U : (ZMod M)ˣ) (hU : (U : ZMod M) = u) :
    frequencyQuotient R M s hsR (s * u * p : ZMod (R * M)) * ↑U⁻¹ = p := by
…

    Mentions: OAI.Ostmann.frequencyQuotient