OAI/NumberTheory/Ostmann/Construction/ScheduledCurrentAmplitude.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.sampledScheduledPhase line 12
2. theorem OAI.Ostmann.sampledScheduledPhase_factor line 25
3. def OAI.Ostmann.scheduledCurrentAmplitude line 58
4. theorem OAI.Ostmann.scheduledCurrentAmplitude_eq_grouped line 73

   Source documentation

   This equality uses the actual phase and original prime prior on the left, so the following arithmetic transfer does not assume a recurrence for it.

   theorem scheduledCurrentAmplitude_eq_grouped {I A Z : Type*}
       [Fintype I] [Fintype A] [Fintype Z]
       (role : I → CopyScheduleRole) (χ : I → ∀ p : ℕ, DirichletCharacter ℂ p)
       (κ : I → ℕ → ℂ) (pivot : ℕ → I) (hpivot : ∀ k, role (pivot k) = .pivot k)
       (n r : ℕ) (e : Fin r ≃ CurrentPivotConstituent role n) (hist : A → FrequencyTree ℤ n)
       (P : Finset ℕ) (hP : ∀ p ∈ P, p.Prime) (Q : Fin r → Finset ℕ) (S : Finset (Fin r → P))
       (hS : ∀ x ∈ S, Function.Injective x)
       (L : A → CopyScheduleH role n → ℕ) (U : Z → CopyScheduleY role n → ℕ)
       [∀ a h, Fact (L a h).Prime] [∀ z y, Fact (U z y).Prime]
       (center : ∀ p : ℕ, ZMod p) (W : Z → ℕ → A → ℂ) (μ : Z → ℝ)
       (hsupport : ∀ z x, x ∈ S → ∀ a, W z (∏ i, (x i : ℕ)) a ≠ 0 →
         Pairwise (fun i j => (Sum.elim (L a) (U z) i).Coprime (Sum.elim (L a) (U z) j)) ∧
   …

   Mentions: OAI.Ostmann.CopyScheduleRole, OAI.Ostmann.CurrentPivotConstituent, OAI.Ostmann.FrequencyTree, OAI.Ostmann.CopyScheduleH, OAI.Ostmann.CopyScheduleY