Increasing Green-tree integrability for R-324

Expanding every renormalized difference in (4.18) replaces selected edges of the linear Green chain by shortcuts whose left endpoint is still earlier than the right endpoint. Every expanded summand is therefore an increasing rooted tree: vertex i+1 has one parent among 0,...,i.

This file proves joint integrability of the Green product for every such parent map. The proof removes the terminal vertex, uses Haar translation invariance for its single incident parent edge, and transports the result through the terminal-coordinate measurable equivalence.

@[reducible, inline]

abbrev Anderson4D.IncreasingTreeParent (n : ℕ) : Type

An increasing rooted tree on vertices Fin (n+1): the edge indexed by i : Fin n joins vertex i+1 to a parent in {0,...,i}.

Equations

• Anderson4D.IncreasingTreeParent n = ((i : Fin n) → Fin (↑i + 1))

def Anderson4D.increasingTreeParentVertex {n : ℕ} (parent : IncreasingTreeParent n) (i : Fin n) : Fin (n + 1)

Embed the dependent parent index into the common vertex carrier.

Equations

• Anderson4D.increasingTreeParentVertex parent i = Fin.castLE ⋯ (parent i)

noncomputable def Anderson4D.increasingTreeGreenProduct {n : ℕ} (parent : IncreasingTreeParent n) (x : Fin (n + 1) → T4) : ℂ

Product of one Green factor along every edge of an increasing tree.

Equations

• Anderson4D.increasingTreeGreenProduct parent x = ∏ i : Fin n, ↑(Anderson4D.greenFn (x (Anderson4D.increasingTreeParentVertex parent i) - x i.succ))

def Anderson4D.IncreasingTreeParent.init {n : ℕ} (parent : IncreasingTreeParent (n + 1)) : IncreasingTreeParent n

Restrict an increasing parent map to all nonterminal edges.

Equations

• parent.init i = parent i.castSucc

def Anderson4D.IncreasingTreeParent.last {n : ℕ} (parent : IncreasingTreeParent (n + 1)) : Fin (n + 1)

Parent of the terminal vertex, cast to the complete preceding carrier.

Equations

• parent.last = Fin.cast ⋯ (parent (Fin.last n))

noncomputable def Anderson4D.increasingTreeLastEquiv (n : ℕ) : (Fin (n + 2) → T4) ≃ᵐ T4 × (Fin (n + 1) → T4)

Separate the terminal vertex from all preceding vertices.

Equations

• Anderson4D.increasingTreeLastEquiv n = MeasurableEquiv.piFinSuccAbove (fun (x : Fin (n + 2)) => Anderson4D.T4) (Fin.last (n + 1))

@[simp]

theorem Anderson4D.increasingTreeLastEquiv_symm_apply (n : ℕ) (y : T4) (v : Fin (n + 1) → T4) : (increasingTreeLastEquiv n).symm (y, v) = Fin.snoc v y

theorem Anderson4D.measurePreserving_increasingTreeLastEquiv (n : ℕ) : MeasureTheory.MeasurePreserving (⇑(increasingTreeLastEquiv n)) (MeasureTheory.Measure.pi fun (x : Fin (n + 2)) => paperMeasure) (paperMeasure.prod (MeasureTheory.Measure.pi fun (x : Fin (n + 1)) => paperMeasure))

theorem Anderson4D.increasingTreeGreenProduct_snoc {n : ℕ} (parent : IncreasingTreeParent (n + 1)) (v : Fin (n + 1) → T4) (y : T4) : increasingTreeGreenProduct parent (Fin.snoc v y) = ↑(greenFn (y - v parent.last)) * increasingTreeGreenProduct parent.init v

Terminal-vertex factorization of an increasing Green tree.

theorem Anderson4D.integrable_increasingTreeGreenProduct {n : ℕ} (parent : IncreasingTreeParent n) : MeasureTheory.Integrable (increasingTreeGreenProduct parent) (MeasureTheory.Measure.pi fun (x : Fin (n + 1)) => paperMeasure)

Every increasing Green tree is jointly integrable in all its vertices. This is the tree analogue of integrable_weightedGreenPath_joint.