Recursive connecting networks for admissible Hepp clusters

This file closes the geometric input left abstract in ClusterCover.lean. At a branching vertex, the connected child-link relation is used to join the already constructed child networks. The construction charges each child network once and at most one scale-sized link for every vertex removed from the finite child-link graph.

Finite edge-set networks

structure Anderson4D.FiniteMetricNetwork (V : Type u) : Type u

A finite set of undirected edges whose associated simple graph is connected. Keeping the edge set as data makes recursive gluing and cost accounting independent of decidability choices for graph adjacency.

• edges : Finset (Sym2 V)
• connected : (SimpleGraph.fromEdgeSet ↑self.edges).Connected

def Anderson4D.finiteNetworkCost {V : Type u} (d : V → V → ℝ) (hsymm : ∀ (a b : V), d a b = d b a) (N : FiniteMetricNetwork V) : ℝ

Cost of a finite network for a symmetric edge weight.

Equations

• Anderson4D.finiteNetworkCost d hsymm N = ∑ e ∈ N.edges, Anderson4D.sym2Weight d hsymm e

Child-link spanning trees and their geometric bridge edges

@[reducible, inline]

abbrev Anderson4D.ClusterChild {t : PlaneTree} (v : t.VPos) : Type

Equations

• Anderson4D.ClusterChild v = ↥(Anderson4D.childrenOf v)

@[reducible, inline]

abbrev Anderson4D.ClusterLeafAt {t : PlaneTree} (v : t.VPos) : Type

Equations

• Anderson4D.ClusterLeafAt v = ↥(Anderson4D.leavesUnder v)

Gluing the child networks at one branch

Recursion over the carrier tree

theorem Anderson4D.exists_finiteMetricNetwork_of_isAdmissible {t : PlaneTree} {Nm : t.HeppMarking} {M : ℕ} {z : ↥t.Leaves → Fin 4 → ℤ} (hadm : IsAdmissible Nm M z) (v : t.VPos) : ∃ (P : FiniteMetricNetwork (ClusterLeafAt v)), finiteNetworkCost (clusterLeafDistance z v) ⋯ P ≤ tildeScale Nm v

Every admissible embedded cluster has a finite connected leaf network whose total geometric length is at most its accumulated Hepp scale.

theorem Anderson4D.hasClusterNetwork_of_isAdmissible {t : PlaneTree} {Nm : t.HeppMarking} {M : ℕ} {z : ↥t.Leaves → Fin 4 → ℤ} (hadm : IsAdmissible Nm M z) (v : t.VPos) : HasClusterNetwork Nm z v

The recursive finite edge-set construction supplies the exact connected network certificate consumed by ClusterCover.

theorem Anderson4D.exists_clusterCover_of_isAdmissible {t : PlaneTree} {Nm : t.HeppMarking} {M : ℕ} {z : ↥t.Leaves → Fin 4 → ℤ} (hadm : IsAdmissible Nm M z) (v : t.VPos) {R : ℝ} (hR : 0 < R) : ∃ Q ⊆ Finset.image z (leavesUnder v), (∀ l ∈ leavesUnder v, ∃ q ∈ Q, znorm (z l - q) ≤ R) ∧ ↑Q.card ≤ 3 * (1 + tildeScale Nm v / R)

Paper (5.22b). Every admissible cluster below v has a cover by embedded leaf centres of radius R and cardinality at most 3 * (1 + tildeScale Nm v / R).