Anchored bidirectional sequence gain

In the general case of paper Step 4, the position carrying the smallest scale need not be the first position. The paper then sums "left and right separately" from that position. This file implements exactly that orientation:

• the left word starts at the anchor and reads the original word backwards;
• the right word starts at the anchor and reads the original word forwards;
• positions past either endpoint repeat the endpoint, hence contribute gain one;
• one global exception set is partitioned and reindexed into the two outward words.

For a fixed anchor, the original word injects into the pair consisting of its padded left and right words. The two unrestricted finite sums can therefore be bounded independently by the rectangular form of Lemma 5.13. Finally the at most m anchor positions cost only another exponential factor.

Words read outwards from an anchor

def Anderson4D.anchoredLeftWord {α : Type u_1} {n : ℕ} (a : Fin (n + 1)) (w : Fin (n + 1) → α) : Fin (n + 1) → α

Read a word from a towards the left. After reaching position zero, keep repeating the endpoint; all added consecutive-pair gains are therefore one.

Equations

• Anderson4D.anchoredLeftWord a w i = if h : ↑i ≤ ↑a then w ⟨↑a - ↑i, ⋯⟩ else w ⟨0, ⋯⟩

def Anderson4D.anchoredRightWord {α : Type u_1} {n : ℕ} (a : Fin (n + 1)) (w : Fin (n + 1) → α) : Fin (n + 1) → α

Read a word from a towards the right. After reaching the final position, keep repeating that endpoint.

Equations

• Anderson4D.anchoredRightWord a w i = if h : ↑a + ↑i < n + 1 then w ⟨↑a + ↑i, h⟩ else w (Fin.last n)

@[simp]

theorem Anderson4D.anchoredLeftWord_zero {α : Type u_1} {n : ℕ} (a : Fin (n + 1)) (w : Fin (n + 1) → α) : anchoredLeftWord a w 0 = w a

@[simp]

theorem Anderson4D.anchoredRightWord_zero {α : Type u_1} {n : ℕ} (a : Fin (n + 1)) (w : Fin (n + 1) → α) : anchoredRightWord a w 0 = w a

theorem Anderson4D.anchoredLeftWord_recover {α : Type u_1} {n : ℕ} (a j : Fin (n + 1)) (w : Fin (n + 1) → α) (hj : ↑j ≤ ↑a) : anchoredLeftWord a w ⟨↑a - ↑j, ⋯⟩ = w j

theorem Anderson4D.anchoredRightWord_recover {α : Type u_1} {n : ℕ} (a j : Fin (n + 1)) (w : Fin (n + 1) → α) (hj : ↑a ≤ ↑j) : anchoredRightWord a w ⟨↑j - ↑a, ⋯⟩ = w j

theorem Anderson4D.anchoredOutwardPair_injective {α : Type u_1} {n : ℕ} (a : Fin (n + 1)) : Function.Injective fun (w : Fin (n + 1) → α) => (anchoredLeftWord a w, anchoredRightWord a w)

theorem Anderson4D.anchoredLeftWord_map {α : Type u_1} {β : Type u_2} {n : ℕ} (f : α → β) (a : Fin (n + 1)) (w : Fin (n + 1) → α) : (anchoredLeftWord a fun (j : Fin (n + 1)) => f (w j)) = fun (j : Fin (n + 1)) => f (anchoredLeftWord a w j)

theorem Anderson4D.anchoredRightWord_map {α : Type u_1} {β : Type u_2} {n : ℕ} (f : α → β) (a : Fin (n + 1)) (w : Fin (n + 1) → α) : (anchoredRightWord a fun (j : Fin (n + 1)) => f (w j)) = fun (j : Fin (n + 1)) => f (anchoredRightWord a w j)

Reindexing one global exception set

def Anderson4D.anchoredLeftExceptionIndex {n : ℕ} (a : Fin (n + 1)) (j : Fin n) : Fin n

An original left edge is reflected into the outward-left indexing.

Equations

• Anderson4D.anchoredLeftExceptionIndex a j = ⟨↑a - 1 - ↑j, ⋯⟩

def Anderson4D.anchoredRightExceptionIndex {n : ℕ} (a : Fin (n + 1)) (j : Fin n) : Fin n

An original right edge is translated into the outward-right indexing.

Equations

• Anderson4D.anchoredRightExceptionIndex a j = ⟨↑j - ↑a, ⋯⟩

def Anderson4D.anchoredLeftExceptions {n : ℕ} (a : Fin (n + 1)) (E : Finset (Fin n)) : Finset (Fin n)

Exceptions on original edges strictly left of the anchor, reflected.

Equations

• Anderson4D.anchoredLeftExceptions a E = Finset.image (Anderson4D.anchoredLeftExceptionIndex a) ({j ∈ E | ↑j < ↑a})

def Anderson4D.anchoredRightExceptions {n : ℕ} (a : Fin (n + 1)) (E : Finset (Fin n)) : Finset (Fin n)

Exceptions on original edges at or right of the anchor, translated.

Equations

• Anderson4D.anchoredRightExceptions a E = Finset.image (Anderson4D.anchoredRightExceptionIndex a) ({j ∈ E | ↑a ≤ ↑j})

theorem Anderson4D.card_anchoredLeftExceptions {n : ℕ} (a : Fin (n + 1)) (E : Finset (Fin n)) : (anchoredLeftExceptions a E).card = {j ∈ E | ↑j < ↑a}.card

theorem Anderson4D.card_anchoredRightExceptions {n : ℕ} (a : Fin (n + 1)) (E : Finset (Fin n)) : (anchoredRightExceptions a E).card = {j ∈ E | ↑a ≤ ↑j}.card

theorem Anderson4D.card_anchoredExceptions_add {n : ℕ} (a : Fin (n + 1)) (E : Finset (Fin n)) : (anchoredLeftExceptions a E).card + (anchoredRightExceptions a E).card = E.card

The two side budgets are an exact partition of the one global budget.

theorem Anderson4D.card_anchoredLeftExceptions_le {n : ℕ} (a : Fin (n + 1)) (E : Finset (Fin n)) : (anchoredLeftExceptions a E).card ≤ E.card

theorem Anderson4D.card_anchoredRightExceptions_le {n : ℕ} (a : Fin (n + 1)) (E : Finset (Fin n)) : (anchoredRightExceptions a E).card ≤ E.card

Dyadic gains and the two outward products

noncomputable def Anderson4D.anchoredCodeEdgeGain (θ : ℝ) {n ν : ℕ} (e : Fin ν → ℤ) (w : Fin (n + 1) → Fin ν) (j : Fin n) : ℝ

One consecutive-pair gain for a code word of dyadic exponents.

Equations

• Anderson4D.anchoredCodeEdgeGain θ e w j = min 1 ((2 ^ e (w j.succ) / 2 ^ e (w j.castSucc)) ^ θ)

theorem Anderson4D.anchoredCodeEdgeGain_nonneg (θ : ℝ) {n ν : ℕ} (e : Fin ν → ℤ) (w : Fin (n + 1) → Fin ν) (j : Fin n) : 0 ≤ anchoredCodeEdgeGain θ e w j

theorem Anderson4D.anchoredLeftWord_eq_first_of_anchor_le {α : Type u_1} {n : ℕ} (a i : Fin (n + 1)) (w : Fin (n + 1) → α) (hi : ↑a ≤ ↑i) : anchoredLeftWord a w i = w 0

theorem Anderson4D.anchoredRightWord_eq_last_of_le_sum {α : Type u_1} {n : ℕ} (a i : Fin (n + 1)) (w : Fin (n + 1) → α) (hi : n ≤ ↑a + ↑i) : anchoredRightWord a w i = w (Fin.last n)

theorem Anderson4D.anchoredLeftCodeEdgeGain_at_original (θ : ℝ) {n ν : ℕ} (e : Fin ν → ℤ) (w : Fin (n + 1) → Fin ν) (a : Fin (n + 1)) (j : Fin n) (hj : ↑j < ↑a) : anchoredCodeEdgeGain θ e (anchoredLeftWord a w) (anchoredLeftExceptionIndex a j) = min 1 ((2 ^ e (w j.castSucc) / 2 ^ e (w j.succ)) ^ θ)

At a genuine original left edge, the outward-left word gives the reverse ratio: its current endpoint is j+1 and its next endpoint is j.

theorem Anderson4D.anchoredRightCodeEdgeGain_at_original (θ : ℝ) {n ν : ℕ} (e : Fin ν → ℤ) (w : Fin (n + 1) → Fin ν) (a : Fin (n + 1)) (j : Fin n) (hj : ↑a ≤ ↑j) : anchoredCodeEdgeGain θ e (anchoredRightWord a w) (anchoredRightExceptionIndex a j) = anchoredCodeEdgeGain θ e w j

At a genuine original right edge, the outward-right ratio is forward.

theorem Anderson4D.anchoredLeftCodeEdgeGain_eq_one_of_anchor_le (θ : ℝ) {n ν : ℕ} (e : Fin ν → ℤ) (w : Fin (n + 1) → Fin ν) (a : Fin (n + 1)) (j : Fin n) (hj : ↑a ≤ ↑j) : anchoredCodeEdgeGain θ e (anchoredLeftWord a w) j = 1

Every padded edge after the genuine left segment has gain exactly one.

theorem Anderson4D.anchoredRightCodeEdgeGain_eq_one_of_le_anchor_add (θ : ℝ) {n ν : ℕ} (e : Fin ν → ℤ) (w : Fin (n + 1) → Fin ν) (a : Fin (n + 1)) (j : Fin n) (hj : n ≤ ↑a + ↑j) : anchoredCodeEdgeGain θ e (anchoredRightWord a w) j = 1

Every padded edge after the genuine right segment has gain exactly one.

noncomputable def Anderson4D.anchoredLeftCodeWeight (θ : ℝ) {n ν : ℕ} (e : Fin ν → ℤ) (E : Finset (Fin n)) (a : Fin (n + 1)) (w : Fin (n + 1) → Fin ν) : ℝ

Equations

• Anderson4D.anchoredLeftCodeWeight θ e E a w = ∏ j ∈ Finset.univ \ Anderson4D.anchoredLeftExceptions a E, Anderson4D.anchoredCodeEdgeGain θ e (Anderson4D.anchoredLeftWord a w) j

noncomputable def Anderson4D.anchoredRightCodeWeight (θ : ℝ) {n ν : ℕ} (e : Fin ν → ℤ) (E : Finset (Fin n)) (a : Fin (n + 1)) (w : Fin (n + 1) → Fin ν) : ℝ

Equations

• Anderson4D.anchoredRightCodeWeight θ e E a w = ∏ j ∈ Finset.univ \ Anderson4D.anchoredRightExceptions a E, Anderson4D.anchoredCodeEdgeGain θ e (Anderson4D.anchoredRightWord a w) j

noncomputable def Anderson4D.anchoredBidirectionalCodeWeight (θ : ℝ) {n ν : ℕ} (e : Fin ν → ℤ) (E : Finset (Fin n)) (a : Fin (n + 1)) (w : Fin (n + 1) → Fin ν) : ℝ

The bidirectional weight: both products start at the same anchor, the left one in reverse original order and the right one in original order.

Equations

• Anderson4D.anchoredBidirectionalCodeWeight θ e E a w = Anderson4D.anchoredLeftCodeWeight θ e E a w * Anderson4D.anchoredRightCodeWeight θ e E a w

theorem Anderson4D.anchoredLeftCodeWeight_nonneg (θ : ℝ) {n ν : ℕ} (e : Fin ν → ℤ) (E : Finset (Fin n)) (a : Fin (n + 1)) (w : Fin (n + 1) → Fin ν) : 0 ≤ anchoredLeftCodeWeight θ e E a w

theorem Anderson4D.anchoredRightCodeWeight_nonneg (θ : ℝ) {n ν : ℕ} (e : Fin ν → ℤ) (E : Finset (Fin n)) (a : Fin (n + 1)) (w : Fin (n + 1) → Fin ν) : 0 ≤ anchoredRightCodeWeight θ e E a w

theorem Anderson4D.anchoredBidirectionalCodeWeight_nonneg (θ : ℝ) {n ν : ℕ} (e : Fin ν → ℤ) (E : Finset (Fin n)) (a : Fin (n + 1)) (w : Fin (n + 1) → Fin ν) : 0 ≤ anchoredBidirectionalCodeWeight θ e E a w

Fixed-anchor and all-anchor bounds

theorem Anderson4D.anchoredBidirectional_code_fixedAnchor_sum_le (θ : ℝ) (hθ : 0 < θ) (B : ℕ) : ∃ (C : ℝ), 1 ≤ C ∧ ∀ (n ν : ℕ) (e : Fin ν → ℤ), ν ≤ n + 1 → Function.Injective e → ∀ (E : Finset (Fin n)), E.card ≤ B → ∀ (a : Fin (n + 1)), ∑ w : Fin (n + 1) → Fin ν, anchoredBidirectionalCodeWeight θ e E a w ≤ C ^ (n + 1)

For a fixed anchor, left and right are bounded separately by Lemma 5.13. The map from the original word to the pair of outward words is injective, so enlarging to all pairs is a valid nonnegative overcount.

theorem Anderson4D.anchoredBidirectional_code_sum_le (θ : ℝ) (hθ : 0 < θ) (B : ℕ) : ∃ (C : ℝ), 1 ≤ C ∧ ∀ (n ν : ℕ) (e : Fin ν → ℤ), ν ≤ n + 1 → Function.Injective e → ∀ (E : Finset (Fin n)), E.card ≤ B → ∑ a : Fin (n + 1), ∑ w : Fin (n + 1) → Fin ν, anchoredBidirectionalCodeWeight θ e E a w ≤ C ^ (n + 1)

Sum also over the choice of anchor position. Since there are n+1 positions and n+1 ≤ 2^(n+1), that final choice is absorbed into the universal exponential base.

Reindexing to the active paper carrier

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

One consecutive-pair gain on the actual active P carrier.

Equations

• Anderson4D.anchoredActivePEdgeGain θ w j = min 1 ((↑↑(w j.succ) / ↑↑(w j.castSucc)) ^ θ)

noncomputable def Anderson4D.anchoredBidirectionalActivePWeight (θ : ℝ) {t : PlaneTree} {Nm : t.HeppMarking} {mu : t.Multiplicities} {n : ℕ} (E : Finset (Fin n)) (a : Fin (n + 1)) (w : Fin (n + 1) → ActivePClass Nm mu) : ℝ

Actual-carrier form of the two products read outwards from the anchor.

Equations

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

theorem Anderson4D.anchoredActivePEdgeGain_enumeration (θ : ℝ) {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) {n : ℕ} (x : Fin (n + 1) → Fin (activePCount Nm mu)) (j : Fin n) : anchoredActivePEdgeGain θ (fun (i : Fin (n + 1)) => (activePEnumeration Nm mu) (x i)) j = anchoredCodeEdgeGain θ (activePExponent Nm mu) x j

theorem Anderson4D.anchoredBidirectionalActivePWeight_enumeration (θ : ℝ) {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) {n : ℕ} (E : Finset (Fin n)) (a : Fin (n + 1)) (x : Fin (n + 1) → Fin (activePCount Nm mu)) : (anchoredBidirectionalActivePWeight θ E a fun (i : Fin (n + 1)) => (activePEnumeration Nm mu) (x i)) = anchoredBidirectionalCodeWeight θ (activePExponent Nm mu) E a x

theorem Anderson4D.anchoredBidirectional_activeP (θ : ℝ) (hθ : 0 < θ) (B : ℕ) : ∃ (C : ℝ), 1 ≤ C ∧ ∀ {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (n : ℕ), activePCount Nm mu ≤ n + 1 → ∀ (E : Finset (Fin n)), E.card ≤ B → ∑ a : Fin (n + 1), ∑ w : Fin (n + 1) → ActivePClass Nm mu, anchoredBidirectionalActivePWeight θ E a w ≤ C ^ (n + 1)

Assembly-facing active-P form for an arbitrary positive exponent and fixed global exception budget. The constant is outside the tree, marking, multiplicity, length, exception, anchor, and word quantifiers.

theorem Anderson4D.anchoredBidirectional_activeP_oneEighth_hundred : ∃ (C : ℝ), 1 ≤ C ∧ ∀ {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (n : ℕ), activePCount Nm mu ≤ n + 1 → ∀ (E : Finset (Fin n)), E.card ≤ 100 → ∑ a : Fin (n + 1), ∑ w : Fin (n + 1) → ActivePClass Nm mu, anchoredBidirectionalActivePWeight (1 / 8) E a w ≤ C ^ (n + 1)

The local inequalities initially produce the 1/8 gain. This specialization is retained for the inner-estimate boundary.

theorem Anderson4D.anchoredBidirectional_activeP_oneSixteenth_hundred : ∃ (C : ℝ), 1 ≤ C ∧ ∀ {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (n : ℕ), activePCount Nm mu ≤ n + 1 → ∀ (E : Finset (Fin n)), E.card ≤ 100 → ∑ a : Fin (n + 1), ∑ w : Fin (n + 1) → ActivePClass Nm mu, anchoredBidirectionalActivePWeight (1 / 16) E a w ≤ C ^ (n + 1)

Counting interface at the 1/16 exponent used by the separately proved even/odd geometric-mean assembly in Step 4.

theorem Anderson4D.anchoredBidirectional_activeP_oneTwentieth_hundred : ∃ (C : ℝ), 1 ≤ C ∧ ∀ {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (n : ℕ), activePCount Nm mu ≤ n + 1 → ∀ (E : Finset (Fin n)), E.card ≤ 100 → ∑ a : Fin (n + 1), ∑ w : Fin (n + 1) → ActivePClass Nm mu, anchoredBidirectionalActivePWeight (1 / 20) E a w ≤ C ^ (n + 1)

Counting interface at the paper's weakened 1/20 exponent, for use after the separately proved outer/inner Hölder allocation.

The literal paper-length specialization. Here n = m - 1 is the number of adjacent edges and the outer sum ranges over all m possible anchor positions.

theorem Anderson4D.anchoredBidirectional_totalMultiplicity (θ : ℝ) (hθ : 0 < θ) (B : ℕ) : ∃ (C : ℝ), 1 ≤ C ∧ ∀ {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities), let n := totalMultiplicity mu - 1; ∀ (E : Finset (Fin n)), E.card ≤ B → ∑ a : Fin (n + 1), ∑ w : Fin (n + 1) → ActivePClass Nm mu, anchoredBidirectionalActivePWeight θ E a w ≤ C ^ totalMultiplicity mu

theorem Anderson4D.anchoredBidirectional_totalMultiplicity_oneEighth_hundred : ∃ (C : ℝ), 1 ≤ C ∧ ∀ {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities), let n := totalMultiplicity mu - 1; ∀ (E : Finset (Fin n)), E.card ≤ 100 → ∑ a : Fin (n + 1), ∑ w : Fin (n + 1) → ActivePClass Nm mu, anchoredBidirectionalActivePWeight (1 / 8) E a w ≤ C ^ totalMultiplicity mu

theorem Anderson4D.anchoredBidirectional_totalMultiplicity_oneSixteenth_hundred : ∃ (C : ℝ), 1 ≤ C ∧ ∀ {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities), let n := totalMultiplicity mu - 1; ∀ (E : Finset (Fin n)), E.card ≤ 100 → ∑ a : Fin (n + 1), ∑ w : Fin (n + 1) → ActivePClass Nm mu, anchoredBidirectionalActivePWeight (1 / 16) E a w ≤ C ^ totalMultiplicity mu

theorem Anderson4D.anchoredBidirectional_totalMultiplicity_oneTwentieth_hundred : ∃ (C : ℝ), 1 ≤ C ∧ ∀ {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities), let n := totalMultiplicity mu - 1; ∀ (E : Finset (Fin n)), E.card ≤ 100 → ∑ a : Fin (n + 1), ∑ w : Fin (n + 1) → ActivePClass Nm mu, anchoredBidirectionalActivePWeight (1 / 20) E a w ≤ C ^ totalMultiplicity mu

Paper specialization

The generic theorem above handles an arbitrary anchor and one global exception set of any fixed budget. The 1/8, budget-100 result is stronger than the paper's intermediate 20/40-exception uses. In particular, no pointwise comparison between a forward and a reverse gain is used: the two outward finite sums are independent applications of Lemma 5.13.

theorem Anderson4D.anchoredBidirectional_code_oneEighth_hundred : ∃ (C : ℝ), 1 ≤ C ∧ ∀ (n ν : ℕ) (e : Fin ν → ℤ), ν ≤ n + 1 → Function.Injective e → ∀ (E : Finset (Fin n)), E.card ≤ 100 → ∑ a : Fin (n + 1), ∑ w : Fin (n + 1) → Fin ν, anchoredBidirectionalCodeWeight (1 / 8) e E a w ≤ C ^ (n + 1)