Documentation

Anderson4D.HeppTree.BranchExcess

Branch excess and the final geometric exponent bound #

For a valid Hepp tree, the sum of childCount - 1 over branching vertices is exactly leafCount - 1. Since a branching vertex has at least two children, its child count is at most twice this excess. Combined with the ancestor-scale geometric sum from ScaleGeometric, this proves the combinatorial part of paper equation (5.27).

source
def Anderson4D.PlaneTree.branchExcess :
PlaneTree → ℕ

Recursive sum of childCount - 1 over a tree.

Equations
Instances For
    source
    def Anderson4D.PlaneTree.branchExcessList :
    List PlaneTree → ℕ

    Forest companion of branchExcess.

    Equations
    Instances For
      source
      theorem Anderson4D.PlaneTree.branchExcess_add_one_eq_leafCount (t : PlaneTree) :
      t.isValid = true → t.branchExcess + 1 = t.leafCount

      Euler identity for a valid rooted tree, in subtraction-free form.

      source
      theorem Anderson4D.PlaneTree.branchExcessList_add_length_eq_leafCountList (cs : List PlaneTree) :
      isValidList cs = true → branchExcessList cs + cs.length = leafCountList cs

      Forest form of the Euler identity.

      source
      theorem Anderson4D.PlaneTree.branchExcess_eq_leafCount_sub_one (t : PlaneTree) (ht : t.isValid = true) :
      t.branchExcess = t.leafCount - 1

      The subtraction form of the valid-tree Euler identity.

      source
      theorem Anderson4D.PlaneTree.sum_childCount_sub_one_eq_branchExcess (t : PlaneTree) :
      ∑ v : t.VPos, (t.childCount ↑v - 1) = t.branchExcess

      The recursive excess is the sum of childCount - 1 over all vertices.

      source
      theorem Anderson4D.PlaneTree.sum_childCount_sub_one_sigma_eq_branchExcessList (cs : List PlaneTree) :
      ∑ x : (i : Fin cs.length) × (cs.get i).VPos, ((cs.get x.fst).childCount ↑x.snd - 1) = branchExcessList cs

      Forest companion of sum_childCount_sub_one_eq_branchExcess.

      source
      theorem Anderson4D.PlaneTree.sum_branchNodes_childCount_sub_one_eq_branchExcess (t : PlaneTree) :
      ∑ v ∈ t.BranchNodes, (t.childCount ↑v - 1) = t.branchExcess

      Non-branching vertices contribute zero to the excess sum.

      source
      theorem Anderson4D.PlaneTree.sum_branchNodes_childCount_le_two_mul_excess (t : PlaneTree) :
      ∑ v ∈ t.BranchNodes, t.childCount ↑v ≤ 2 * t.branchExcess

      In a valid tree, the sum of branch child counts is at most twice the total branch excess.

      source
      theorem Anderson4D.PlaneTree.sum_branchNodes_childCount_le_two_mul_leafCount_sub_one (t : PlaneTree) (ht : t.isValid = true) :
      ∑ v ∈ t.BranchNodes, t.childCount ↑v ≤ 2 * (t.leafCount - 1)

      Valid-tree form of the branching-count estimate in paper (5.27).

      source
      theorem Anderson4D.PlaneTree.sum_childCount_mul_ancestor_ratio_le_two_mul_leafCount (t : PlaneTree) (ht : t.isValid = true) (Nm : t.HeppMarking) :
      ∑ v ∈ t.BranchNodes, ↑(t.childCount ↑v) * ∑ u ∈ strictBranchAncestors v, ↑(scaleN Nm v) / ↑(scaleN Nm u) ≤ 2 * ↑t.leafCount

      Paper (5.27): after reordering by the lower branch vertex, the ancestor scale ratios cost at most 2 * leafCount in total.