MovingPatternPrimeHaarComparison.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The original finite-pattern prime integral, with its actual CRT law

theorem OAI.Ostmann.PublishedProgressionInput.moving_original_pattern_prime_haar_rate line 17

Source documentation

A direct application of the published progression input to the literal pattern integral. Structural tree and compensation assumptions are derived from the sampler and its prime ranges. The cutoff is uniform in all finite pattern spaces, the sampled assignment, and the spectator list.

theorem PublishedProgressionInput.moving_original_pattern_prime_haar_rate
    (input : PublishedProgressionInput) (n : ℕ) (Cbudget : ℝ) (d : ℕ) :
    ∀ᶠ L : ℝ in atTop,
      ∀ (B C I : Type) [Fintype C] [Fintype I] (N m : ℕ)
        (e : Fin (N + 1) ≃ B ⊕ C) (tierB : B → ℕ) (tierC : C → ℕ)
        (t : Bool → FrequencyTree ℤ n) (small : TreeLeafTuple (List B) n)
        (slot : (TreeLeafIndex n × Fin m) ↪ B) (pattern : Bool × MovingSampleIndex n → C)
        (primes : Finset ℕ) (hprimes : ∀ p ∈ primes, p.Prime)
        (x : Fin (N + 1) → primes)
        (p : I → ℕ) [∀ i, Fact (p i).Prime]
        (g : ∀ i, ZMod (p i) → ℂ) (Dq : ∀ i, (ZMod (p i))ˣ)
        (f : ℤ → ℂ) (outside : List ℕ) (childBound pivotBound : ℕ → ℕ)
…

Mentions: OAI.Ostmann.PublishedProgressionInput, OAI.Ostmann.FrequencyTree, OAI.Ostmann.TreeLeafTuple, OAI.Ostmann.TreeLeafIndex, OAI.Ostmann.MovingSampleIndex, OAI.Ostmann.primes