OAI/NumberTheory/Ostmann/Arithmetic/ReconstructedPhaseWeight.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.branchPairwise_parts line 12
2. def OAI.Ostmann.retainedWeightedCoefficient line 22
3. def OAI.Ostmann.copiedWeightedAmplitude line 33
4. theorem OAI.Ostmann.reconstructedOffDiagonal_eq_copiedWeightedAmplitude line 52

   Source documentation

   Only the original branch supports are hypotheses. Cross-copy distinctness and the units at the new root are consequences of the equation and ranges.

   theorem reconstructedOffDiagonal_eq_copiedWeightedAmplitude
       {A H Y : Type*} [Fintype A] [Fintype H] [Fintype Y]
       (L : A → H → ℕ) (U : Y → ℕ)
       [∀ a h, Fact (L a h).Prime] [∀ y, Fact (U y).Prime]
       (t : ∀ p : ℕ, ZMod p)
       (χH : H → ∀ p : ℕ, DirichletCharacter ℂ p)
       (χY : Y → ∀ p : ℕ, DirichletCharacter ℂ p)
       (b : Option (H ⊕ Y) → Option (H ⊕ Y) → ℤ)
       (ν : A → H → ℂ) (νY : A → Y → ℂ) (v : A → ℤ)
       (W : ℕ → A → ℂ) (T : Finset ℕ) (B K V : ℕ)
       (hT : ∀ M ∈ T, 0 < M)
       (hsupport : ∀ M ∈ T, ∀ a, W M a ≠ 0 →
   …