OAI/NumberTheory/Ostmann/Construction/PrimeGuardedAmplitude.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.scheduledPartitionAssignment_pairwise_iff line 13
2. def OAI.Ostmann.primeGuardedCurrentAmplitude line 30
3. theorem OAI.Ostmann.primeGuardedCurrentAmplitude_eq_restricted line 51

   Source documentation

   The full prime guard separates exactly into an injective pivot tuple and the retained branch guard. Pivot coprimality is supplied by the inherited coefficient, so it is not added as a new hypothesis on the main theorem.

   theorem primeGuardedCurrentAmplitude_eq_restricted {I A Z : Type*}
       [Fintype I] [Fintype A] [Fintype Z]
       (role : I → CopyScheduleRole) (χ : I → ∀ p : ℕ, DirichletCharacter ℂ p)
       (κ : I → ℕ → ℂ) (pivot : ℕ → I) (n r : ℕ)
       (e : Fin r ≃ CurrentPivotConstituent role n) (hist : A → FrequencyTree ℤ n)
       (P : Finset ℕ) (hP : ∀ p ∈ P, p.Prime) (Q : Fin r → Finset ℕ)
       (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 → ℝ)
       (hM : ∀ z (x : Fin r → P) a, W z (∏ i, (x i : ℕ)) a ≠ 0 →
         (∏ i, (x i : ℕ)).Coprime ((∏ h, L a h) * ∏ y, U z y)) :
       primeGuardedCurrentAmplitude role χ κ pivot n r e hist P hP Q L U center W μ =
   …

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