OAI/NumberTheory/Ostmann/Arithmetic/MovingFrequencyResidues.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Frequency residues with compensation factors inverted

Unlike the signed integer recursion, this recursion divides only by the frequency. Compensation factors are inverted modulo a frequency power, so no internal prime enters its period. One power is consumed per reversal.

  1. def OAI.Ostmann.MovingSlotReversal.signedNumerator line 16
  2. def OAI.Ostmann.MovingSlotReversal.frequencyPivot line 21
  3. theorem OAI.Ostmann.coprime_bezout_inverse_modEq line 26
  4. theorem OAI.Ostmann.MovingSlotReversal.signedNumerator_modEq line 35
  5. theorem OAI.Ostmann.MovingSlotReversal.frequencyPivot_modEq line 41
  6. theorem OAI.Ostmann.MovingSlotReversal.frequencyPivot_nat_modEq line 51
  7. def OAI.Ostmann.movingFrequencyLocalUnits line 65
  8. def OAI.Ostmann.movingFrequencyGate line 69
  9. theorem OAI.Ostmann.movingFrequencyLocalUnits_modEq line 78
  10. theorem OAI.Ostmann.MovingSlotData.frequencyProduct_node_dvd line 85
  11. theorem OAI.Ostmann.movingFrequencyGate_modEq line 98

    Source documentation

    The entire frequency block has a period containing only frequencies. The compensation primes have disappeared from the period.

    theorem movingFrequencyGate_modEq {σ : Type*} (value : σ → ℕ) (R : ℤ)
    {n : ℕ} (T : MovingSlotData σ n) (hf : T.Frequencies (· ≠ 0))
    (hR : T.frequencyProduct ∣ R) (XL XR YL YR : ℤ)
    (hL : XL ≡ YL [ZMOD R ^ (n + 1)]) (hRight : XR ≡ YR [ZMOD R ^ (n + 1)]) :
    movingFrequencyGate value R T XL XR ↔ movingFrequencyGate value R T YL YR := by
…

    Mentions: OAI.Ostmann.MovingSlotData, OAI.Ostmann.movingFrequencyGate

  12. theorem OAI.Ostmann.movingNaturalProduct_coprime line 124
  13. theorem OAI.Ostmann.movingFrequencyGate_nat_iff line 136

    Source documentation

    On an original integral history this frequency-only recursion is exactly the original subtree-frequency unit support. No stronger giant unit test is inserted and all frequency divisibility tests remain in the new recursion.

    theorem movingFrequencyGate_nat_iff {σ : Type*} (value : σ → ℕ) (R : ℤ)
    (hsmall : ∀ i, IsCoprime (value i : ℤ) R)
    {n : ℕ} (T : MovingSlotData σ n) (hf : T.Frequencies (· ≠ 0))
    (hR : T.frequencyProduct ∣ R) (XL XR : ℕ) (hI : T.Integral value XL XR) :
    movingFrequencyGate value R T XL XR ↔ movingAuxiliaryUnits value [] T XL XR := by
…

    Mentions: OAI.Ostmann.MovingSlotData, OAI.Ostmann.movingFrequencyGate, OAI.Ostmann.movingAuxiliaryUnits