MovingPrimePatternArithmeticComparison.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Original-pattern arithmetic for two prime giant residues

theorem OAI.Ostmann.movingPrimePattern_arithmetic_comparison line 14

Source documentation

Remove the actual prime-square exclusions and replace the remaining simultaneous line probabilities by their symbolic flags under the original pattern law. No injectivity assumption is imposed on the sampling measure.

theorem movingPrimePattern_arithmetic_comparison {A B C : Type*}
    [Fintype A] [Nonempty A] [Fintype B] [Fintype C] {N n : ℕ}
    (e : Fin (N + 1) ≃ B ⊕ C) (prime : A → ℕ)
    (hpInj : Function.Injective prime) (hprime : ∀ a, (prime a).Prime)
    (tierB : B → ℕ) (tierC : C → ℕ) (t : Bool → FrequencyTree ℤ n)
    (small bulk : Bool → TreeLeafTuple (List B) n) (pattern : Bool × MovingSampleIndex n → C)
    (rep : ∀ c, {i : Bool × MovingSampleIndex n // pattern i = c})
    (hsmall : ∀ b, ∀ i ∈ flattenMovingSlots n (small b), n ≤ tierB i)
    (hbulk : ∀ b, ∀ i ∈ flattenMovingSlots n (bulk b), n ≤ tierB i)
    (htier : ∀ i, tierC (pattern i) = movingSampleTier i.2)
    (d : ℕ) (F U : ℝ) (hF : 1 ≤ F) (hU : 1 ≤ U)
    (hsize : ∀ b, (movingPatternFinData e n t small bulk pattern b).SizeLE d)
…

Mentions: OAI.Ostmann.FrequencyTree, OAI.Ostmann.TreeLeafTuple, OAI.Ostmann.MovingSampleIndex, OAI.Ostmann.flattenMovingSlots, OAI.Ostmann.movingSampleTier, OAI.Ostmann.movingPatternFinData