ClusterDiameter

Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.

l.bad.clusters.geometry, clause (2): the diameter bound

diam(𝒩(𝒞)) < 4 · 3^{b(((n-1)∨1) + h_{(n-1)∨1})} · 3^{m-(((n-1)∨1) + h_{(n-1)∨1})}

As in clause (1) only the deterministic geometric layer is delivered: the statements are conditional on avoidance of the bad-cluster diameter failure, carried by the binder havoid, which is the manuscript's own conditioning on p.minimal.scale.separation (see the module docstring of ClusterLayerConstraint). No probability estimate is used.

The diameter carrier, and why this one

The printed diam(𝒩(𝒞)) is the diameter of a set of cubes. Two choices have to be made explicit.

• Closed or half-open cubes. closedCubeCarrier 𝒥 = ⋃_{□ ∈ 𝒥} \overline{□} takes the union of the closed cubes. This is the exact analogue of the site-level choice already proved in Provider/Percolation/ClusterTwo.lean, where closedLatDiam = latDiam + 1 — the diameter of the union of the closed cubes — was preferred to the centre-to-centre latDiam as "the larger and hence the faithful reading of the printed diam". The same reasoning applies here: cubeSet □ ⊆ \overline{□}, so closedCubeCarrier dominates the half-open union and the bound proved for it is the stronger statement.
• ℓ^∞ or Euclidean. Metric.diam on Vec d = Fin d → ℝ is the sup diameter, because the ambient metric on a Pi type is the sup metric. No such conversion is performed here; every statement below is an ℓ^∞ statement.
• Non-vacuity. Metric.diam is 0 on an unbounded set, so a diam bound is only informative together with boundedness of the carrier. The primitive content is in any case the pointwise estimate norm_sub_lt_three_rpow_add_three_of_mem_whitneyNeighborhood, which is what every consumer of a diameter actually uses, and from which both the diam bound diam_closedCubeCarrier_whitneyNeighborhood_lt_four_mul_three_rpow and the boundedness are read off.

The accounting, and where the factor 4 comes from

Write l for the least Whitney layer that 𝒩(𝒞) occupies, j ≤ l for the base index of the lift, L = j + h_j, s = m - L and A = 3^{bL}. Clause (1) places every cube of 𝒩(𝒞) in layer l or l+1, hence at depth ≥ L, hence at side ≤ 3^s; so every cube in sight — the two endpoint cubes □, □' of 𝒩(𝒞) and the two cubes Q, Q' ∈ 𝒞 they touch — has radius ≤ 3^s/2. The core estimate norm_cubeCenter_sub_lt_of_connected₂ of clause (1), run at the common lift depth L, gives ‖c_Q - c_{Q'}‖ < A·3^s, and the five-term triangle inequality

‖x - y‖ ≤ ρ□ + (ρ□ + ρQ) + ‖c_Q - c_{Q'}‖ + (ρQ' + ρ□') + ρ□'
        < 3^s/2 + 3^s + A·3^s + 3^s + 3^s/2 = (A + 3)·3^s

The printed display is stated at the index (n-1)∨1 for a layer n that 𝒩(𝒞) intersects. Clause (1) gives l ≤ n ≤ l+1 and 1 ≤ l, hence (n-1)∨1 ≤ l and l ≤ ((n-1)∨1) + 2, which is precisely the admissible range of base indices j in the general statements.

References

• ABK26, l.bad.clusters.geometry; e.cluster.diameter.bound; e.neighborhood.def; e.diameter.deterministic.

The closed carrier of a family of cubes

def Algsuperdiff.Section3.Provider.Whitney.closedCubeCarrier {d : ℕ} (J : Set (HCPolySupport.TriadicCube d)) : Set (HCPolySupport.Vec d)

The carrier of diam in e.cluster.diameter.bound: the union of the closed cubes of a family, a subset of Vec d = Fin d → ℝ, whose ambient metric is the sup metric.

Equations

• Algsuperdiff.Section3.Provider.Whitney.closedCubeCarrier J = ⋃ Q ∈ J, Metric.closedBall (HCPolySupport.cubeCenter Q) (HCPolySupport.cubeRadius Q)

theorem Algsuperdiff.Section3.Provider.Whitney.mem_closedCubeCarrier_iff {d : ℕ} {J : Set (HCPolySupport.TriadicCube d)} {x : HCPolySupport.Vec d} : x ∈ closedCubeCarrier J ↔ ∃ Q ∈ J, x ∈ Metric.closedBall (HCPolySupport.cubeCenter Q) (HCPolySupport.cubeRadius Q)

theorem Algsuperdiff.Section3.Provider.Whitney.closedBall_subset_closedCubeCarrier {d : ℕ} {J : Set (HCPolySupport.TriadicCube d)} {Q : HCPolySupport.TriadicCube d} (hQ : Q ∈ J) : Metric.closedBall (HCPolySupport.cubeCenter Q) (HCPolySupport.cubeRadius Q) ⊆ closedCubeCarrier J

The corrected rounding

theorem Algsuperdiff.Section3.Provider.Whitney.three_rpow_add_three_mul_lt_four_mul {b : ℝ} (hb0 : 0 < b) {hs k₀ : ℕ} (hk₀ : 3 ≤ k₀) (m : ℤ) (j : ℕ) : (3 ^ (b * ↑(j + whitneyScaleSeq b hs k₀ j)) + 3) * 3 ^ (m - ↑(j + whitneyScaleSeq b hs k₀ j)) < 4 * 3 ^ (b * ↑(j + whitneyScaleSeq b hs k₀ j)) * 3 ^ (m - ↑(j + whitneyScaleSeq b hs k₀ j))

The lift chain at a common base index

The headline estimates

theorem Algsuperdiff.Section3.Provider.Whitney.norm_sub_lt_three_rpow_add_three_of_mem_whitneyNeighborhood {d : ℕ} {M : ABKModel d} {m : ℤ} {b : ℝ} {hs k₀ : ℕ} {omega : Cutoff.CutoffSample d} (hb0 : 0 < b) (hb : b ≤ 1 / 8) (hk₀ : 3 ≤ k₀) (havoid : ∀ (h : ℕ), hs ≤ h → ∀ u ∈ Percolation.cubeFinset h, ↑(Percolation.badClusterDiam M m h omega u) < 3 ^ (b * ↑h)) {S : Set (HCPolySupport.TriadicCube d)} (hSsub : S ⊆ whitneyPartition m (whitneyScaleSeq b hs k₀)) (hSbad : ∀ Q ∈ S, omega ∈ BadEvents.bad M Q) {Q₀ : HCPolySupport.TriadicCube d} (hQ₀ : Q₀ ∈ S) {j : ℕ} (hjl : j ≤ leastWhitneyLayer m (whitneyScaleSeq b hs k₀) (whitneyNeighborhood m (whitneyScaleSeq b hs k₀) (badComponent S Q₀))) (hlj : leastWhitneyLayer m (whitneyScaleSeq b hs k₀) (whitneyNeighborhood m (whitneyScaleSeq b hs k₀) (badComponent S Q₀)) ≤ j + 2) {U W : HCPolySupport.TriadicCube d} (hU : U ∈ whitneyNeighborhood m (whitneyScaleSeq b hs k₀) (badComponent S Q₀)) (hW : W ∈ whitneyNeighborhood m (whitneyScaleSeq b hs k₀) (badComponent S Q₀)) {x y : HCPolySupport.Vec d} (hx : x ∈ Metric.closedBall (HCPolySupport.cubeCenter U) (HCPolySupport.cubeRadius U)) (hy : y ∈ Metric.closedBall (HCPolySupport.cubeCenter W) (HCPolySupport.cubeRadius W)) : ‖x - y‖ < (3 ^ (b * ↑(j + whitneyScaleSeq b hs k₀ j)) + 3) * 3 ^ (m - ↑(j + whitneyScaleSeq b hs k₀ j))

e.cluster.diameter.bound, the sharp pointwise form. On avoidance of the bad-cluster diameter failure, any two points of the closed cubes of the closure-touching neighborhood of a connected component of an abstract bad family are less than (3^{bL} + 3)·3^{m-L} apart in the ℓ^∞ sense, where L = j + h_j for any base index j inside the admissible window j ≤ n_min(𝒩(𝒞)) ≤ j + 2.

theorem Algsuperdiff.Section3.Provider.Whitney.diam_closedCubeCarrier_whitneyNeighborhood_lt_four_mul_three_rpow {d : ℕ} {M : ABKModel d} {m : ℤ} {b : ℝ} {hs k₀ : ℕ} {omega : Cutoff.CutoffSample d} (hb0 : 0 < b) (hb : b ≤ 1 / 8) (hk₀ : 3 ≤ k₀) (havoid : ∀ (h : ℕ), hs ≤ h → ∀ u ∈ Percolation.cubeFinset h, ↑(Percolation.badClusterDiam M m h omega u) < 3 ^ (b * ↑h)) {S : Set (HCPolySupport.TriadicCube d)} (hSsub : S ⊆ whitneyPartition m (whitneyScaleSeq b hs k₀)) (hSbad : ∀ Q ∈ S, omega ∈ BadEvents.bad M Q) {Q₀ : HCPolySupport.TriadicCube d} (hQ₀ : Q₀ ∈ S) {j : ℕ} (hjl : j ≤ leastWhitneyLayer m (whitneyScaleSeq b hs k₀) (whitneyNeighborhood m (whitneyScaleSeq b hs k₀) (badComponent S Q₀))) (hlj : leastWhitneyLayer m (whitneyScaleSeq b hs k₀) (whitneyNeighborhood m (whitneyScaleSeq b hs k₀) (badComponent S Q₀)) ≤ j + 2) : Metric.diam (closedCubeCarrier (whitneyNeighborhood m (whitneyScaleSeq b hs k₀) (badComponent S Q₀))) < 4 * 3 ^ (b * ↑(j + whitneyScaleSeq b hs k₀ j)) * 3 ^ (m - ↑(j + whitneyScaleSeq b hs k₀ j))

The printed display

theorem Algsuperdiff.Section3.Provider.Whitney.diam_closedCubeCarrier_whitneyNeighborhood_lt_of_intersectsLayer {d : ℕ} {M : ABKModel d} {m : ℤ} {b : ℝ} {hs k₀ : ℕ} {omega : Cutoff.CutoffSample d} (hb0 : 0 < b) (hb : b ≤ 1 / 8) (hk₀ : 3 ≤ k₀) (havoid : ∀ (h : ℕ), hs ≤ h → ∀ u ∈ Percolation.cubeFinset h, ↑(Percolation.badClusterDiam M m h omega u) < 3 ^ (b * ↑h)) {S : Set (HCPolySupport.TriadicCube d)} (hSsub : S ⊆ whitneyPartition m (whitneyScaleSeq b hs k₀)) (hSbad : ∀ Q ∈ S, omega ∈ BadEvents.bad M Q) {Q₀ : HCPolySupport.TriadicCube d} (hQ₀ : Q₀ ∈ S) {n : ℕ} (hmeet : IntersectsLayer m (whitneyScaleSeq b hs k₀) (whitneyNeighborhood m (whitneyScaleSeq b hs k₀) (badComponent S Q₀)) n) : Metric.diam (closedCubeCarrier (whitneyNeighborhood m (whitneyScaleSeq b hs k₀) (badComponent S Q₀))) < 4 * 3 ^ (b * ↑(max (n - 1) 1 + whitneyScaleSeq b hs k₀ (max (n - 1) 1))) * 3 ^ (m - ↑(max (n - 1) 1 + whitneyScaleSeq b hs k₀ (max (n - 1) 1)))

diam(𝒩(𝒞)) < 4 · 3^{b(((n-1)∨1)+h_{(n-1)∨1})} · 3^{m-(((n-1)∨1)+h_{(n-1)∨1})} .

The manuscript's own justification of the index shift — "n_min ≥ (n-1)∨1 whenever 𝒩(𝒞) intersects layer n" — is here the pair (n-1)∨1 ≤ n_min(𝒩(𝒞)) and n_min(𝒩(𝒞)) ≤ ((n-1)∨1) + 2, both read off the proved clause (1).