ArithmeticPrecision.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The exact loss of frequency precision at a reversing node

theorem OAI.Ostmann.modEq_cancel_coprime_left line 10

theorem OAI.Ostmann.reversal_residue_precision line 18

Source documentation

Division by s consumes one copy of R; division by its unit factor consumes none.

theorem reversal_residue_precision (R s u u' N N' p p' : ℤ) (k : ℕ)
    (hs : s ≠ 0) (hsR : s ∣ R) (hu : IsCoprime u R)
    (hN : N = s * u * p) (hN' : N' = s * u' * p')
    (hmod : N ≡ N' [ZMOD R ^ (k + 1)]) (humod : u ≡ u' [ZMOD R ^ k]) :
    p ≡ p' [ZMOD R ^ k] := by
…

theorem OAI.Ostmann.reversal_chain_residue_precision line 33

Source documentation

At every depth of a chain the remaining power still determines the reconstructed integer.

theorem reversal_chain_residue_precision (R : ℤ) (s u u' v v' : ℕ → ℤ) (k : ℕ)
    (hs : ∀ j, s j ≠ 0) (hsR : ∀ j, s j ∣ R) (hu : ∀ j, IsCoprime (u j) R)
    (hv : ∀ j, v j = s j * u j * v (j + 1))
    (hv' : ∀ j, v' j = s j * u' j * v' (j + 1))
    (hmod : v 0 ≡ v' 0 [ZMOD R ^ (k + 1)])
    (humod : ∀ j, u j ≡ u' j [ZMOD R ^ (k + 1)]) :
    ∀ j ≤ k + 1, v j ≡ v' j [ZMOD R ^ (k + 1 - j)] := by
…