OAI/NumberTheory/Ostmann/Arithmetic/MovingPatternLineComparison.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.movingPattern_line_comparison line 14

   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 movingPattern_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