TreeCoordinates.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

Rational coordinates at a tree split

These identities are equations tree-difference-ratio, tree-held-square, and tree-p-square of the manuscript. Nonzero hypotheses state precisely that the reconstructed node is valid.

def OAI.Ostmann.reconstructedEntry line 19
def OAI.Ostmann.parentArgument line 22
def OAI.Ostmann.childArgument line 24
theorem OAI.Ostmann.reconstructedEntry_relation line 26
theorem OAI.Ostmann.tree_child_difference line 31
theorem OAI.Ostmann.tree_child_ratio line 40
theorem OAI.Ostmann.tree_reconstructed_square line 48
theorem OAI.Ostmann.tree_held_square line 58

theorem OAI.Ostmann.tree_product_ratio line 69

Source documentation

Exposing a child product makes its ratio an inverse square of the free product.

theorem tree_product_ratio {G : Type*} [CommGroup G]
    (sL sR XL XR CL CR P m : G) :
    (sL / sR) * ((XR * CR * (P / m)) / (XL * CL * m)) =
      ((sL / sR) * (XR * CR * P / (XL * CL))) * (m⁻¹) ^ 2 := by
…

theorem OAI.Ostmann.children_eq_pair_coordinates line 76

Source documentation

Difference and ratio identify the child arguments with the sampling coordinates.

theorem children_eq_pair_coordinates {K : Type*} [Field K]
    (x z d t : K) (hz : z ≠ 0) (hd : d ≠ 0)
    (hdiff : x - z = d) (hratio : x / z = t) :
    (x, z) = (d * t / (t - 1), d / (t - 1)) := by
…

theorem OAI.Ostmann.tree_children_eq_pair_coordinates line 85

Source documentation

The rational tree formulas produce exactly the pair used by the density model.

theorem tree_children_eq_pair_coordinates {K : Type*} [Field K]
    (s sL sR D u HL HR P : K)
    (hs : s ≠ 0) (hsR : sR ≠ 0) (hD : D ≠ 0) (hu : u ≠ 0)
    (hL : HL ≠ 0) (hR : HR ≠ 0) (hP : P ≠ 0)
    (hrel : P * (s * u) = sL * HR - sR * HL) :
    (childArgument sL D u HL P, childArgument sR D u HR P) =
      (parentArgument s D HL HR * ((sL / sR) * (HR / HL)) /
        ((sL / sR) * (HR / HL) - 1),
       parentArgument s D HL HR / ((sL / sR) * (HR / HL) - 1)) := by
…

Mentions: OAI.Ostmann.childArgument, OAI.Ostmann.parentArgument

theorem OAI.Ostmann.reconstructedEntry_zero_iff_ratio_one line 101

Source documentation

A reconstructed node is invalid precisely at the singular child ratio.

theorem reconstructedEntry_zero_iff_ratio_one {K : Type*} [Field K]
    (s sL sR u HL HR : K) (hs : s ≠ 0) (hsR : sR ≠ 0)
    (hu : u ≠ 0) (hL : HL ≠ 0) :
    reconstructedEntry s sL sR u HL HR = 0 ↔ (sL / sR) * (HR / HL) = 1 := by
…

Mentions: OAI.Ostmann.reconstructedEntry

theorem OAI.Ostmann.tree_parent_fixed_product line 112

Source documentation

At a fixed node product the root argument is independent of the free split.

theorem tree_parent_fixed_product {K : Type*} [Field K]
    (s D XL XR CL CR P m : K) (hm : m ≠ 0) :
    parentArgument s D (XL * CL * m) (XR * CR * (P / m)) =
      s / (D * XL * CL * XR * CR * P) := by
…

Mentions: OAI.Ostmann.parentArgument