MovingSeparatedSupportedPair.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The original supported prime pair at the separated arithmetic modulus

def OAI.Ostmann.movingOriginalSupportedPair line 11

Source documentation

The literal product in the original sampled coefficient square.

noncomputable def movingOriginalSupportedPair {σ I : Type*} (q : I → ℕ)
    [∀ i, Fact (q i).Prime] (value : σ → ℕ) (outside : List ℕ)
    (childBound pivotBound : ℕ → ℕ)
    (F : Bool → {n : ℕ} → MovingSlotData σ n → ℤ → ℂ)
    (E : Bool → {n : ℕ} → MovingSlotData σ n → ℤ → ℤ → ℤ → ℝ)
    (g : ∀ i, ZMod (q i) → ℂ) (Dq : Bool → ∀ i, (ZMod (q i))ˣ) (S : Finset I)
    (ψ : 𝓢(ℝ, ℂ)) (X lo hi : ℝ) (φ : ℝ → ℝ) (G : ℕ → ℝ)
    {n : ℕ} (T : Bool → MovingSlotData σ n) (t : Bool → FrequencyTree ℤ n)
    (XL XR : ℕ) : ℂ :=
…

Mentions: OAI.Ostmann.MovingSlotData, OAI.Ostmann.FrequencyTree

theorem OAI.Ostmann.movingOriginalSupportedPair_separated_factor line 27