MovingSpectatorZero.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The spectator zero convention eliminates inserted nonunits

theorem OAI.Ostmann.movingSlotSpectator_zero line 12

Source documentation

A giant which is zero at an outside prime survives along one child path until a leaf. Its zero contribution is thus forced by the original transform.

theorem movingSlotSpectator_zero {σ : Type*} {q : ℕ} [Fact q.Prime]
    (value : σ → ℕ) (g : ZMod q → ℂ) (hg : g 0 = 0) (D : (ZMod q)ˣ)
    {n : ℕ} (T : MovingSlotData σ n) (XL XR : ℕ)
    (hzero : (XL : ZMod q) = 0 ∨ (XR : ZMod q) = 0) :
    movingSlotSpectator value g D T XL XR = 0 := by
…

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

theorem OAI.Ostmann.movingSlotWeight_spectator_of_zero line 31

Source documentation

For the actual transforms (which vanish at zero), no extra hypothesis that the composite pivot is a unit is needed for spectator factorization.

theorem movingSlotWeight_spectator_of_zero {σ : Type*} {q : ℕ} [Fact q.Prime]
    (value : σ → ℕ) (childBound pivotBound : ℕ → ℕ)
    (F : MovingSlotState σ → ℤ → ℂ)
    (extra : MovingSlotState σ → ℤ → ℤ → ℤ → ℝ)
    (g : ZMod q → ℂ) (hg : g 0 = 0) (D : (ZMod q)ˣ)
    {n : ℕ} (T : MovingSlotData σ n) (t : FrequencyTree ℤ n) (hT : T.Follows t)
    (XL XR : ℕ) :
    recursiveTransferWeight (movingSlotSystem value childBound pivotBound)
        (fun x s => F x s * spectatorHistoryLeaf (movingSlotModulus value) g D x s)
        (movingSlotCutoff value childBound pivotBound extra) n ⟨n, T, XL, XR⟩ t =
      recursiveTransferWeight (movingSlotSystem value childBound pivotBound) F
        (movingSlotCutoff value childBound pivotBound extra) n ⟨n, T, XL, XR⟩ t *
…

Mentions: OAI.Ostmann.MovingSlotState, OAI.Ostmann.MovingSlotData, OAI.Ostmann.FrequencyTree, OAI.Ostmann.recursiveTransferWeight, OAI.Ostmann.movingSlotSystem, OAI.Ostmann.spectatorHistoryLeaf, OAI.Ostmann.movingSlotModulus, OAI.Ostmann.movingSlotCutoff