PermutedAdditiveCancellation.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Common-center additive phases cancel under the actual matching

theorem OAI.Ostmann.tupleCofactor_equiv line 11
def OAI.Ostmann.primeTupleAdditivePhase line 20
theorem OAI.Ostmann.primeTupleAdditivePhase_equiv line 25
theorem OAI.Ostmann.primeTupleAdditivePhase_norm line 35

theorem OAI.Ostmann.permuted_additive_phase_cancel line 46

Source documentation

This is the exact cancellation needed in both a bulk permutation and an identified diagonal pair; the centers are functions of the actual prime.

theorem permuted_additive_phase_cancel {I J : Type*} [Fintype I] [Fintype J]
    (e : I ≃ J) (p : J → ℕ) (hp : ∀ j, p j ≠ 0) (t : ∀ p : ℕ, ZMod p) (v : ℤ)
    (W₁ W₂ : ℂ) :
    (primeTupleAdditivePhase (fun i => p (e i)) (fun i => hp (e i)) t v * W₁) *
      conj (primeTupleAdditivePhase p hp t v * W₂) = W₁ * conj W₂ := by
…

Mentions: OAI.Ostmann.primeTupleAdditivePhase