BulkCollisionSupport.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The original arithmetic support forces distinct bulk primes

theorem OAI.Ostmann.prime_list_injective_of_pairwise line 11
theorem OAI.Ostmann.buildMovingSlotData_injective_of_support line 23

theorem OAI.Ostmann.movingFrequencyPageAverage_zero_of_bulk_collision line 52

Source documentation

The frequency factor vanishes on collisions before any averaging or resampling is performed.

theorem movingFrequencyPageAverage_zero_of_bulk_collision {σ : Type*}
    (value : σ → ℕ) (n m : ℕ) (slot : (TreeLeafIndex n × Fin m) ↪ σ)
    (t : FrequencyTree ℤ n) (small : TreeLeafTuple (List σ) n)
    (samples : MovingSampleSlots σ n) (outside : List ℕ)
    (hprime : ∀ i, (value i).Prime) (hbad : ¬Function.Injective (value ∘ slot))
    (F : Bool → {k : ℕ} → MovingSlotData σ k → ℤ → ℂ)
    (E : Bool → {k : ℕ} → MovingSlotData σ k → ℤ → ℤ → ℤ → ℝ)
    (T : Bool → MovingSlotData σ n)
    (hT : T false = buildMovingSlotData n t small (bulkSlotLeaves n m slot) samples)
    (nodes : Bool → List MovingFormulaNode) (R : ℤ)
    (r : ℕ) [NeZero r] (input : PublishedProgressionInput) (Q : ℕ) (y : ℝ) :
    movingFrequencyPageAverage value outside F E T nodes R r input Q y = 0 := by
…

Mentions: OAI.Ostmann.TreeLeafIndex, OAI.Ostmann.FrequencyTree, OAI.Ostmann.TreeLeafTuple, OAI.Ostmann.MovingSampleSlots, OAI.Ostmann.MovingSlotData, OAI.Ostmann.buildMovingSlotData, OAI.Ostmann.bulkSlotLeaves, OAI.Ostmann.MovingFormulaNode, OAI.Ostmann.PublishedProgressionInput, OAI.Ostmann.movingFrequencyPageAverage

theorem OAI.Ostmann.movingFrequencyPageAverage_collision_gate line 76

Source documentation

Inserting the distinctness gate leaves the literal supported arithmetic coefficient unchanged.

theorem movingFrequencyPageAverage_collision_gate {σ : Type*}
    (value : σ → ℕ) (n m : ℕ) (slot : (TreeLeafIndex n × Fin m) ↪ σ)
    (t : FrequencyTree ℤ n) (small : TreeLeafTuple (List σ) n)
    (samples : MovingSampleSlots σ n) (outside : List ℕ)
    (hprime : ∀ i, (value i).Prime)
    (F : Bool → {k : ℕ} → MovingSlotData σ k → ℤ → ℂ)
    (E : Bool → {k : ℕ} → MovingSlotData σ k → ℤ → ℤ → ℤ → ℝ)
    (T : Bool → MovingSlotData σ n)
    (hT : T false = buildMovingSlotData n t small (bulkSlotLeaves n m slot) samples)
    (nodes : Bool → List MovingFormulaNode) (R : ℤ)
    (r : ℕ) [NeZero r] (input : PublishedProgressionInput) (Q : ℕ) (y : ℝ) (A : ℂ) :
    movingFrequencyPageAverage value outside F E T nodes R r input Q y * A =
…