OAI/NumberTheory/Ostmann/Tree/RationalProfileLeaves.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Weighted horizontal-level averages with actual independent leaf products

  1. theorem OAI.Ostmann.rationalProfileLeafValue_fiber_sum line 11
  2. theorem OAI.Ostmann.rationalProfileLeafValue_mean_eq line 68
  3. theorem OAI.Ostmann.rationalProfileLeafValue_mean_le line 86

    Source documentation

    Horizontal-level domination for a different nonnegative test at each node.

    theorem rationalProfileLeafValue_mean_le {p : ℕ} [Fact p.Prime] (D : (ZMod p)ˣ)
    {n : ℕ} {C : (ZMod p)ˣ} (T : RationalTreeData (ZMod p)ˣ n C)
    (w : TreeLeafTuple (ZMod p → ℝ) n) (hw : treeWeightsNonneg n w)
    (XL XR : (ZMod p)ˣ) :
    (∑ x : TreeLeafTuple (ZMod p)ˣ n, rationalProfileLeafValue D T w XL XR x) /
      (Fintype.card (TreeLeafTuple (ZMod p)ˣ n) : ℝ) ≤
        (2 : ℝ) ^ (2 ^ n - 1) * treeProfileMean n w := by
…

    Mentions: OAI.Ostmann.RationalTreeData, OAI.Ostmann.TreeLeafTuple, OAI.Ostmann.treeWeightsNonneg, OAI.Ostmann.rationalProfileLeafValue, OAI.Ostmann.treeProfileMean