GiantTransformProduct.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Recombining the two giant phases with the common regular transform

theorem OAI.Ostmann.bool_tupleCofactor line 15

theorem OAI.Ostmann.movingRegularTransform_two_giant_phases line 24

Source documentation

The cofactor formula in the two-prime statistic is exactly the full Fourier transform of the original ordered regular-prime tuple.

theorem movingRegularTransform_two_giant_phases {I : Type*} [Fintype I]
    (q : Bool → ℕ) (p : I → ℕ) [∀ b, Fact (q b).Prime] [∀ i, Fact (p i).Prime]
    (hp : Function.Injective p) (greg ggiant : ∀ r : ℕ, ZMod r → ℂ)
    (favorable : ℕ → Bool) (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 =
    ((if favorable (q true) then complexUnitPhase
      (ggiant (q true) ((s : ZMod (q true)) *
        ((D * q false * (∏ i, p i) : ℕ) : ZMod (q true))⁻¹)) else 0) *
      (if favorable (q false) then complexUnitPhase
…

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

theorem OAI.Ostmann.movingGiantPhase_regularFactor_eq line 72

Source documentation

The common factor actually used by the statistic is this same cofactor product, including the two giant denominators.

theorem movingGiantPhase_regularFactor_eq {σ B I : Type*} [Fintype I] {n : ℕ}
    (value : σ → ℕ) (outside : List ℕ) (small bulk : TreeLeafTuple (List B) n)
    (y : B → σ) (q : Bool → ℕ) (p : I → ℕ) [∀ b, Fact (q b).Prime]
    (hprod : MovingSlotReversal.naturalProduct (value ∘ y)
      (flattenMovingSlots n small ++ flattenMovingSlots n bulk) = ∏ i, p i)
    (greg ggiant : ∀ r : ℕ, ZMod r → ℂ) (favorable : ℕ → Bool) (s : ℤ) :
    movingGiantPhase value outside small bulk ggiant favorable s y
        (Real.log (q true)) (Real.log (q false)) *
      movingExternalRegularFactor value outside small bulk greg s y
        (Real.log (q true)) (Real.log (q false)) =
    ((if favorable (q true) then complexUnitPhase
      (ggiant (q true) ((s : ZMod (q true)) *
…

Mentions: OAI.Ostmann.TreeLeafTuple, OAI.Ostmann.MovingSlotReversal.naturalProduct, OAI.Ostmann.flattenMovingSlots, OAI.Ostmann.movingGiantPhase, OAI.Ostmann.movingExternalRegularFactor, OAI.Ostmann.complexUnitPhase