OAI/NumberTheory/Ostmann/Arithmetic/MovingPairedTransform.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.movingPairedGiantEquiv line 15
2. theorem OAI.Ostmann.movingTaggedTransform_paired line 43

   Source documentation

   Both surviving giants and every regular factor occur once in the next full transform. This is independent of the reconstructed pivot.

   theorem movingTaggedTransform_paired {A : Type*} (value : A → ℕ)
       (n r m : ℕ) (left right : MovingRegularSlot n r m → A) (XL XR : ℕ)
       (hXL : XL ≠ 0) (hXR : XR ≠ 0)
       (hleft : ∀ i, value (left i) ≠ 0) (hright : ∀ i, value (right i) ≠ 0)
       (greg ggiant : ∀ q : ℕ, ZMod q → ℂ) (favorable : ℕ → Bool) (D : ℕ) (s : ℤ) :
       movingTaggedTransform
         (Sum.elim (Sum.elim (fun _ : Unit => XL) (value ∘ left))
           (Sum.elim (fun _ : Unit => XR) (value ∘ right)))
         (Sum.elim (Sum.elim (fun _ : Unit => true) (fun _ => false))
           (Sum.elim (fun _ : Unit => true) (fun _ => false))) greg ggiant favorable D s =
       movingTaggedTransform
         (Sum.elim (fun b : Bool => if b then XL else XR)
   …

   Mentions: OAI.Ostmann.MovingRegularSlot, OAI.Ostmann.movingTaggedTransform

3. theorem OAI.Ostmann.movingTaggedTransform_full line 86

   Source documentation

   The tagged presentation is the same full transform used by the coefficient-to-prime-statistic identity.

   theorem movingTaggedTransform_full {I : Type*} [Fintype I]
       (q : Bool → ℕ) (p : I → ℕ) [∀ b, NeZero (q b)] [∀ i, NeZero (p i)]
       (greg ggiant : ∀ q : ℕ, ZMod q → ℂ) (favorable : ℕ → Bool) (D : ℕ) (s : ℤ) :
       movingTaggedTransform (Sum.elim q p)
         (Sum.elim (fun _ => true) (fun _ => false)) greg ggiant favorable D s =
       movingRegularTransform (Sum.elim q p)
         (fun i => match i with
           | .inl b => fun t => if favorable (q b) then complexUnitPhase (ggiant (q b) t) else 0
           | .inr j => greg (p j)) D s := by
   …

   Mentions: OAI.Ostmann.movingTaggedTransform, OAI.Ostmann.movingRegularTransform, OAI.Ostmann.complexUnitPhase