OAI/NumberTheory/Ostmann/Arithmetic/MovingTransferTransform.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.movingTaggedTransform line 13

   Source documentation

   A common formula for regular factors and the two marked giant phases. Using the modulus as an explicit argument makes reindexing independent of presentation of the dependent residue types.

   noncomputable def movingTaggedTransform {I : Type*} [Fintype I]
       (p : I → ℕ) (giant : I → Bool)
       (greg ggiant : ∀ q : ℕ, ZMod q → ℂ) (favorable : ℕ → Bool) (D : ℕ) (s : ℤ) : ℂ :=
   …

2. theorem OAI.Ostmann.movingTaggedTransform_equiv line 21
3. theorem OAI.Ostmann.movingTaggedTransform_restored line 36

   Source documentation

   Restoring a compensation sample places precisely the extracted giant and its compensation factors before the surviving giant and regular factors.

   theorem movingTaggedTransform_restored {A : Type*} (value : A → ℕ)
       (n r m : ℕ) (u : TreeLeafIndex n × Fin 4 → A)
       (y : MovingRegularSlot n r m → A) (XL XR : ℕ)
       (hXL : XL ≠ 0) (hXR : XR ≠ 0)
       (hu : ∀ i, value (u i) ≠ 0) (hy : ∀ i, value (y i) ≠ 0)
       (greg ggiant : ∀ q : ℕ, ZMod q → ℂ) (favorable : ℕ → Bool) (D : ℕ) (s : ℤ) :
       movingTaggedTransform
         (Sum.elim (fun b : Bool => if b then XL else XR)
           (value ∘ movingRestoreSample n r m u y))
         (Sum.elim (fun _ => true) (fun _ => false)) greg ggiant favorable D s =
       movingTaggedTransform
         (Sum.elim (Sum.elim (fun _ : Unit => XL) (value ∘ u))
   …

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