MovingSignedSpectator.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Signed residue representatives for the literal spectator recursion

theorem OAI.Ostmann.int_modEq_ediv line 12
Source documentation
Clearing the input period makes division compatible with congruence, even when the individual numerators are not divisible by the denominator.
```
theorem int_modEq_ediv (c m x y : ℤ) (hc : c ≠ 0)
    (h : x ≡ y [ZMOD c * m]) : x / c ≡ y / c [ZMOD m] := by
…
```
def OAI.Ostmann.MovingSlotReversal.signedPivot line 24
theorem OAI.Ostmann.MovingSlotReversal.signedPivot_nat line 30
def OAI.Ostmann.movingSignedSpectator line 41

theorem OAI.Ostmann.movingSignedSpectator_nat line 54

Source documentation

Signed representatives agree with the original natural recursion on its proved integral support. No extra unit condition is imposed.

theorem movingSignedSpectator_nat {σ : Type*} {q : ℕ} [Fact q.Prime]
    (value : σ → ℕ) (hvalue : ∀ i, value i ≠ 0) (g : ZMod q → ℂ) (D : (ZMod q)ˣ)
    {n : ℕ} (T : MovingSlotData σ n) (hf : T.Frequencies (· ≠ 0)) (XL XR : ℕ)
    (hI : T.Integral value XL XR) :
    movingSignedSpectator value g D T XL XR = movingSlotSpectator value g D T XL XR := by
…

Mentions: OAI.Ostmann.MovingSlotData, OAI.Ostmann.movingSignedSpectator, OAI.Ostmann.movingSlotSpectator

theorem OAI.Ostmann.MovingSlotReversal.signedPivot_modEq line 70

theorem OAI.Ostmann.movingSignedSpectator_modEq line 83

Source documentation

Signed representatives are periodic before imposing any real support.

theorem movingSignedSpectator_modEq {σ : Type*} {q : ℕ} [Fact q.Prime]
    (value : σ → ℕ) (hvalue : ∀ i, value i ≠ 0)
    (g : ZMod q → ℂ) (D : (ZMod q)ˣ) {n : ℕ} (T : MovingSlotData σ n)
    (hf : T.Frequencies (· ≠ 0)) (XL XR YL YR : ℤ)
    (hL : (XL : ℤ) ≡ (YL : ℤ) [ZMOD (q : ℤ) * movingSpectatorDenominator value T])
    (hR : (XR : ℤ) ≡ (YR : ℤ) [ZMOD (q : ℤ) * movingSpectatorDenominator value T]) :
    movingSignedSpectator value g D T XL XR = movingSignedSpectator value g D T YL YR := by
…

Mentions: OAI.Ostmann.MovingSlotData, OAI.Ostmann.movingSpectatorDenominator, OAI.Ostmann.movingSignedSpectator

theorem OAI.Ostmann.movingSlotSpectator_eq_residue line 135
theorem OAI.Ostmann.movingSignedSpectator_norm line 146