OAI/NumberTheory/Ostmann/Arithmetic/MovingOneGiant.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.movingOneGiantModuli line 17
2. instance OAI.Ostmann.movingOneGiantModuli_prime line 20
3. instance OAI.Ostmann.movingOneGiantModuli_neZero line 25
4. def OAI.Ostmann.movingOneGiantFactors line 30
5. theorem OAI.Ostmann.movingOneGiantModuli_product line 36
6. theorem OAI.Ostmann.movingOneGiantFactors_giant_norm line 41
7. theorem OAI.Ostmann.movingOneGiantFactors_neg line 50
8. theorem OAI.Ostmann.movingOneGiant_restored line 66

   Source documentation

   The restored full factor is in the order required by giant transfer.

   theorem movingOneGiant_restored {σ : Type*} (value : σ → ℕ)
       (n r m : ℕ) (u : TreeLeafIndex n × Fin 4 → σ)
       (y : MovingRegularSlot n r m → σ) (P X : ℕ)
       (hP : P ≠ 0) (hX : X ≠ 0) (hu : ∀ i, value (u i) ≠ 0) (hy : ∀ i, value (y i) ≠ 0)
       (greg ggiant : ∀ q : ℕ, ZMod q → ℂ) (favorable : ℕ → Bool) (D : ℕ) (s : ℤ) :
       let _ : NeZero P := ⟨hP⟩
   …

   Mentions: OAI.Ostmann.TreeLeafIndex, OAI.Ostmann.MovingRegularSlot

9. theorem OAI.Ostmann.movingOneGiant_restored_average line 94

   Source documentation

   The original compensation, giant, and surviving priors may be left abstract while reindexing their common full Fourier factor.

   theorem movingOneGiant_restored_average {σ A : Type} [Fintype σ] [Fintype A]
       (value : σ → ℕ) (hvalue : ∀ z, value z ≠ 0) (n r m : ℕ)
       (P : Finset ℕ) (hP : ∀ p : P, (p : ℕ) ≠ 0)
       (X : A → ℕ) (hX : ∀ a, X a ≠ 0) (y : A → MovingRegularSlot n r m → σ)
       (v : A → ℤ) (D : ℕ)
       (greg ggiant : ∀ q : ℕ, ZMod q → ℂ) (favorable : ℕ → Bool)
       (wU : (TreeLeafIndex n × Fin 4 → σ) → ℂ) (wP : P → ℂ)
       (W : (TreeLeafIndex n × Fin 4 → σ) → P → A → ℂ) :
       let _ : ∀ p : P, NeZero (p : ℕ) := fun p => ⟨hP p⟩
   …

   Mentions: OAI.Ostmann.MovingRegularSlot, OAI.Ostmann.TreeLeafIndex