MovingPrimePatternLineComparison.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Original-pattern arithmetic for two prime giant residues

theorem OAI.Ostmann.movingPrimePattern_line_comparison line 17

Source documentation

Apply the proved comparison to the actual pattern tree and its original external priors. All occurrence rows and unique representatives are derived from that constructor. The loss involves internal classes, not bulk size.

theorem movingPrimePattern_line_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