Reverse single-scale power comparison

Equation (5.71) also gives the comparison in the direction needed by the final single-scale assembly. The price is the square of the off-path inverse parent-scale ratios. This file bounds that product by the uniform loss from (5.69), and packages the subsequent insertion of the full ratio cube.

noncomputable def Anderson4D.singleScaleBranchPower {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (compound : Finset t.VPos) : ℝ

The branch-scale power on the left of paper (5.72).

Equations

• Anderson4D.singleScaleBranchPower Nm mu compound = ∏ v ∈ t.BranchNodes, ↑(Anderson4D.scaleN Nm v) ^ (-2 * (↑(Anderson4D.gamma2 mu compound v) - 1))

noncomputable def Anderson4D.singleScaleLeafPower {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (compound : Finset t.VPos) (l₀ : HeppLeaf t) : ℝ

The leaf-scale power on the right of paper (5.72), including the distinguished-parent factor.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Anderson4D.offPathInverseRatioProduct {t : PlaneTree} (Nm : t.HeppMarking) (l₀ : HeppLeaf t) : ℝ

The residual product in (5.71), specialized to the dyadic marking.

Equations

• Anderson4D.offPathInverseRatioProduct Nm l₀ = ∏ v ∈ Anderson4D.branchesOffLeafPath l₀, Anderson4D.inverseParentScaleRatio Nm v

theorem Anderson4D.branchesOffLeafPath_subset_nonrootBranches {t : PlaneTree} (l₀ : HeppLeaf t) : branchesOffLeafPath l₀ ⊆ nonrootBranches t

Every off-path branch is a non-root branch.

theorem Anderson4D.one_le_inverseParentScaleRatio_of_mem_nonrootBranches {t : PlaneTree} (Nm : t.HeppMarking) {v : t.VPos} (hv : v ∈ nonrootBranches t) : 1 ≤ inverseParentScaleRatio Nm v

On a non-root branch, the inverse parent-scale ratio is at least one.

theorem Anderson4D.offPathInverseRatioProduct_le_fullProduct {t : PlaneTree} (Nm : t.HeppMarking) (l₀ : HeppLeaf t) : offPathInverseRatioProduct Nm l₀ ≤ ∏ v ∈ nonrootBranches t, inverseParentScaleRatio Nm v

The off-path inverse-ratio product is bounded by the product over all non-root branches.

theorem Anderson4D.offPathInverseRatioProduct_le_uniformPower {t : PlaneTree} (ht : t.isValid = true) (hroot : t.rootV ∈ t.BranchNodes) (Nm : t.HeppMarking) (mu : t.Multiplicities) (_compound : Finset t.VPos) (l₀ : HeppLeaf t) (hscale : SatisfiesSingleScaleCondition Nm mu) : offPathInverseRatioProduct Nm l₀ ≤ (8 * Real.exp 4) ^ totalMultiplicity mu

Uniform (8 exp 4)^m bound for the residual product in (5.71).

theorem Anderson4D.singleScale_leafPower_eq_branchPower_mul_offPathSquare {t : PlaneTree} (ht : t.isValid = true) (hroot : t.rootV ∈ t.BranchNodes) (Nm : t.HeppMarking) (mu : t.Multiplicities) (compound : Finset t.VPos) (l₀ : HeppLeaf t) : singleScaleLeafPower Nm mu compound l₀ = singleScaleBranchPower Nm mu compound * offPathInverseRatioProduct Nm l₀ ^ 2

Exact reverse form of (5.71): the leaf power is the branch power times the square of the residual off-path inverse-ratio product.

theorem Anderson4D.singleScale_leafPower_le_uniformPower_mul_branchPower {t : PlaneTree} (ht : t.isValid = true) (hroot : t.rootV ∈ t.BranchNodes) (Nm : t.HeppMarking) (mu : t.Multiplicities) (compound : Finset t.VPos) (l₀ : HeppLeaf t) (hscale : SatisfiesSingleScaleCondition Nm mu) : singleScaleLeafPower Nm mu compound l₀ ≤ (8 * Real.exp 4) ^ (2 * totalMultiplicity mu) * singleScaleBranchPower Nm mu compound

The closure direction needed after the copy elimination: leafPower ≤ (8 exp 4)^(2m) * branchPower.

theorem Anderson4D.singleScale_leafPower_le_uniformPower_mul_branchPower_mul_ratioCube {t : PlaneTree} (ht : t.isValid = true) (hroot : t.rootV ∈ t.BranchNodes) (Nm : t.HeppMarking) (mu : t.Multiplicities) (compound : Finset t.VPos) (l₀ : HeppLeaf t) (hscale : SatisfiesSingleScaleCondition Nm mu) : singleScaleLeafPower Nm mu compound l₀ ≤ (8 * Real.exp 4) ^ (5 * totalMultiplicity mu) * singleScaleBranchPower Nm mu compound * ∏ v ∈ nonrootBranches t, parentScaleRatio Nm v ^ 3

Consumable final form: after reversing (5.72), reinsert the full cube of parent-scale ratios at total cost (8 exp 4)^(5m).