OAI/NumberTheory/Ostmann/Construction/InitialMovingCoefficient.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.initialMovingTuple_scale line 11

   Source documentation

   Freezing spectators changes the Fourier scale by their exact product.

   theorem initialMovingTuple_scale (P : Finset ℕ) (b d r : ℕ)
       (sl sr : Fin d → P) (XL XR : P)
       (y : MovingRegularSlot 0 (r + r) (b + b) → P) (X : ℝ) :
       ((∏ i, ((initialMovingTuple b d r sl sr XL XR y i : P) : ℕ) : ℕ) : ℝ) / X =
         ((XL : ℕ) * (XR : ℕ) * (∏ i, (y i : ℕ)) : ℕ) /
           (X / ((∏ i, ((Fin.append sl sr i : P) : ℕ)) : ℕ)) := by
   …

   Mentions: OAI.Ostmann.MovingRegularSlot, OAI.Ostmann.initialMovingTuple

2. theorem OAI.Ostmann.initial_moving_coefficient line 23

   Source documentation

   Distinct original spectators give precisely the cofactor units used by all later histories. Their transforms and the retained phase transform factor without changing the original Fourier weight.

   theorem initial_moving_coefficient (P : Finset ℕ) [∀ p : P, NeZero (p : ℕ)]
       (hP : ∀ p ∈ P, p.Prime) (b d r : ℕ)
       (S : ∀ q : ℕ, Finset (ZMod q)) (fav : ℕ → Bool)
       (sl sr : Fin d → P) (hdistinct : Function.Injective (Fin.append sl sr))
       (XL XR : P) (y : MovingRegularSlot 0 (r + r) (b + b) → P)
       (ψ : 𝓢(ℝ, ℂ)) (X : ℝ) (V : ℕ) :
       let q : Fin (d + d) → ℕ := fun i => ((Fin.append sl sr i : P) : ℕ)
   …

   Mentions: OAI.Ostmann.MovingRegularSlot