OAI/NumberTheory/Ostmann/Arithmetic/FrozenSupportedArithmetic.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.bulkIndexPredicate line 9
2. theorem OAI.Ostmann.bulkIndexPredicate_eq_true line 12
3. theorem OAI.Ostmann.bulkIndexPredicate_eq_false line 16
4. def OAI.Ostmann.frozenBulkFrequencyFactor line 20
5. theorem OAI.Ostmann.frozenBulkFrequencyFactor_norm_le line 32
6. theorem OAI.Ostmann.movingSupportedArithmetic_bulk_residues line 52

   Source documentation

   The nonbulk coprimalities stay inside the fixed frequency factor. The only injectivity used here is the actual distinct-bulk event, removed later under its original product prior.

   theorem movingSupportedArithmetic_bulk_residues {σ I : Type*} [Fintype I]
       (base value : σ → ℕ) (n m : ℕ) (slot : (TreeLeafIndex n × Fin m) ↪ σ)
       (hv : ∀ i ∉ Set.range slot, value i = base i)
       (t : Bool → FrequencyTree ℤ n) (small : Bool → TreeLeafTuple (List σ) n)
       (samples : Bool → MovingSampleSlots σ n)
       (hvsmall : ∀ b, movingSlotValues value n (small b) = movingSlotValues base n (small b))
       (hvsamples : ∀ b, (samples b).values value = (samples b).values base)
       (e : Equiv.Perm (TreeLeafIndex n × Fin m))
       (T : Bool → MovingSlotData σ n)
       (hT : ∀ b, T b = buildMovingSlotData n (t b) (small b)
         (if b then bulkSlotLeaves n m (slot ∘ e.symm) else bulkSlotLeaves n m slot) (samples b))
       (F : Bool → {k : ℕ} → MovingSlotData σ k → ℤ → ℂ)
   …

   Mentions: OAI.Ostmann.TreeLeafIndex, OAI.Ostmann.FrequencyTree, OAI.Ostmann.TreeLeafTuple, OAI.Ostmann.MovingSampleSlots, OAI.Ostmann.movingSlotValues, OAI.Ostmann.MovingSlotData, OAI.Ostmann.buildMovingSlotData, OAI.Ostmann.bulkSlotLeaves