The power ledger in paper equation (5.71)

This file lifts the nodewise exponent identity already proved in SingleScaleSetup to the direct finite-product identity used in Step 1 of Proposition 5.10. The distinguished leaf is kept explicit.

def Anderson4D.branchesOffLeafPath {t : PlaneTree} (l₀ : HeppLeaf t) : Finset t.VPos

Branch nodes whose subtree does not contain the distinguished leaf.

Equations

• Anderson4D.branchesOffLeafPath l₀ = {v ∈ t.BranchNodes | ¬↑v <+: ↑↑l₀}

def Anderson4D.branchChildrenOffLeafPath {t : PlaneTree} (v : t.VPos) (l₀ : HeppLeaf t) : Finset t.VPos

A branch child is off the distinguished path exactly when its subtree does not contain the distinguished leaf.

Equations

• Anderson4D.branchChildrenOffLeafPath v l₀ = {c ∈ Anderson4D.branchChildren v | ¬↑c <+: ↑↑l₀}

def Anderson4D.branchesOffLeafPathRatioExponent {t : PlaneTree} (v : t.VPos) (l₀ : HeppLeaf t) : ℤ

Collected exponent of one branch scale in the last ratio product of paper (5.71).

Equations

• Anderson4D.branchesOffLeafPathRatioExponent v l₀ = ↑(Anderson4D.branchChildren v).card - ↑(Anderson4D.branchChildrenTowardLeaf v l₀).card - if ↑v <+: ↑↑l₀ then 0 else 1

theorem Anderson4D.branchesOffLeafPath_ratio_product {t : PlaneTree} (ht : t.isValid = true) (l₀ : HeppLeaf t) (N : t.VPos → ℝ) (hN : ∀ v ∈ t.BranchNodes, 0 < N v) : ∏ v ∈ branchesOffLeafPath l₀, N (PlaneTree.parentV v) / N v = ∏ p ∈ t.BranchNodes, N p ^ branchesOffLeafPathRatioExponent p l₀

The final ratio product in (5.71), regrouped as one integer power at every branch node.

theorem Anderson4D.paper571_rhs_product_eq_collected {t : PlaneTree} (ht : t.isValid = true) (hroot : t.rootV ∈ t.BranchNodes) (mu : t.Multiplicities) (compound : Finset t.VPos) (l₀ : HeppLeaf t) (N : t.VPos → ℝ) (hN : ∀ v ∈ t.BranchNodes, 0 < N v) : ((∏ l ∈ simpleLeaves t compound, N (PlaneTree.parentV l) ^ 2) * ∏ l ∈ compoundLeaves t compound, N (PlaneTree.parentV l) ^ ↑(mu.m l)) * N (PlaneTree.parentV ↑l₀) ^ (-1) * ∏ v ∈ branchesOffLeafPath l₀, N (PlaneTree.parentV v) / N v = ∏ v ∈ t.BranchNodes, N v ^ paper571RhsExponent mu compound l₀ v

The uncollected right side of (5.71) equals the product carrying the nodewise exponent paper571RhsExponent.

theorem Anderson4D.paper571_direct_product_identity {t : PlaneTree} (ht : t.isValid = true) (hroot : t.rootV ∈ t.BranchNodes) (mu : t.Multiplicities) (compound : Finset t.VPos) (l₀ : HeppLeaf t) (N : t.VPos → ℝ) (hN : ∀ v ∈ t.BranchNodes, 0 < N v) : ∏ v ∈ t.BranchNodes, N v ^ (↑(gamma2 mu compound v) - 1) = ((∏ l ∈ simpleLeaves t compound, N (PlaneTree.parentV l) ^ 2) * ∏ l ∈ compoundLeaves t compound, N (PlaneTree.parentV l) ^ ↑(mu.m l)) * N (PlaneTree.parentV ↑l₀) ^ (-1) * ∏ v ∈ branchesOffLeafPath l₀, N (PlaneTree.parentV v) / N v

Paper equation (5.71) in direct finite-product form.

theorem Anderson4D.paper572_branchPower_le_leafPower {t : PlaneTree} (ht : t.isValid = true) (hroot : t.rootV ∈ t.BranchNodes) (mu : t.Multiplicities) (compound : Finset t.VPos) (l₀ : HeppLeaf t) (N : t.VPos → ℝ) (hN : ∀ v ∈ t.BranchNodes, 0 < N v) (hmono : ∀ v ∈ t.BranchNodes, v ≠ t.rootV → N v ≤ N (PlaneTree.parentV v)) : ∏ v ∈ t.BranchNodes, N v ^ (-2 * (↑(gamma2 mu compound v) - 1)) ≤ ((∏ l ∈ simpleLeaves t compound, N (PlaneTree.parentV l) ^ (-4)) * ∏ l ∈ compoundLeaves t compound, N (PlaneTree.parentV l) ^ (-2 * ↑(mu.m l))) * N (PlaneTree.parentV ↑l₀) ^ 2

Paper (5.72)'s power inequality. Squaring the inverse of (5.71) leaves an extra negative square of the off-path parent ratios; it is at most one because branch scales increase toward the root.

theorem Anderson4D.singleScale_branchPower_le_leafPower {t : PlaneTree} (ht : t.isValid = true) (hroot : t.rootV ∈ t.BranchNodes) (Nm : t.HeppMarking) (mu : t.Multiplicities) (compound : Finset t.VPos) (l₀ : HeppLeaf t) : ∏ v ∈ t.BranchNodes, ↑(scaleN Nm v) ^ (-2 * (↑(gamma2 mu compound v) - 1)) ≤ ((∏ l ∈ simpleLeaves t compound, ↑(scaleN Nm (PlaneTree.parentV l)) ^ (-4)) * ∏ l ∈ compoundLeaves t compound, ↑(scaleN Nm (PlaneTree.parentV l)) ^ (-2 * ↑(mu.m l))) * ↑(scaleN Nm (PlaneTree.parentV ↑l₀)) ^ 2

Specialization of the (5.72) power ledger to the dyadic Hepp marking.

theorem Anderson4D.one_le_uniformPower_mul_parentScaleRatioCube {t : PlaneTree} (ht : t.isValid = true) (hroot : t.rootV ∈ t.BranchNodes) (Nm : t.HeppMarking) (mu : t.Multiplicities) (hscale : SatisfiesSingleScaleCondition Nm mu) : 1 ≤ (8 * Real.exp 4) ^ (3 * totalMultiplicity mu) * ∏ v ∈ nonrootBranches t, parentScaleRatio Nm v ^ 3

Quantitative form of the first reduction after (5.69): the missing cube of the parent-scale-ratio product can be inserted at exponential cost.