OAI/NumberTheory/Ostmann/Arithmetic/FrequencyTreeSum.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.FrequencyTree line 14
2. instance OAI.Ostmann.frequencyTreeFintype line 18
3. def OAI.Ostmann.frequencyRoot line 24
4. def OAI.Ostmann.frequencyTreeWeight line 28
5. theorem OAI.Ostmann.frequencyTreeWeight_nonneg line 34
6. theorem OAI.Ostmann.frequencyTree_sum_le line 43

   Source documentation

   Each pair of parent frequencies is summed before either child pair. Only the leaf mass remains after all internal frequencies are eliminated.

   theorem frequencyTree_sum_le {A : Type} [Fintype A]
       (K : A → A → A → ℝ) (W : A → ℝ) (C : ℝ)
       (hK : ∀ a b c, 0 ≤ K a b c) (hW : ∀ a, 0 ≤ W a) (hC : 0 ≤ C)
       (hsum : ∀ b c, ∑ a : A, K a b c ≤ C) (n : ℕ) :
       (∑ x : FrequencyTree A n, frequencyTreeWeight K W n x) ≤
         C ^ (2 ^ n - 1) * (∑ a : A, W a) ^ (2 ^ n) := by
   …

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