OAI/NumberTheory/Ostmann/Arithmetic/MovingPatternRegularSupport.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.movingPatternRegularSlots line 12

   Source documentation

   The common top list, before its primes are drawn.

   noncomputable def movingPatternRegularSlots {B C : Type*} {N : ℕ} (e : Fin (N + 1) ≃ B ⊕ C)
       (n m : ℕ) (small : TreeLeafTuple (List B) n) (slot : (TreeLeafIndex n × Fin m) ↪ B) :
       List (Fin (N + 1)) :=
   …

   Mentions: OAI.Ostmann.TreeLeafTuple, OAI.Ostmann.TreeLeafIndex

2. theorem OAI.Ostmann.movingPatternRegularSlots_external line 18
3. theorem OAI.Ostmann.naturalProduct_eq_finprod line 30
4. theorem OAI.Ostmann.movingPatternFinBulkData_regular_perm line 38

   Source documentation

   The two history roots contain precisely the fixed regular slots.

   theorem movingPatternFinBulkData_regular_perm {B C : Type*} {N n m : ℕ}
       (e : Fin (N + 1) ≃ B ⊕ C) (t : Bool → FrequencyTree ℤ n)
       (small : TreeLeafTuple (List B) n) (slot : (TreeLeafIndex n × Fin m) ↪ B)
       (pattern : Bool × MovingSampleIndex n → C) (b : Bool) :
       (movingPatternFinBulkData e n m t (fun _ => small) slot (Equiv.refl _) pattern b).regularSlots.Perm
         (movingPatternRegularSlots e n m small slot) := by
   …

   Mentions: OAI.Ostmann.FrequencyTree, OAI.Ostmann.TreeLeafTuple, OAI.Ostmann.TreeLeafIndex, OAI.Ostmann.MovingSampleIndex, OAI.Ostmann.movingPatternFinBulkData, OAI.Ostmann.movingPatternRegularSlots

5. theorem OAI.Ostmann.movingPattern_regular_pairwise line 53

   Source documentation

   Distinctness of the canonical regular enumeration comes from the original support guard, so repeated independent draws need no extra assumption.

   theorem movingPattern_regular_pairwise {B C : Type*} {N n m : ℕ}
       (e : Fin (N + 1) ≃ B ⊕ C) (t : Bool → FrequencyTree ℤ n)
       (small : TreeLeafTuple (List B) n) (slot : (TreeLeafIndex n × Fin m) ↪ B)
       (pattern : Bool × MovingSampleIndex n → C) (value : Fin (N + 1) → ℕ)
       (outside : List ℕ) (b : Bool)
       (h : movingRegularOutsidePairwise value outside
         (movingPatternFinBulkData e n m t (fun _ => small) slot (Equiv.refl _) pattern b)) :
       Pairwise (fun i j : Fin (movingPatternRegularSlots e n m small slot).length =>
         (value ((movingPatternRegularSlots e n m small slot).get i)).Coprime
           (value ((movingPatternRegularSlots e n m small slot).get j))) := by
   …

   Mentions: OAI.Ostmann.FrequencyTree, OAI.Ostmann.TreeLeafTuple, OAI.Ostmann.TreeLeafIndex, OAI.Ostmann.MovingSampleIndex, OAI.Ostmann.movingRegularOutsidePairwise, OAI.Ostmann.movingPatternFinBulkData, OAI.Ostmann.movingPatternRegularSlots

6. theorem OAI.Ostmann.movingPattern_regular_arithmetic_coprime line 78

   Source documentation

   External regular primes are coprime to the separated internal/frequency block on the original prior support.

   theorem movingPattern_regular_arithmetic_coprime {A B C I : Type*}
       [Fintype C] [Fintype I] {N n m : ℕ}
       (e : Fin (N + 1) ≃ B ⊕ C) (prime : A → ℕ) (hprime : ∀ a, (prime a).Prime)
       (x : Fin (N + 1) → A) (r : ℕ) (p : I → ℕ) (hp : ∀ i, (p i).Prime)
       (small : TreeLeafTuple (List B) n) (slot : (TreeLeafIndex n × Fin m) ↪ B)
       (hr : ∀ i, r.Coprime (prime (x i)))
       (hcross : ∀ b c, prime (x (e.symm (.inl b))) ≠ prime (x (e.symm (.inr c))))
       (hspect : ∀ i j, prime (x j) ≠ p i) :
       (MovingSlotReversal.naturalProduct (fun i => prime (x i))
         (movingPatternRegularSlots e n m small slot)).Coprime
         (∏ b, movingArithmeticModuli r p (movingPatternInternalPrimes e prime x) Finset.univ b) := by
   …

   Mentions: OAI.Ostmann.TreeLeafTuple, OAI.Ostmann.TreeLeafIndex, OAI.Ostmann.MovingSlotReversal.naturalProduct, OAI.Ostmann.movingPatternRegularSlots, OAI.Ostmann.movingArithmeticModuli, OAI.Ostmann.movingPatternInternalPrimes

7. theorem OAI.Ostmann.movingPattern_regular_page_projection line 103

   Source documentation

   The same one-prime conductor deletion used in the priors removes any Page contribution from the original regular list.

   theorem movingPattern_regular_page_projection {A B C I : Type*}
       [Fintype C] [Fintype I] {N n m : ℕ}
       (e : Fin (N + 1) ≃ B ⊕ C) (prime : A → ℕ) (hprime : ∀ a, (prime a).Prime)
       (x : Fin (N + 1) → A) (p : I → ℕ) (hp : ∀ i, (p i).Prime)
       (small : TreeLeafTuple (List B) n) (slot : (TreeLeafIndex n × Fin m) ↪ B)
       (S : Finset ℤ) (V cutoff : ℕ) (t : FrequencyTree (S × S) n)
       (hS : ∀ s ∈ S, s ≠ 0 ∧ s.natAbs ≤ V) (hcut : V < cutoff)
       (hlarge : ∀ i, cutoff ≤ prime (x i)) (z : Option PrimitiveRealZero)
       (hdelete : ∀ a, z = some a → ∀ q,
         deletedConductorPrime a.modulus cutoff = some q → ∀ i, prime (x i) ≠ q)
       (hdeletep : ∀ a, z = some a → ∀ q,
         deletedConductorPrime a.modulus cutoff = some q → ∀ i, p i ≠ q) :
   …

   Mentions: OAI.Ostmann.TreeLeafTuple, OAI.Ostmann.TreeLeafIndex, OAI.Ostmann.FrequencyTree, OAI.Ostmann.PrimitiveRealZero, OAI.Ostmann.deletedConductorPrime