OAI/NumberTheory/Ostmann/ZeroDensity/RationalNodeDensity.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The density bound for an actual reconstructed node

The fixed parent product makes its argument independent of the split. The reconstructed entry vanishes exactly when the child ratio is one. Thus the inverse-square density estimate applies to the actual formulas, with the manuscript's invalid-node convention.

  1. def OAI.Ostmann.rationalNodeArgument line 19
  2. def OAI.Ostmann.rationalNodeRatioConstant line 23
  3. def OAI.Ostmann.rationalNodeValue line 27
  4. theorem OAI.Ostmann.rationalNodeValue_eq_ratio line 36
  5. theorem OAI.Ostmann.rationalNodeValue_sum_le line 86

    Source documentation

    Conditional counting density of one actual rational tree split.

    theorem rationalNodeValue_sum_le {p : ℕ} [Fact p.Prime]
    (s sL sR D u XL XR CL CR P : (ZMod p)ˣ)
    (f g : ZMod p → ℝ) (hf : f 0 = 0) (hg : g 0 = 0)
    (hfn : ∀ x, 0 ≤ f x) (hgn : ∀ x, 0 ≤ g x) :
    (∑ m : (ZMod p)ˣ, rationalNodeValue s sL sR D u XL XR CL CR P f g m) ≤
      2 * ∑ x : ZMod p, f x * g (x - rationalNodeArgument s D XL XR CL CR P) := by
…

    Mentions: OAI.Ostmann.rationalNodeValue, OAI.Ostmann.rationalNodeArgument