Final endpoint-preserving lattice assembly

This file combines the non-extremal, extremal, and bare-leaf branches of the endpoint-preserving Hepp-tree decomposition. The endpoint bracket is never discarded.

theorem Anderson4D.primitiveEndpointTreeIncidenceSum_le_of_card_eq_aux {C : ℝ} (hC : PermSumEstimate C) {M n K : ℕ} (hn : 2 ≤ n) {t : PlaneTree} (ht : t.isValid = true) (hroot : t.rootV ∈ t.BranchNodes) (mu : t.Multiplicities) (htotal : totalMultiplicity mu = 2 * n) (hcard : (nonrootBranches t).card = n - 2) (hnL : n ≤ K * (Nat.log 2 (4 * M) + 1)) (Y : Finset (Fin (2 * n) → Z4)) (A : Finset (Fin (2 * n))) (x₀ x₁ : Z4) : primitiveEndpointTreeIncidenceSum M n ⋯ t Y A x₀ x₁ ≤ volumeEstimateFinalConstant ^ t.leafCount * (1 + 2 * ↑t.leafCount) ^ 2 * latticeBracketInvFourth x₀ x₁ * (↑(n * n) * ((256 * (4 * C) * (↑K + 1)) ^ n * ↑(Nat.log 2 (4 * M) + 1) ^ (n - 2)))

Extremal counterpart of primitiveEndpointTreeIncidenceSum_le_of_card_lt_aux.

noncomputable def Anderson4D.primitiveEndpointTreeRawBound (C : ℝ) (M n K : ℕ) (t : PlaneTree) (x₀ x₁ : Z4) : ℝ

A common nonnegative raw bound for every tree branch.

Equations

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

theorem Anderson4D.primitiveEndpointTreeRawBound_nonneg {C : ℝ} (hC : 0 ≤ C) (M n K : ℕ) (t : PlaneTree) (x₀ x₁ : Z4) : 0 ≤ primitiveEndpointTreeRawBound C M n K t x₀ x₁

theorem Anderson4D.primitiveEndpointTreeTupleIncidence_le_rawBound {C : ℝ} (hC : PermSumEstimate C) {M n K : ℕ} (hn : 2 ≤ n) {t : PlaneTree} (ht : t.isValid = true) (hnL : n ≤ K * (Nat.log 2 (4 * M) + 1)) (A : Finset (Fin (2 * n))) (x₀ x₁ : Z4) : primitiveEndpointTreeIncidenceSum M n ⋯ t (primitiveEndpointTreeTupleFamily M n ⋯ t A x₀ x₁) A x₀ x₁ ≤ primitiveEndpointTreeRawBound C M n K t x₀ x₁

Uniform raw bound for the tree slice which actually occurs in the endpoint lattice cover.

theorem Anderson4D.primitiveEndpointLatticeSum_le_rawTreeSum {C : ℝ} (hC : PermSumEstimate C) {M n K : ℕ} (hn : 2 ≤ n) (hnL : n ≤ K * (Nat.log 2 (4 * M) + 1)) (A : Finset (Fin (2 * n))) (x₀ x₁ : Z4) : primitiveEndpointLatticeSum M n ⋯ A x₀ x₁ ≤ ∑ t ∈ rdec_treeEnum (2 * n), primitiveEndpointTreeRawBound C M n K t x₀ x₁

Complete discrete endpoint estimate, retaining only a finite sum of explicit nonnegative raw tree bounds.

theorem Anderson4D.primitiveEndpointTreeRawBound_le_uniform {C : ℝ} (hC : 0 ≤ C) {M n K : ℕ} {t : PlaneTree} (hleaf : t.leafCount ≤ 2 * n) (x₀ x₁ : Z4) : primitiveEndpointTreeRawBound C M n K t x₀ x₁ ≤ latticeBracketInvFourth x₀ x₁ * ((8 * (↑K + 1)) ^ n * ↑(Nat.log 2 (4 * M) + 1) ^ (n - 2) + (16 * volumeEstimateFinalConstant) ^ (2 * n) * (↑(2 ^ n) * ((32 * (4 * C) * (↑K + 1)) ^ n * ↑(Nat.log 2 (4 * M) + 1) ^ (n - 2)) + ↑(n * n) * ((256 * (4 * C) * (↑K + 1)) ^ n * ↑(Nat.log 2 (4 * M) + 1) ^ (n - 2))))

Uniformize the only tree-dependent scalar in the raw bound using leafCount ≤ 2n from the enumerating carrier.

theorem Anderson4D.primitiveEndpointLatticeSum_le_uniformTreeBound {C : ℝ} (hC : PermSumEstimate C) {M n K : ℕ} (hn : 2 ≤ n) (hnL : n ≤ K * (Nat.log 2 (4 * M) + 1)) (A : Finset (Fin (2 * n))) (x₀ x₁ : Z4) : primitiveEndpointLatticeSum M n ⋯ A x₀ x₁ ≤ ↑(4 ^ (4 * (2 * n))) * (latticeBracketInvFourth x₀ x₁ * ((8 * (↑K + 1)) ^ n * ↑(Nat.log 2 (4 * M) + 1) ^ (n - 2) + (16 * volumeEstimateFinalConstant) ^ (2 * n) * (↑(2 ^ n) * ((32 * (4 * C) * (↑K + 1)) ^ n * ↑(Nat.log 2 (4 * M) + 1) ^ (n - 2)) + ↑(n * n) * ((256 * (4 * C) * (↑K + 1)) ^ n * ↑(Nat.log 2 (4 * M) + 1) ^ (n - 2)))))

Sum the raw bounds over the exponentially bounded tree carrier.