Product of the two analytic collapse calls

This file combines Proposition 5.10 on the restricted subtree with the Proposition 5.9 induction hypothesis on the contracted tree. The contracted right-hand side is expanded into its W-sum, so each summand is exactly combinedCollapseTerm.

The combined analytic estimate

theorem Anderson4D.collapse_analytic_product_le_sum_combinedCollapseTerm {C0 D : ℝ} (hsingle : SingleScaleEstimate C0) {t : PlaneTree} (ht : t.isValid = true) (hroot : t.rootV ∈ t.BranchNodes) (Nm : t.HeppMarking) (mu : t.Multiplicities) (compound : Finset t.VPos) (hcompound : compound ⊆ t.Leaves) (z : HeppLeaf t → Fin 4 → ℤ) (hsep : IsSeparatedEmbedding Nm z) (hdiam : SatisfiesSubtreeDiameter Nm mu z) {r : t.VPos} (hr : IsLowestCollapseEligible Nm mu r) (lstar : InsideLeaf r) (d : RawCollapseData (InsideLeaf r) (OutsideLeaf r)) (hSpec : CollapseMultiplicitySpec (splitLeafMultiplicity mu r) d) (hblocks : 2 ≤ d.blocks.length) (hIH : InductiveConclusion C0 D (t.contractAt ↑r)) : 4 ^ d.insideLength * (↑(collapseCutCount d + 1).factorial)⁻¹ * paperSum (leafMultiplicity (restrictMultiplicities mu r)) (singleScaleChainWeight (restrictEmbedding z r) d.adjacentCutIndices) * paperSum (leafMultiplicity (contractMultiplicities mu r (collapseCutCount d) ⋯)) (primitiveSeparatedChainWeight (contractEmbedding z r lstar)) ≤ ∑ W ∈ (nonrootBranches (t.contractAt ↑r)).powerset, combinedCollapseTerm C0 D d.insideLength (collapseCutCount d) d.collapsed.length Nm mu compound r ⋯ W

The two analytic calls in the eligible-collapse step, multiplied and expanded into the contracted-tree W-sum.