RetainedAdditiveMatching.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The common-center additive phase cancels on the matched diagonal

theorem OAI.Ostmann.retainedAdditiveBranch_equiv line 18
theorem OAI.Ostmann.retainedAdditiveBranch_norm line 28
theorem OAI.Ostmann.retained_additive_matching_cancel line 33

theorem OAI.Ostmann.retainedPrimePhase_matching line 49

Source documentation

The integer pivot and the common prime centers introduce no residual additive phase in a matched pair, even when the character rows differ.

theorem retainedPrimePhase_matching (e : Equiv.Perm H)
    (center : ∀ p : ℕ, ZMod p)
    (χH χH' : H → ∀ p : ℕ, DirichletCharacter ℂ p)
    (χY χY' : Y → ∀ p : ℕ, DirichletCharacter ℂ p)
    (b b' : Option (H ⊕ Y) → Option (H ⊕ Y) → ℤ)
    (νH νH' : H → ℂ) (νY νY' : Y → ℂ) (M : ℕ) (v : ℤ) (W W' : ℂ) :
    (W * retainedPrimePhase L U center χH χY b νH νY M v) *
      conj (W' * retainedPrimePhase (fun h => L (e h)) U center χH' χY' b' νH' νY' M v) =
    (W * retainedCharacterBranch L U χH χY b νH νY M) *
      conj (W' * retainedCharacterBranch (fun h => L (e h)) U χH' χY' b' νH' νY' M) := by
…

Mentions: OAI.Ostmann.retainedPrimePhase, OAI.Ostmann.retainedCharacterBranch