OAI/NumberTheory/Ostmann/Construction/TransferDirectedPhase.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.copiedSlotCharacter line 12

   Source documentation

   Characters keep their original slot identity when a slot is copied.

   def copiedSlotCharacter {H Y : Type*}
       (χH : H → ∀ p : ℕ, DirichletCharacter ℂ p)
       (χY : Y → ∀ p : ℕ, DirichletCharacter ℂ p) :
       (Bool × H) ⊕ Y → ∀ p : ℕ, DirichletCharacter ℂ p
     | .inl (_, h) => χH h
     | .inr y => χY y

2. def OAI.Ostmann.copiedSlotUnary line 19
3. theorem OAI.Ostmann.transfer_directed_phase line 34

   Source documentation

   The previously proved complete transfer identity has exactly the directed phase maintained by the iteration, with no residual local factors.

   theorem transfer_directed_phase {H Y : Type*} [Fintype H] [Fintype Y]
       (q : (Bool × H) ⊕ Y → ℕ) [∀ i, Fact (q i).Prime]
       (t : ∀ p : ℕ, ZMod p)
       (χH : H → ∀ p : ℕ, DirichletCharacter ℂ p)
       (χY : Y → ∀ p : ℕ, DirichletCharacter ℂ p)
       (b : Option (H ⊕ Y) → Option (H ⊕ Y) → ℤ)
       (νL νR : H → ℂ) (νYL νYR : Y → ℂ) (M : ℕ) (v w s : ℤ)
       (hrel : v * (∏ h, q (.inl (false, h))) - w * (∏ h, q (.inl (true, h))) = s * M)
       (hc : Pairwise (fun i j => (q i).Coprime (q j)))
       (hM : ∀ i, M.Coprime (q i))
       (hs : ∀ i, IsUnit (s : ZMod (q i)))
       (hb : ∀ y, b (some (.inr y)) (some (.inr y)) = 0) :
   …