OAI/NumberTheory/Ostmann/Arithmetic/MovingInternalLocalFactor.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Actual internal-prime factors before averaging

  1. def OAI.Ostmann.movingInternalLocalSupport line 12

    Source documentation

    All occurrences of a fixed internal prime impose their line modulo p and exclude its zero lift modulo p². Repeated occurrences remain simultaneous.

    noncomputable def movingInternalLocalSupport {σ : Type*} (value : σ → ℕ)
    {n : ℕ} (T : MovingSlotData σ n) (p : ℕ) (x y : ZMod (p ^ 2)) : Prop :=
…

    Mentions: OAI.Ostmann.MovingSlotData

  2. theorem OAI.Ostmann.movingInternalLocalSupport_iff line 20
  3. def OAI.Ostmann.movingInternalPairFactor line 50
  4. theorem OAI.Ostmann.movingInternalPairFactor_product line 55