PairDensity.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Density of one tree split

Given the parent difference, a split coordinate produces the child ratio as a fixed unit times its inverse square. Each valid child pair therefore has multiplicity at most two. Zero weights at zero discard invalid nodes.

theorem OAI.Ostmann.pair_ratio_sum_eq line 20

Source documentation

A full-field sum in ratio coordinates is exactly the difference convolution.

theorem pair_ratio_sum_eq {p : ℕ} [Fact p.Prime]
    (d : (ZMod p)ˣ) (f g : ZMod p → ℝ) (hf : f 0 = 0) (hg : g 0 = 0) :
    (∑ t : (ZMod p)ˣ, if t = 1 then 0 else
      f ((d : ZMod p) * (t : ZMod p) / ((t : ZMod p) - 1)) *
        g ((d : ZMod p) / ((t : ZMod p) - 1))) =
      ∑ x : ZMod p, f x * g (x - d) := by
…

theorem OAI.Ostmann.pair_inverse_square_density line 57

Source documentation

Counting form of the conditional density bound at one internal node.

theorem pair_inverse_square_density {p : ℕ} [Fact p.Prime]
    (d K : (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)ˣ,
      let t := K * (m⁻¹) ^ 2
…