CharacterLiteralDiagonal.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The literal diagonal of the original signed character prior

theorem OAI.Ostmann.character_literal_diagonal_split line 12

Source documentation

The split uses disjointness only between the true bulk and the remaining original cells. The selected word bin removes the zero frequency.

theorem character_literal_diagonal_split {k : ℕ} (m : ℕ) (r : Fin k → ℕ) (f n : ℕ)
    (Q : Fin (m + 1) → Finset ℕ) (U : Finset ℕ)
    (R : (v : CharacterCell k) → Fin (characterCellSize r f v) → Finset ℕ)
    (hQ : ∀ i : Fin m, Q i.succ = U) (htop : Disjoint U (Q 0))
    (hR : ∀ v i, Disjoint U (R v i))
    (χ : (Σ v, Fin (characterSize m r f v)) → ∀ p : ℕ, DirichletCharacter ℂ p)
    (κ : (Σ v, Fin (characterSize m r f v)) → ℕ → ℂ)
    (pivot : ℕ → (Σ v, Fin (characterSize m r f v)))
    (P : Finset ℕ) (hP : ∀ p ∈ P, p.Prime)
    (J : ℕ) (hJ : 0 < J) (cellLo cellHi : CharacterCell k → ℕ)
    (V cap : ℕ → ℕ) (leaf : ScheduleAtomState (characterRole k) → ℤ → ℂ)
    (center : ∀ p : ℕ, ZMod p) (p : CharacterRole k)
…

Mentions: OAI.Ostmann.CharacterCell, OAI.Ostmann.characterCellSize, OAI.Ostmann.characterSize, OAI.Ostmann.ScheduleAtomState, OAI.Ostmann.characterRole, OAI.Ostmann.CharacterRole