The outer P-word gain in the single-scale estimate

This file isolates the P-word gain estimate (5.77), which is the sequence input used in (5.76), including the paper's indexing convention. A word of length k + 2 has k + 1 adjacent edges. The first edge is omitted because the product in (5.76) starts at the one-based index j = 2; E : Finset (Fin k) records at most 99 further omitted edges and is shifted one place to the right. Thus the bounded-skip form of Lemma 5.13 is used with the honest total budget 100.

The active P values are first replaced by the finite subtype of pCarrier. Only that subtype is enumerated by Fin ν. Its dyadic exponents are injective because the values in the carrier are distinct; repeated occurrences of a P value in a word remain arbitrary repetitions of the corresponding Fin ν index.

The active P carrier and its dyadic enumeration

@[reducible, inline]

abbrev Anderson4D.activePCount {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) : ℕ

Number ν of distinct active dyadic P values.

Equations

• Anderson4D.activePCount Nm mu = Fintype.card (Anderson4D.ActivePClass Nm mu)

noncomputable def Anderson4D.activePEnumeration {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) : Fin (activePCount Nm mu) ≃ ActivePClass Nm mu

A fixed enumeration of the distinct active P values.

Equations

• Anderson4D.activePEnumeration Nm mu = (Fintype.equivFin (Anderson4D.ActivePClass Nm mu)).symm

theorem Anderson4D.activeP_eq_pow_log {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (P : ActivePClass Nm mu) : ↑P = 2 ^ Nat.log 2 ↑P

On the active carrier, taking Nat.log 2 recovers the dyadic value.

noncomputable def Anderson4D.activePExponent {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (i : Fin (activePCount Nm mu)) : ℤ

Integer exponent attached to the enumerated dyadic value.

Equations

• Anderson4D.activePExponent Nm mu i = ↑(Nat.log 2 ↑((Anderson4D.activePEnumeration Nm mu) i))

theorem Anderson4D.activePExponent_injective {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) : Function.Injective (activePExponent Nm mu)

The exponent family, rather than a word containing repeated exponent indices, is injective.

theorem Anderson4D.activePEnumeration_cast_eq_zpow {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (i : Fin (activePCount Nm mu)) : ↑↑((activePEnumeration Nm mu) i) = 2 ^ activePExponent Nm mu i

The enumerated natural P is exactly the corresponding real zpow.

theorem Anderson4D.activePCount_le_totalMultiplicity {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) : activePCount Nm mu ≤ totalMultiplicity mu

There are no more distinct active P values than word positions. The three classification maps can only decrease cardinality, and every leaf multiplicity is at least two (in particular at least one).

theorem Anderson4D.two_le_totalMultiplicity {t : PlaneTree} (mu : t.Multiplicities) : 2 ≤ totalMultiplicity mu

Every paper word has length at least two.

The edge shift in (5.76)

def Anderson4D.outerTailEdgeEmbedding (k : ℕ) : Fin k ↪ Fin (k + 1)

Shift a tail edge one position to the right in the full edge list.

Equations

• Anderson4D.outerTailEdgeEmbedding k = { toFun := Fin.succ, inj' := ⋯ }

@[simp]

theorem Anderson4D.outerTailEdgeEmbedding_ne_zero {k : ℕ} (i : Fin k) : (outerTailEdgeEmbedding k) i ≠ 0

def Anderson4D.outerGainExceptions {k : ℕ} (E : Finset (Fin k)) : Finset (Fin (k + 1))

The full exception set: the first edge, omitted because the product in (5.76) starts at j = 2, together with the shifted additional exceptions.

Equations

• Anderson4D.outerGainExceptions E = insert 0 (Finset.map (Anderson4D.outerTailEdgeEmbedding k) E)

@[simp]

theorem Anderson4D.mem_outerGainExceptions_zero {k : ℕ} (E : Finset (Fin k)) : 0 ∈ outerGainExceptions E

@[simp]

theorem Anderson4D.mem_outerGainExceptions_succ {k : ℕ} (E : Finset (Fin k)) (j : Fin k) : j.succ ∈ outerGainExceptions E ↔ j ∈ E

theorem Anderson4D.card_outerGainExceptions {k : ℕ} (E : Finset (Fin k)) : (outerGainExceptions E).card = E.card + 1

theorem Anderson4D.card_outerGainExceptions_le_hundred {k : ℕ} {E : Finset (Fin k)} (hE : E.card ≤ 99) : (outerGainExceptions E).card ≤ 100

theorem Anderson4D.fullEdges_diff_outerGainExceptions {k : ℕ} (E : Finset (Fin k)) : Finset.univ \ outerGainExceptions E = Finset.map (outerTailEdgeEmbedding k) (Finset.univ \ E)

After removing the first edge, the remaining full edge indices are exactly the successors of the tail indices not in E.

theorem Anderson4D.prod_diff_outerGainExceptions_eq_tail {k : ℕ} (E : Finset (Fin k)) (f : Fin (k + 1) → ℝ) : ∏ j ∈ Finset.univ \ outerGainExceptions E, f j = ∏ i ∈ Finset.univ \ E, f i.succ

Product-level form of the one-place edge-index shift.

The rectangular sequence estimate at θ = 1/20

theorem Anderson4D.outerGain_code_sum_le : ∃ (C : ℝ), 1 ≤ C ∧ ∀ (k ν : ℕ) (e : Fin ν → ℤ), ν ≤ k + 2 → Function.Injective e → ∀ (E : Finset (Fin k)), E.card ≤ 99 → ∑ x : Fin (k + 2) → Fin ν, ∏ j ∈ Finset.univ \ outerGainExceptions E, min 1 ((2 ^ e (x j.succ) / 2 ^ e (x j.castSucc)) ^ (1 / 20)) ≤ C ^ (k + 2)

Paper (5.77), in its exact rectangular form.

The word has length k + 2, while ν is only the number of distinct dyadic values. Entries of a word may repeat. The first edge and at most 99 additional tail edges are omitted, so Lemma 5.13 is invoked with budget 100. The constant is outside all data quantifiers.

Reindexing the actual paper carrier

noncomputable def Anderson4D.activePWordEquiv {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (M : ℕ) : (Fin M → Fin (activePCount Nm mu)) ≃ (Fin M → ActivePClass Nm mu)

Pointwise enumeration equivalence, used to reindex whole P words.

Equations

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

noncomputable def Anderson4D.outerPWordGain {t : PlaneTree} {Nm : t.HeppMarking} {mu : t.Multiplicities} {k : ℕ} (w : Fin (k + 2) → ActivePClass Nm mu) (j : Fin (k + 1)) : ℝ

The actual min(1,(P_{j+1}/P_j)^{1/20}) factor in (5.76).

Equations

• Anderson4D.outerPWordGain w j = min 1 ((↑↑(w j.succ) / ↑↑(w j.castSucc)) ^ (1 / 20))

noncomputable def Anderson4D.outerPWordTailGain {t : PlaneTree} {Nm : t.HeppMarking} {mu : t.Multiplicities} {k : ℕ} (w : Fin (k + 2) → ActivePClass Nm mu) (i : Fin k) : ℝ

The same gain indexed directly by the paper's tail positions: i = 0 represents the one-based edge j = 2.

Equations

• Anderson4D.outerPWordTailGain w i = Anderson4D.outerPWordGain w i.succ

theorem Anderson4D.outerGain_activeP_sum_le : ∃ (C : ℝ), 1 ≤ C ∧ ∀ {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (k : ℕ), activePCount Nm mu ≤ k + 2 → ∀ (E : Finset (Fin k)), E.card ≤ 99 → ∑ w : Fin (k + 2) → ActivePClass Nm mu, ∏ j ∈ Finset.univ \ outerGainExceptions E, outerPWordGain w j ≤ C ^ (k + 2)

Actual-carrier form of (5.77).

This is the assembly-facing theorem: the sum is over words in the subtype of active natural P values, and the factors are literal ratios of those values. The only cardinality assumption is the necessary rectangular one ν ≤ k + 2; it is discharged for the paper word by activePCount_le_totalMultiplicity.

theorem Anderson4D.outerGain_activeP_tail_sum_le : ∃ (C : ℝ), 1 ≤ C ∧ ∀ {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (k : ℕ), activePCount Nm mu ≤ k + 2 → ∀ (E : Finset (Fin k)), E.card ≤ 99 → ∑ w : Fin (k + 2) → ActivePClass Nm mu, ∏ i ∈ Finset.univ \ E, outerPWordTailGain w i ≤ C ^ (k + 2)

Literal tail-indexed form of the (5.77) gain used in (5.76): a length-k+2 word, product over its one-based edges j = 2, ..., k+1, with at most 99 of those factors removed.

theorem Anderson4D.outerGain_totalMultiplicity_sum_le : ∃ (C : ℝ), 1 ≤ C ∧ ∀ {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities), let k := totalMultiplicity mu - 2; ∀ (E : Finset (Fin k)), E.card ≤ 99 → ∑ w : Fin (k + 2) → ActivePClass Nm mu, ∏ j ∈ Finset.univ \ outerGainExceptions E, outerPWordGain w j ≤ C ^ totalMultiplicity mu

Paper specialization: choose the word length to be the total multiplicity.

Writing the length as (m - 2) + 2 keeps the first-edge shift definitionally transparent. two_le_totalMultiplicity proves that this is exactly m, and no extra hypothesis beyond the project data is needed.

theorem Anderson4D.outerGain_totalMultiplicity_tail_sum_le : ∃ (C : ℝ), 1 ≤ C ∧ ∀ {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities), have k := totalMultiplicity mu - 2; ∀ (E : Finset (Fin k)), E.card ≤ 99 → ∑ w : Fin (k + 2) → ActivePClass Nm mu, ∏ i ∈ Finset.univ \ E, outerPWordTailGain w i ≤ C ^ totalMultiplicity mu

Total-multiplicity specialization of the literal tail-indexed theorem.