OAI/NumberTheory/Ostmann/Arithmetic/ArithmeticFrequencyTree.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.pairedFrequencyKernel line 12
2. theorem OAI.Ostmann.pairedFrequencyKernel_sum_le line 18
3. def OAI.Ostmann.pairedFrequencyLeaf line 59
4. theorem OAI.Ostmann.pairedFrequencyLeaf_sum_le line 62
5. theorem OAI.Ostmann.arithmetic_frequency_tree_sum_le line 88

   Source documentation

   Root-first elimination leaves only the two histories' leaf frequencies. The exponent 2^n-1 is the exact number of internal nodes.

   theorem arithmetic_frequency_tree_sum_le (S : Finset ℤ) (N V : ℕ) (D : ℝ)
       (hD : 0 ≤ D) (hS : ∀ s ∈ S, s ≠ 0 ∧ s.natAbs ≤ N)
       (hdiv : ∀ v ∈ S, ∀ w ∈ S, ((v.natAbs.gcd w.natAbs).divisors.card : ℝ) ≤ D)
       (n : ℕ) :
       (∑ x : FrequencyTree (S × S) n,
         frequencyTreeWeight (pairedFrequencyKernel S D) (pairedFrequencyLeaf S V) n x) ≤
         (8 * D ^ 4 * (1 + Real.log N) ^ 3) ^ (2 ^ n - 1) * (2 * (V : ℝ)) ^ (2 * 2 ^ n) := by
   …

   Mentions: OAI.Ostmann.FrequencyTree, OAI.Ostmann.frequencyTreeWeight, OAI.Ostmann.pairedFrequencyKernel, OAI.Ostmann.pairedFrequencyLeaf