Minimizer

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

Lexicographic crossing-path minimizers

This file formulates the path selected by first minimizing the number of inflated-good vertices and then its length. The second minimization is the mechanism that controls excursions through an occurring inflated cube.

def Algsuperdiff.Section5.Percolation.spliceGeodesic {d : ℕ} (Γ : List (Site d)) (i j : Fin Γ.length) : List (Site d)

Replace the part of Γ from positions i through j by the synchronous geodesic joining the two indexed vertices.

Equations

• Algsuperdiff.Section5.Percolation.spliceGeodesic Γ i j = List.take (↑i) Γ ++ Algsuperdiff.Section5.Percolation.geodesic (Γ.get i) (Γ.get j) ++ List.drop (↑j + 1) Γ

def Algsuperdiff.Section5.Percolation.pathWalk {d : ℕ} (x : Site d) (xs : List (Site d)) : IsPath (x :: xs) → (latticeGraph d).Walk x ((x :: xs).getLast ⋯)

Convert a list satisfying the lattice path relation into a graph walk.

Equations

• Algsuperdiff.Section5.Percolation.pathWalk x [] _h = SimpleGraph.Walk.nil
• Algsuperdiff.Section5.Percolation.pathWalk x (y :: ys) h = SimpleGraph.Walk.cons ⋯ (Algsuperdiff.Section5.Percolation.pathWalk y ys ⋯)

theorem Algsuperdiff.Section5.Percolation.exists_nodup_crossing_subpath {d k : ℕ} {Γ : List (Site d)} (hΓ : IsPathFrom k Γ) : ∃ (Δ : List (Site d)), IsPathFrom k Δ ∧ Δ.Nodup ∧ Δ ⊆ Γ

Every crossing walk has a crossing subpath with no repeated vertices and no new vertices.

noncomputable def Algsuperdiff.Section5.Percolation.inflatedGoodVertexCountNat {Ω : Type u_1} {d : ℕ} (B : ℕ → Site d → Set Ω) (Γ : List (Site d)) (ω : Ω) : ℕ

The number of distinct vertices of Γ outside the inflated bad set.

Equations

• Algsuperdiff.Section5.Percolation.inflatedGoodVertexCountNat B Γ ω = {z ∈ Γ.toFinset | ω ∉ Algsuperdiff.Section5.Percolation.inflatedBadSet B z}.card

def Algsuperdiff.Section5.Percolation.IsPreferredPath {Ω : Type u_1} {d : ℕ} (B : ℕ → Site d → Set Ω) (k : ℕ) (ω : Ω) (Γ : List (Site d)) : Prop

A crossing path preferred lexicographically by inflated-good count and then by length.

Equations

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

theorem Algsuperdiff.Section5.Percolation.exists_preferredPath {Ω : Type u_1} {d k : ℕ} (B : ℕ → Site d → Set Ω) (ω : Ω) (hex : ∃ (Γ : List (Site d)), IsPathFrom k Γ) : ∃ (Γ : List (Site d)), IsPreferredPath B k ω Γ

Whenever a crossing path exists, a lexicographically preferred crossing path exists.

theorem Algsuperdiff.Section5.Percolation.IsPreferredPath.cost_le {Ω : Type u_1} {d k : ℕ} {B : ℕ → Site d → Set Ω} {ω : Ω} {Γ Δ : List (Site d)} (hΓ : IsPreferredPath B k ω Γ) (hΔ : IsPathFrom k Δ) : inflatedGoodVertexCountNat B Γ ω ≤ inflatedGoodVertexCountNat B Δ ω

A preferred path has no greater inflated-good cost than any crossing path.

theorem Algsuperdiff.Section5.Percolation.IsPreferredPath.length_le {Ω : Type u_1} {d k : ℕ} {B : ℕ → Site d → Set Ω} {ω : Ω} {Γ Δ : List (Site d)} (hΓ : IsPreferredPath B k ω Γ) (hΔ : IsPathFrom k Δ) (hcost : inflatedGoodVertexCountNat B Δ ω = inflatedGoodVertexCountNat B Γ ω) : Γ.length ≤ Δ.length

Among crossing paths with the same inflated-good cost, a preferred path has minimal length.

theorem Algsuperdiff.Section5.Percolation.IsPreferredPath.nodup {Ω : Type u_1} {d k : ℕ} {B : ℕ → Site d → Set Ω} {ω : Ω} {Γ : List (Site d)} (hΓ : IsPreferredPath B k ω Γ) : Γ.Nodup

A lexicographically preferred crossing path has no repeated vertices.

noncomputable def Algsuperdiff.Section5.Percolation.pathVerticesInCube {d : ℕ} (L : ℕ) (Γ : List (Site d)) (v : Site d) : Finset (Site d)

The distinct vertices of a path which belong to one centered triadic cube.

Equations

• Algsuperdiff.Section5.Percolation.pathVerticesInCube L Γ v = {z ∈ Γ.toFinset | z ∈ Algsuperdiff.Section5.Percolation.latticeCubeSites L v}

noncomputable def Algsuperdiff.Section5.Percolation.cubeVisitIndices {d : ℕ} (L : ℕ) (Γ : List (Site d)) (v : Site d) : Finset (Fin Γ.length)

The positions along a path whose vertices lie in the specified lattice cube.

Equations

• Algsuperdiff.Section5.Percolation.cubeVisitIndices L Γ v = {i : Fin Γ.length | Γ.get i ∈ Algsuperdiff.Section5.Percolation.latticeCubeSites L v}

theorem Algsuperdiff.Section5.Percolation.IsPreferredPath.card_pathVerticesInCube_le {Ω : Type u_1} {d k L : ℕ} {B : ℕ → Site d → Set Ω} {v : Site d} {ω : Ω} {Γ : List (Site d)} (hΓ : IsPreferredPath B k ω Γ) (hω : ω ∈ inflatedBadEvent B L v) : (pathVerticesInCube L Γ v).card ≤ 3 ^ L + 1

A preferred path visits at most 3^L + 1 distinct sites of any occurring inflated bad cube.

noncomputable def Algsuperdiff.Section5.Percolation.inflatedBadVertices {Ω : Type u_1} {d : ℕ} (B : ℕ → Site d → Set Ω) (Γ : List (Site d)) (ω : Ω) : Finset (Site d)

The vertices of Γ at which the all-scale inflated bad event occurs.

Equations

• Algsuperdiff.Section5.Percolation.inflatedBadVertices B Γ ω = {z ∈ Γ.toFinset | ω ∈ Algsuperdiff.Section5.Percolation.inflatedBadSet B z}

theorem Algsuperdiff.Section5.Percolation.inflatedVertexCount_eq_card_inflatedBadVertices {Ω : Type u_1} {d : ℕ} (B : ℕ → Site d → Set Ω) (Γ : List (Site d)) (ω : Ω) : inflatedVertexCount B Γ ω = ↑(inflatedBadVertices B Γ ω).card

The real inflated-vertex count is the cardinality of the corresponding finite vertex set.

theorem Algsuperdiff.Section5.Percolation.inflatedGoodVertexCountNat_add_inflatedVertexCount_eq_card {Ω : Type u_1} {d : ℕ} (B : ℕ → Site d → Set Ω) (Γ : List (Site d)) (ω : Ω) : ↑(inflatedGoodVertexCountNat B Γ ω) + inflatedVertexCount B Γ ω = ↑Γ.toFinset.card

The inflated-good and inflated-bad vertex counts partition the distinct vertices of a path.

theorem Algsuperdiff.Section5.Percolation.coe_inflatedGoodVertexCountNat_le_goodVertexCount {Ω : Type u_1} {d : ℕ} (B : ℕ → Site d → Set Ω) (Γ : List (Site d)) (ω : Ω) : ↑(inflatedGoodVertexCountNat B Γ ω) ≤ goodVertexCount B Γ ω

The inflated-good count is no larger than the original good-vertex count.

theorem Algsuperdiff.Section5.Percolation.IsPreferredPath.mem_weightedCubeEvent_of_competitor_goodVertexCount_lt {Ω : Type u_1} {d k m : ℕ} {B : ℕ → Site d → Set Ω} {lam : ℝ} {ω : Ω} {Γ Δ : List (Site d)} (hΓ : IsPreferredPath B k ω Γ) (hΔ : IsPathFrom k Δ) (hlen : Γ.length = 3 ^ k + m) (hgood : goodVertexCount B Δ ω < (1 - lam) * 3 ^ k) : ω ∈ weightedCubeEvent B Γ ((lam * 3 ^ k + ↑m) / 2)

A preferred path inherits the weighted inflated-cube threshold from any light crossing path at the same outcome.