SignedAtomSchedule.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The positive and conjugate atom copies retain their original characters

def OAI.Ostmann.signedAtomRole line 12
Source documentation
The first squared-amplitude branch supplies the copied roles. The other branch is retained outside throughout the transfer schedule.
```
def signedAtomRole {I : Type*} (role : I → CopyScheduleRole) :
    Bool × I → CopyScheduleRole := fun i => if i.1 then role i.2 else .outside
```
Mentions: OAI.Ostmann.CopyScheduleRole
def OAI.Ostmann.signedAtomCharacter line 15
theorem OAI.Ostmann.signedAtomCharacter_active line 20

theorem OAI.Ostmann.signedAtomCharacter_matching line 31

Source documentation

Even negative transfer copies keep the character of their original atom. Every prime-slot matching in H therefore preserves the character assignment.

theorem signedAtomCharacter_matching {I : Type*} (role : I → CopyScheduleRole)
    (size : I → ℕ) (χ : ∀ p : ℕ, DirichletCharacter ℂ p) (n : ℕ)
    (e : Equiv.Perm (CopyScheduleH
      (fun i : Σ j : Bool × I, Fin (size j.2) => signedAtomRole role i.1) n))
    (h : CopyScheduleH
      (fun i : Σ j : Bool × I, Fin (size j.2) => signedAtomRole role i.1) n) :
    signedAtomCharacter size χ (copyScheduleOrigin n (e h).val) =
      signedAtomCharacter size χ (copyScheduleOrigin n h.val) :=
…

Mentions: OAI.Ostmann.CopyScheduleRole, OAI.Ostmann.CopyScheduleH, OAI.Ostmann.signedAtomRole, OAI.Ostmann.signedAtomCharacter, OAI.Ostmann.copyScheduleOrigin