Regrouping skipped-branch sets after collapse

For fixed r and s, the map W ↦ liftWPrime r s W embeds the contracted non-root-branch powerset into the original one. Consequently the induction sum can be reindexed without a fibre-cardinality loss.

Injectivity

theorem Anderson4D.liftContractFinset_injective {t : PlaneTree} {p : PlaneTree.Pos} (hp : t.IsPos p) : Function.Injective (liftContractFinset hp)

Mapping a finite set along the retained-vertex embedding is injective.

theorem Anderson4D.liftWPrime_injective_of_subset {t : PlaneTree} (r : t.VPos) (s : ℕ) {W₁ W₂ : Finset (t.contractAt ↑r).VPos} (hW₁ : W₁ ⊆ nonrootBranches (t.contractAt ↑r)) (hW₂ : W₂ ⊆ nonrootBranches (t.contractAt ↑r)) (h : liftWPrime r s W₁ = liftWPrime r s W₂) : W₁ = W₂

On contracted non-root branch sets, W ↦ W' is injective. In the s = 1 case the inserted vertex r can be erased because it is absent from both lifted contracted sets.

theorem Anderson4D.liftWPrime_injOn_powerset {t : PlaneTree} (r : t.VPos) (s : ℕ) : Set.InjOn (liftWPrime r s) ↑(nonrootBranches (t.contractAt ↑r)).powerset

Set-theoretic injectivity on the contracted non-root powerset.

Landing in the original powerset

theorem Anderson4D.liftWPrime_mem_original_powerset {t : PlaneTree} (r : t.VPos) (hr : r ∈ nonrootBranches t) (s : ℕ) {W : Finset (t.contractAt ↑r).VPos} (hW : W ∈ (nonrootBranches (t.contractAt ↑r)).powerset) : liftWPrime r s W ∈ (nonrootBranches t).powerset

A contracted non-root branch subset maps to an original non-root branch subset.

theorem Anderson4D.image_liftWPrime_powerset_subset {t : PlaneTree} (r : t.VPos) (hr : r ∈ nonrootBranches t) (s : ℕ) : Finset.image (liftWPrime r s) (nonrootBranches (t.contractAt ↑r)).powerset ⊆ (nonrootBranches t).powerset

The image of the contracted powerset is contained in the original powerset.

Exact reindexing and the sum upper bound

theorem Anderson4D.sum_liftWPrime_eq_sum_image {t : PlaneTree} (r : t.VPos) (s : ℕ) (g : Finset t.VPos → ℝ) : ∑ W ∈ (nonrootBranches (t.contractAt ↑r)).powerset, g (liftWPrime r s W) = ∑ W' ∈ Finset.image (liftWPrime r s) (nonrootBranches (t.contractAt ↑r)).powerset, g W'

Exact reindexing onto the image; injectivity means there is no fibre multiplicity.

theorem Anderson4D.sum_contracted_powerset_le_sum_original_powerset {t : PlaneTree} (r : t.VPos) (hr : r ∈ nonrootBranches t) (s : ℕ) (f : Finset (t.contractAt ↑r).VPos → ℝ) (g : Finset t.VPos → ℝ) (hfg : ∀ W ∈ (nonrootBranches (t.contractAt ↑r)).powerset, f W ≤ g (liftWPrime r s W)) (hg : ∀ W' ∈ (nonrootBranches t).powerset, 0 ≤ g W') : ∑ W ∈ (nonrootBranches (t.contractAt ↑r)).powerset, f W ≤ ∑ W' ∈ (nonrootBranches t).powerset, g W'

Generic no-fibre-loss regrouping bound. Only the target summands need to be nonnegative in order to enlarge the image to the full original powerset; the source summands may be arbitrary.