Geometric summation along marked ancestor chains

Marks strictly increase toward the root and are powers of two. Consequently the ratios of a fixed branch scale to the scales of its strict ancestors form a subseries of 1/2 + 1/4 + …. This is the geometric input in paper (5.27), used to keep the six-step volume iteration exponentially bounded.

noncomputable def Anderson4D.strictBranchAncestors {t : PlaneTree} (v : t.VPos) : Finset t.VPos

Strict branching ancestors of v, represented by path prefixes.

Equations

• Anderson4D.strictBranchAncestors v = {a ∈ t.BranchNodes | ↑a <+: ↑v ∧ a ≠ v}

@[simp]

theorem Anderson4D.mem_strictBranchAncestors {t : PlaneTree} {v a : t.VPos} : a ∈ strictBranchAncestors v ↔ a ∈ t.BranchNodes ∧ ↑a <+: ↑v ∧ a ≠ v

def Anderson4D.ancestorGap {t : PlaneTree} (v a : t.VPos) : ℕ

Number of tree edges from an ancestor a down to v.

Equations

• Anderson4D.ancestorGap v a = List.length ↑v - List.length ↑a

theorem Anderson4D.ancestorGap_pos {t : PlaneTree} {v a : t.VPos} (ha : ↑a <+: ↑v) (hne : a ≠ v) : 0 < ancestorGap v a

theorem Anderson4D.marking_add_ancestorGap_le {t : PlaneTree} (ht : t.isValid = true) (Nm : t.HeppMarking) {a v : t.VPos} (hav : IsAncestor a v) (hv : v ∈ t.BranchNodes) : Nm.Nexp v + ancestorGap v a ≤ Nm.Nexp a

Along a valid marked tree, the exponent gain from a branch to any branching ancestor is at least their depth gap.

theorem Anderson4D.scaleN_mul_two_pow_ancestorGap_le {t : PlaneTree} (ht : t.isValid = true) (Nm : t.HeppMarking) {a v : t.VPos} (hav : IsAncestor a v) (hv : v ∈ t.BranchNodes) : scaleN Nm v * 2 ^ ancestorGap v a ≤ scaleN Nm a

Dyadic scale form of marking_add_ancestorGap_le.

theorem Anderson4D.scaleN_div_scaleN_le_half_pow_ancestorGap {t : PlaneTree} (ht : t.isValid = true) (Nm : t.HeppMarking) {a v : t.VPos} (hav : IsAncestor a v) (hv : v ∈ t.BranchNodes) : ↑(scaleN Nm v) / ↑(scaleN Nm a) ≤ (1 / 2) ^ ancestorGap v a

Each ancestor-scale ratio is bounded by the corresponding power of 1/2.

theorem Anderson4D.sum_scaleN_div_ancestor_le_one {t : PlaneTree} (ht : t.isValid = true) (Nm : t.HeppMarking) {v : t.VPos} (hv : v ∈ t.BranchNodes) : ∑ a ∈ strictBranchAncestors v, ↑(scaleN Nm v) / ↑(scaleN Nm a) ≤ 1

Paper (5.27), one-branch geometric chain. The sum of the ratio of one branch scale to all of its strict branching-ancestor scales is at most one.

theorem Anderson4D.sum_childCount_mul_ancestor_ratio_le {t : PlaneTree} (ht : t.isValid = true) (Nm : t.HeppMarking) : ∑ v ∈ t.BranchNodes, ↑(t.childCount ↑v) * ∑ a ∈ strictBranchAncestors v, ↑(scaleN Nm v) / ↑(scaleN Nm a) ≤ ∑ v ∈ t.BranchNodes, ↑(t.childCount ↑v)

Paper (5.27), reordered double-sum form. Weighting each branch by its number of children and then summing its scale ratio over all strict ancestors costs at most the sum of the child counts.