OAI/NumberTheory/Ostmann/Arithmetic/MovingPrimeBulkSupport.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.movingFrequencyCorePrimeAverage_bulk_residues line 11
2. theorem OAI.Ostmann.movingFrequencyPrimeAverage_nonbulk line 32
3. theorem OAI.Ostmann.movingFrequencyPrimeAverage_actual_nonbulk line 63

   Source documentation

   For the literal formula-node list, the remaining frequency-size tests depend on the frequency tree alone.

   theorem movingFrequencyPrimeAverage_actual_nonbulk {σ : Type*}
       (value base : σ → ℕ) (bulk : σ → Bool) (outside : List ℕ)
       (hv : ∀ i, bulk i = false → value i = base i)
       (hvalue : ∀ i, value i ≠ 0) (childBound pivotBound : ℕ → ℕ)
       (F : Bool → {n : ℕ} → MovingSlotData σ n → ℤ → ℂ)
       (E : Bool → {n : ℕ} → MovingSlotData σ n → ℤ → ℤ → ℤ → ℝ)
       {n : ℕ} (T : Bool → MovingSlotData σ n) (hf : ∀ b, (T b).Frequencies (· ≠ 0))
       (hprime : ∀ b, ∀ L ∈ (T b).regularLists, ∀ i ∈ L, (value i).Prime)
       (hnodup : ∀ b, ∀ L ∈ (T b).regularLists, (L.filter bulk).Nodup)
       (hinj : ∀ i j, bulk i = true → bulk j = true → value i = value j → i = j)
       (hcross : ∀ b, ∀ L ∈ (T b).regularLists, ∀ i ∈ L, ∀ j ∈ L,
         bulk i ≠ bulk j → value i ≠ value j)
   …

   Mentions: OAI.Ostmann.MovingSlotData

4. theorem OAI.Ostmann.movingPrimeCoreSpectator_bulk_residues line 97
5. theorem OAI.Ostmann.movingSupportedPrimeArithmetic_bulk_residues line 143
6. theorem OAI.Ostmann.movingFrequencyPrimeAverage_zero_of_bulk_collision line 198
7. theorem OAI.Ostmann.movingFrequencyPrimeAverage_collision_gate line 222

   Source documentation

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

   theorem movingFrequencyPrimeAverage_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 : ℕ) (xg y : ℝ) (A : ℂ) :
       movingFrequencyPrimeAverage value outside F E T nodes R r input Q xg y * A =
   …

   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.movingFrequencyPrimeAverage