OAI/NumberTheory/Ostmann/Characters/TreeProfile.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Nonuniform nonnegative weights at a horizontal level of the tree

  1. def OAI.Ostmann.treeWeightsNonneg line 11
  2. def OAI.Ostmann.treeProfileMean line 15
  3. def OAI.Ostmann.treeProfileMajorant line 20
  4. theorem OAI.Ostmann.treeProfileMajorant_zero line 27
  5. theorem OAI.Ostmann.treeProfileMajorant_nonneg line 31
  6. theorem OAI.Ostmann.treeProfileMean_nonneg line 47
  7. theorem OAI.Ostmann.treeProfileMajorant_mean_le line 55

    Source documentation

    The density loss is two for every internal node, with a separate mean for each leaf.

    theorem treeProfileMajorant_mean_le {p : ℕ} [Fact p.Prime]
    (n : ℕ) (w : TreeLeafTuple (ZMod p → ℝ) n) (hw : treeWeightsNonneg n w) :
    (∑ d : (ZMod p)ˣ, treeProfileMajorant n w d) /
      (Fintype.card (ZMod p)ˣ : ℝ) ≤
        (2 : ℝ) ^ (2 ^ n - 1) * treeProfileMean n w := by
…

    Mentions: OAI.Ostmann.TreeLeafTuple, OAI.Ostmann.treeWeightsNonneg, OAI.Ostmann.treeProfileMajorant, OAI.Ostmann.treeProfileMean