Outer dyadic summation in the single-scale estimate

This file formalizes the finite combinatorial ledger used in Step 3 of the proof of Proposition 5.10, equations (5.76)--(5.86): the simple/compound majority partition and estimates (5.83)--(5.85), followed by the ordering and absorption argument in (5.86).

The companion SingleScaleSequence module supplies the P-sequence gain (5.77), including the at-most-99 skipped positions; the assembly modules combine it with the declarations below for the actual copy permutations.

The first sections record the exact conditional class-word count (5.79) and the multinomial factorizations behind (5.80)--(5.82). The subsequent sections specialize them to the (N,X) → (N,Y) → P classification constructed in SingleScaleSetup.

A generic two-level multinomial identity

theorem Anderson4D.multinomial_fiberwise {ι : Type u_1} {κ : Type u_2} [DecidableEq ι] [DecidableEq κ] (s : Finset ι) (t : Finset κ) (g : ι → κ) (f : ι → ℕ) (hmap : ∀ i ∈ s, g i ∈ t) : Nat.multinomial s f = (Nat.multinomial t fun (j : κ) => ∑ i ∈ s with g i = j, f i) * ∏ j ∈ t, Nat.multinomial ({i ∈ s | g i = j}) f

Exact multinomial factorization through finite fibers.

This is the algebraic identity used twice below: first to group (N,X) classes by (N,Y), and later to group (N,Y) classes by their common maximal scale X*. Empty fibers cause no problem, since their multinomial coefficient is one.

theorem Anderson4D.multinomial_subtype_eq {ι : Type u_1} [DecidableEq ι] (s : Finset ι) (f : ι → ℕ) : (Nat.multinomial Finset.univ fun (i : ↥s) => f ↑i) = Nat.multinomial s f

Replacing a finite carrier by its subtype does not change its multinomial coefficient.

Counting fine words over a fixed coarse word

theorem Anderson4D.card_validWords_eq_multinomial {ι : Type u_1} [Fintype ι] [DecidableEq ι] {M : ℕ} (mult : ι → ℕ) (hM : ∑ i : ι, mult i = M) : (validWords mult).card = Nat.multinomial Finset.univ mult

The number of admissible words with multiplicity function mult is the corresponding multinomial coefficient. This is the finite word-count bridge needed before applying the fiberwise identities above.

def Anderson4D.validRefinements {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] [DecidableEq ι] [DecidableEq κ] {M : ℕ} (mult : ι → ℕ) (g : ι → κ) (y : Fin M → κ) : Finset (Fin M → ι)

Fine words with prescribed multiplicities which refine a fixed coarse word through g.

Equations

• Anderson4D.validRefinements mult g y = {x ∈ Anderson4D.validWords mult | ∀ (j : Fin M), g (x j) = y j}

theorem Anderson4D.card_validRefinements {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] [DecidableEq ι] [DecidableEq κ] {M : ℕ} (mult : ι → ℕ) (g : ι → κ) (y : Fin M → κ) (hmass : ∀ (b : κ), ∑ a : { i : ι // g i = b }, mult ↑a = Fintype.card { j : Fin M // y j = b }) : (validRefinements mult g y).card = ∏ b : κ, Nat.multinomial Finset.univ fun (a : { i : ι // g i = b }) => mult ↑a

Conditional word count through a finite coarse map.

If the fixed coarse word y uses each coarse letter b exactly as often as the total fine multiplicity above b, then the number of admissible fine words refining y is the product of the fiber multinomial coefficients. This is the abstract counting statement behind paper (5.79).

A finite dyadic-window lemma

theorem Anderson4D.card_le_three_of_pow_two_pairwise_lt_eight {ι : Type u_1} [DecidableEq ι] (s : Finset ι) (x e : ι → ℕ) (hpow : ∀ a ∈ s, x a = 2 ^ e a) (hinj : Set.InjOn e ↑s) (hclose : ∀ a ∈ s, ∀ b ∈ s, x a < 8 * x b) : s.card ≤ 3

At most three distinct powers of two can be pairwise within a strict factor 8. This is the finite cardinality fact used to turn m_{N,X} ∼ XY into the lacunarity required by Lemma 5.12.

theorem Anderson4D.card_le_four_of_pow_two_pairwise_lt_sixteen {ι : Type u_1} [DecidableEq ι] (s : Finset ι) (x e : ι → ℕ) (hpow : ∀ a ∈ s, x a = 2 ^ e a) (hinj : Set.InjOn e ↑s) (hclose : ∀ a ∈ s, ∀ b ∈ s, x a < 16 * x b) : s.card ≤ 4

Four-point version used after grouping the (N,Y) classes by X*.

theorem Anderson4D.lacunary_subtype {ι : Type u_1} [DecidableEq ι] {K : ℕ} (s : Finset ι) (f : ι → ℕ) (h : Lacunary K s f) : Lacunary K Finset.univ fun (a : ↥s) => f ↑a

Passing from a finset to its subtype carrier preserves Lacunary.

theorem Anderson4D.multinomial_le_pow_of_lacunary_finset (K : ℕ) (hK : 1 ≤ K) : ∃ (C : ℝ), 1 ≤ C ∧ ∀ {ι : Type u_1} [DecidableEq ι] (s : Finset ι) (f : ι → ℕ), Lacunary K s f → ↑(Nat.multinomial s f) ≤ C ^ ∑ i ∈ s, f i

Finset-indexed form of Lemma 5.12 (5.51).

BinomialBounds states the result for tuples on Fin r; this wrapper reindexes an arbitrary finite carrier without changing either the multinomial coefficient or its total mass.

The fixed-P carriers

def Anderson4D.activeNXToP {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) : ActiveNXClass Nm mu → ActivePClass Nm mu

The active class map (N,X) ↦ P = YN⁴.

Equations

• Anderson4D.activeNXToP Nm mu a = ⟨Anderson4D.singleScaleSigma3 (Anderson4D.singleScaleSigma2 Nm mu ↑a), ⋯⟩

def Anderson4D.activeNXMultiplicity {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) : ActiveNXClass Nm mu → ℕ

Multiplicity of an active (N,X) class.

Equations

• Anderson4D.activeNXMultiplicity Nm mu a = Anderson4D.multiplicityNX Nm mu ↑a

def Anderson4D.activePMultiplicity {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) : ActivePClass Nm mu → ℕ

Multiplicity of an active P class.

Equations

• Anderson4D.activePMultiplicity Nm mu P = Anderson4D.multiplicityP Nm mu ↑P

def Anderson4D.nxAtP {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (P : ℕ) : Finset NXClass

Active (N,X) classes whose image under σ₃ ∘ σ₂ is P.

Equations

• Anderson4D.nxAtP Nm mu P = {a ∈ Anderson4D.nxCarrier Nm mu | Anderson4D.singleScaleSigma3 (Anderson4D.singleScaleSigma2 Nm mu a) = P}

def Anderson4D.nxToNY {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) : NXClass → NYClass

The class map (N,X) ↦ (N,Y) used inside a fixed P fiber.

Equations

• Anderson4D.nxToNY Nm mu = Anderson4D.singleScaleSigma2 Nm mu

theorem Anderson4D.nxAtP_mapsTo_nyAtP {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (P : ℕ) {a : NXClass} (ha : a ∈ nxAtP Nm mu P) : nxToNY Nm mu a ∈ nyAtP Nm mu P

theorem Anderson4D.nxAtP_fiber_eq_nxAtNY {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (P : ℕ) {q : NYClass} (hq : q ∈ nyAtP Nm mu P) : {a ∈ nxAtP Nm mu P | nxToNY Nm mu a = q} = nxAtNY Nm mu q

theorem Anderson4D.nxAtP_fiber_mass {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (P : ℕ) {q : NYClass} (hq : q ∈ nyAtP Nm mu P) : ∑ a ∈ nxAtP Nm mu P with nxToNY Nm mu a = q, multiplicityNX Nm mu a = multiplicityNY Nm mu q

theorem Anderson4D.multiplicityP_eq_sum_NX {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (P : ℕ) : multiplicityP Nm mu P = ∑ a ∈ nxAtP Nm mu P, multiplicityNX Nm mu a

The total multiplicity in a fixed P fiber can be summed directly over its (N,X) classes.

noncomputable def Anderson4D.activeNXFiberEquiv {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (P : ActivePClass Nm mu) : { a : ActiveNXClass Nm mu // activeNXToP Nm mu a = P } ≃ ↥(nxAtP Nm mu ↑P)

Equations

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

@[simp]

theorem Anderson4D.activeNXFiberEquiv_val {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (P : ActivePClass Nm mu) (a : { a : ActiveNXClass Nm mu // activeNXToP Nm mu a = P }) : ↑((activeNXFiberEquiv Nm mu P) a) = ↑↑a

theorem Anderson4D.activeNX_fiber_mass {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (P : ActivePClass Nm mu) : ∑ a : { a : ActiveNXClass Nm mu // activeNXToP Nm mu a = P }, activeNXMultiplicity Nm mu ↑a = activePMultiplicity Nm mu P

theorem Anderson4D.activeNX_fiber_multinomial {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (P : ActivePClass Nm mu) : (Nat.multinomial Finset.univ fun (a : { a : ActiveNXClass Nm mu // activeNXToP Nm mu a = P }) => activeNXMultiplicity Nm mu ↑a) = Nat.multinomial (nxAtP Nm mu ↑P) (multiplicityNX Nm mu)

theorem Anderson4D.paper579_conditional_classWord_count {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (y : Fin (totalMultiplicity mu) → ActivePClass Nm mu) (hy : y ∈ validWords (activePMultiplicity Nm mu)) : (validRefinements (activeNXMultiplicity Nm mu) (activeNXToP Nm mu) y).card = ∏ P ∈ pCarrier Nm mu, Nat.multinomial (nxAtP Nm mu P) (multiplicityNX Nm mu)

Paper (5.79), in the word representation used by this project.

For a fixed valid P-word, the admissible (N,X) class words refining it are counted by the product, over active P, of the multinomial coefficients of the (N,X) multiplicities in that fiber.

theorem Anderson4D.fixedP_multinomial_decomposition {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (P : ℕ) : Nat.multinomial (nxAtP Nm mu P) (multiplicityNX Nm mu) = Nat.multinomial (nyAtP Nm mu P) (multiplicityNY Nm mu) * ∏ q ∈ nyAtP Nm mu P, Nat.multinomial (nxAtNY Nm mu q) (multiplicityNX Nm mu)

Exact two-level decomposition used in the reduction (5.80) to (5.81):

multinomial((m_{N,X})_{P}) equals the multinomial of the (N,Y) masses times the product of the within-(N,Y) multinomials.

Lacunarity inside one (N,Y) class

theorem Anderson4D.nyClass_Y_pos {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) {q : NYClass} (hq : q ∈ nyCarrier Nm mu) : 0 < q.2

theorem Anderson4D.multiplicityNX_lacunary {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) {q : NYClass} (hq : q ∈ nyCarrier Nm mu) : Lacunary 3 (nxAtNY Nm mu q) (multiplicityNX Nm mu)

The family (m_{N,X})_X in a fixed (N,Y) class is 3-lacunary.

Indeed, XY ≤ m_{N,X} < 4XY; if two such masses lie in the same window [Z,2Z), their dyadic X values differ by a strict factor less than 8. Hence at most three distinct powers of two occur.

The second lacunary grouping in (5.86)

def Anderson4D.nyAtPX {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (P X : ℕ) : Finset NYClass

Fixed-P (N,Y) classes with a prescribed maximal multiplicity scale X*. These are the paper's blocks B(i).

Equations

• Anderson4D.nyAtPX Nm mu P X = {q ∈ Anderson4D.nyAtP Nm mu P | Anderson4D.maxXAtNY Nm mu q = X}

theorem Anderson4D.nyAtPX_active {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) {P X : ℕ} {q : NYClass} (hq : q ∈ nyAtPX Nm mu P X) : q ∈ nyCarrier Nm mu

theorem Anderson4D.nyAtPX_P {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) {P X : ℕ} {q : NYClass} (hq : q ∈ nyAtPX Nm mu P X) : singleScaleSigma3 q = P

theorem Anderson4D.nyAtPX_maxX {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) {P X : ℕ} {q : NYClass} (hq : q ∈ nyAtPX Nm mu P X) : maxXAtNY Nm mu q = X

theorem Anderson4D.nyClass_second_eq_pow_log {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) {q : NYClass} (hq : q ∈ nyCarrier Nm mu) : q.2 = 2 ^ Nat.log 2 q.2

theorem Anderson4D.one_le_maxXAtNY {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) {q : NYClass} (hq : q ∈ nyCarrier Nm mu) : 1 ≤ maxXAtNY Nm mu q

theorem Anderson4D.multiplicityNY_lacunary_fixed_P_X {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (P X : ℕ) : Lacunary 4 (nyAtPX Nm mu P X) (multiplicityNY Nm mu)

For fixed P and fixed X*, the masses m_{N,Y} are 4-lacunary.

The bounds X*Y ≤ m_{N,Y} ≤ 8X*Y put all Y values in one mass window within a strict factor 16. At fixed P = YN⁴, distinct classes have distinct dyadic Y, so there can be at most four.

def Anderson4D.xStarCarrierAtP {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (P : ℕ) : Finset ℕ

The active X* values among (N,Y) classes at fixed P.

Equations

• Anderson4D.xStarCarrierAtP Nm mu P = Finset.image (fun (q : Anderson4D.NYClass) => Anderson4D.maxXAtNY Nm mu q) (Anderson4D.nyAtP Nm mu P)

def Anderson4D.multiplicityPX {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (P X : ℕ) : ℕ

Paper's q(i): total (N,Y) mass in a fixed X* block.

Equations

• Anderson4D.multiplicityPX Nm mu P X = ∑ q ∈ Anderson4D.nyAtPX Nm mu P X, Anderson4D.multiplicityNY Nm mu q

def Anderson4D.yMassPX {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (P X : ℕ) : ℕ

Paper's W(i): the sum of the dyadic Y values in one X* block.

Equations

• Anderson4D.yMassPX Nm mu P X = ∑ q ∈ Anderson4D.nyAtPX Nm mu P X, q.2

theorem Anderson4D.nyAtP_mapsTo_xStarCarrier {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (P : ℕ) {q : NYClass} (hq : q ∈ nyAtP Nm mu P) : maxXAtNY Nm mu q ∈ xStarCarrierAtP Nm mu P

theorem Anderson4D.multiplicityP_eq_sum_PX {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (P : ℕ) : multiplicityP Nm mu P = ∑ X ∈ xStarCarrierAtP Nm mu P, multiplicityPX Nm mu P X

theorem Anderson4D.xStarCarrier_dyadic {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) {P X : ℕ} (hX : X ∈ xStarCarrierAtP Nm mu P) : IsDyadicNat X

theorem Anderson4D.xStarCarrier_pos {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) {P X : ℕ} (hX : X ∈ xStarCarrierAtP Nm mu P) : 0 < X

theorem Anderson4D.multiplicityPX_bounds {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (P X : ℕ) : X * yMassPX Nm mu P X ≤ multiplicityPX Nm mu P X ∧ multiplicityPX Nm mu P X ≤ 8 * X * yMassPX Nm mu P X

The comparison q(i) ∼ Z(i)W(i) used immediately below (5.86), with explicit constants 1 and 8.

theorem Anderson4D.fixedP_NY_multinomial_decomposition {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (P : ℕ) : Nat.multinomial (nyAtP Nm mu P) (multiplicityNY Nm mu) = Nat.multinomial (xStarCarrierAtP Nm mu P) (multiplicityPX Nm mu P) * ∏ X ∈ xStarCarrierAtP Nm mu P, Nat.multinomial (nyAtPX Nm mu P X) (multiplicityNY Nm mu)

Exact block decomposition at the start of (5.86), grouping equal X* values and writing their masses as q(i).

theorem Anderson4D.withinPX_multinomial_le : ∃ (C : ℝ), 1 ≤ C ∧ ∀ {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (P X : ℕ), ↑(Nat.multinomial (nyAtPX Nm mu P X) (multiplicityNY Nm mu)) ≤ C ^ multiplicityPX Nm mu P X

Lemma 5.12 applied inside every fixed-X* block B(i).

theorem Anderson4D.withinPX_multinomial_product_le : ∃ (C : ℝ), 1 ≤ C ∧ ∀ {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (P : ℕ), ↑(∏ X ∈ xStarCarrierAtP Nm mu P, Nat.multinomial (nyAtPX Nm mu P X) (multiplicityNY Nm mu)) ≤ C ^ multiplicityP Nm mu P

theorem Anderson4D.fixedP_NY_multinomial_le_XStar : ∃ (C : ℝ), 1 ≤ C ∧ ∀ {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (P : ℕ), ↑(Nat.multinomial (nyAtP Nm mu P) (multiplicityNY Nm mu)) ≤ C ^ multiplicityP Nm mu P * ↑(Nat.multinomial (xStarCarrierAtP Nm mu P) (multiplicityPX Nm mu P))

First reduction in (5.86): after the lacunary estimates inside the blocks B(i), only the multinomial of the block masses q(i) remains.

theorem Anderson4D.withinNY_multinomial_le : ∃ (C : ℝ), 1 ≤ C ∧ ∀ {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) {q : NYClass}, q ∈ nyCarrier Nm mu → ↑(Nat.multinomial (nxAtNY Nm mu q) (multiplicityNX Nm mu)) ≤ C ^ multiplicityNY Nm mu q

The within-(N,Y) multinomial in (5.80) is exponentially bounded in m_{N,Y}. This is the precise application of Lemma 5.12 justified by multiplicityNX_lacunary.

theorem Anderson4D.withinNY_multinomial_product_le : ∃ (C : ℝ), 1 ≤ C ∧ ∀ {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (P : ℕ), ↑(∏ q ∈ nyAtP Nm mu P, Nat.multinomial (nxAtNY Nm mu q) (multiplicityNX Nm mu)) ≤ C ^ multiplicityP Nm mu P

Product form of the within-(N,Y) estimate at fixed P.

The exponent is exactly m_P, because the (N,Y) fibers in nyAtP partition the P-class.

theorem Anderson4D.fixedP_multinomial_le_outerNY : ∃ (C : ℝ), 1 ≤ C ∧ ∀ {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (P : ℕ), ↑(Nat.multinomial (nxAtP Nm mu P) (multiplicityNX Nm mu)) ≤ C ^ multiplicityP Nm mu P * ↑(Nat.multinomial (nyAtP Nm mu P) (multiplicityNY Nm mu))

Reduction from (5.80) to (5.81): at fixed P, summing over all (N,X) classes costs only an exponential factor times the multinomial of the coarser (N,Y) masses.

The algebraic skeleton of the S/C partition in (5.82)

The actual majority predicate and its simple/compound payoffs are deliberately left to the remaining (5.83)--(5.85) assembly listed in the module header.

def Anderson4D.boolFiber {ι : Type u_1} [DecidableEq ι] (s : Finset ι) (p : ι → Bool) (b : Bool) : Finset ι

Equations

• Anderson4D.boolFiber s p b = {i ∈ s | p i = b}

theorem Anderson4D.boolFiber_union {ι : Type u_1} [DecidableEq ι] (s : Finset ι) (p : ι → Bool) : boolFiber s p false ∪ boolFiber s p true = s

theorem Anderson4D.boolFiber_disjoint {ι : Type u_1} [DecidableEq ι] (s : Finset ι) (p : ι → Bool) : Disjoint (boolFiber s p false) (boolFiber s p true)

theorem Anderson4D.multinomial_bool (f : Bool → ℕ) : Nat.multinomial Finset.univ f = (f false + f true).choose (f false)

theorem Anderson4D.multinomial_bool_partition {ι : Type u_1} [DecidableEq ι] (s : Finset ι) (f : ι → ℕ) (p : ι → Bool) : Nat.multinomial s f = (∑ i ∈ boolFiber s p false, f i + ∑ i ∈ boolFiber s p true, f i).choose (∑ i ∈ boolFiber s p false, f i) * Nat.multinomial (boolFiber s p false) f * Nat.multinomial (boolFiber s p true) f

Exact factorial split underlying (5.82). The leading binomial chooses which copies belong to the false and true groups; the two remaining factors permute within the groups.

theorem Anderson4D.multinomial_bool_partition_le {ι : Type u_1} [DecidableEq ι] (s : Finset ι) (f : ι → ℕ) (p : ι → Bool) : Nat.multinomial s f ≤ (2 ^ ∑ i ∈ s, f i) * Nat.multinomial (boolFiber s p false) f * Nat.multinomial (boolFiber s p true) f

The generic algebraic inequality underlying paper (5.82), with loss 2^(∑ i, f i). Its paper specialization has exponent m_P; the theorem is independent of the simple/compound majority predicate.