OAI/NumberTheory/Ostmann/Arithmetic/FrozenFrequencySupport.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.movingFrequencyPageAverage_nonbulk line 11
2. theorem OAI.Ostmann.movingFrequencyPageAverage_actual_nonbulk line 42

   Source documentation

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

   theorem movingFrequencyPageAverage_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