OAI/NumberTheory/Ostmann/Arithmetic/MovingPatternArithmeticComparison.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.movingPatternLineProduct line 12
2. def OAI.Ostmann.movingPatternHaarProduct line 19
3. def OAI.Ostmann.movingPatternFlagProduct line 27
4. def OAI.Ostmann.movingOriginalPatternWeight line 40
5. theorem OAI.Ostmann.movingPattern_arithmetic_comparison line 51

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