Flips and flip metrics
Lax185574.Flips Β· concepts/Lax185574/Flips.lean Β· lax-185574
No public endorsements yet.
Loading reviewβ¦
Sign in with ORCIDNatural Language Statement
Definition
For a graph G and a partition π« of V β V(G), a π«-flip of G is a graph H with V(H) = V such that for every pair X, Y β π« (possibly X = Y), either H[X, Y] = G[X, Y] or H[X, Y] = αΈ [X, Y]. If |π«| β€ s, then H is an s-flip of G. The associated flip metric and its balls are
dist_π«(u, v) β max { dist^H(u, v) : H is a π«-flip of G }, Ball^π«_r(v) β { u : dist_π«(u, v) β€ r } = β { Ball^H_r(v) : H is a π«-flip of G }.
As a shorthand, for a graph G and a set S β V(G), a π«S-flip of G is called an S-flip, and dist_S^G β dist{π«_S} and Ball^S_r β Ball^{π«_S}_r. Here π«_S is the partition into atomic types over S, see and .
Concept map
In the paper
- page 14 of this submission's paper
Lean source view on GitHub
| 1 | import Lax185574.Partitions |
| 2 | import Lax185574.GaifmanGraph |
| 3 | |
| 4 | /-! |
| 5 | --- |
| 6 | title: Flips and flip metrics |
| 7 | type: definition |
| 8 | --- |
| 9 | For a graph G and a partition π« of V β V(G), a *π«-flip* of G is a graph |
| 10 | H with V(H) = V such that for every pair X, Y β π« (possibly X = Y), |
| 11 | either H[X, Y] = G[X, Y] or H[X, Y] = αΈ [X, Y]. If |π«| β€ s, then H is |
| 12 | an *s-flip* of G. The associated *flip metric* and its balls are |
| 13 | |
| 14 | dist_π«(u, v) β max { dist^H(u, v) : H is a π«-flip of G }, |
| 15 | Ball^π«_r(v) β { u : dist_π«(u, v) β€ r } = β { Ball^H_r(v) : H is a π«-flip of G }. |
| 16 | |
| 17 | As a shorthand, for a graph G and a set S β V(G), a π«_S-flip of G is |
| 18 | called an *S-flip*, and dist_S^G β dist_{π«_S} and Ball^S_r β Ball^{π«_S}_r. |
| 19 | Here π«_S is the partition into atomic types over S, see |
| 20 | `Lax185574.AtomicTypes` and `Lax185574.Partitions`. |
| 21 | |
| 22 | # Formalization notes |
| 23 | |
| 24 | "H[X, Y] = G[X, Y] or H[X, Y] = αΈ [X, Y]" says that on all pairs of |
| 25 | distinct vertices x β X, y β Y, adjacency in H agrees with adjacency in |
| 26 | G, or on all of them it agrees with non-adjacency in G. For X = Y this |
| 27 | reads H[X] = G[X] or H[X] = αΈ [X], which is the intended meaning. The |
| 28 | parts X and Y are named by vertices a and b with X = π«(a) and Y = π«(b). |
| 29 | |
| 30 | The bound dist_π«(u, v) β€ r is `FlipWithinDist`: in every π«-flip, some |
| 31 | walk from u to v has length at most r. Distances are measured by walks, |
| 32 | as in `Lax185574.GaifmanGraph`, so the maximum of the paper is never |
| 33 | needed as a number, and an infinite distance in some flip is allowed. |
| 34 | The ball is the set of vertices u with dist_π«(v, u) β€ r, which is the |
| 35 | intersection form of the paper. The ball Ball^S_r(v) is |
| 36 | `flipBall G (atomicTypes G S) r v` and gets no separate name. An s-flip |
| 37 | is a π«-flip with `Nat.card (Quotient π«) β€ s`, which is spelled out where |
| 38 | it is used. |
| 39 | -/ |
| 40 | |
| 41 | namespace Lax185574.Flips |
| 42 | |
| 43 | open Lax185574.Partitions Lax185574.GaifmanGraph |
| 44 | |
| 45 | universe z |
| 46 | |
| 47 | variable {V : Type z} |
| 48 | |
| 49 | /-- `H` is a `π«`-flip of `G`: for every pair of parts `π«(a)`, `π«(b)`, |
| 50 | adjacency in `H` between distinct vertices of these parts either agrees |
| 51 | with adjacency in `G` throughout, or with non-adjacency in `G` |
| 52 | throughout. -/ |
| 53 | def IsFlip (G : SimpleGraph V) (P : Setoid V) (H : SimpleGraph V) : Prop := |
| 54 | β a b : V, |
| 55 | (β x y : V, P x a β P y b β x β y β (H.Adj x y β G.Adj x y)) β¨ |
| 56 | (β x y : V, P x a β P y b β x β y β (H.Adj x y β Β¬ G.Adj x y)) |
| 57 | |
| 58 | /-- `dist_π«(u, v) β€ r`: in every `π«`-flip of `G`, some walk from `u` |
| 59 | to `v` has length at most `r`. -/ |
| 60 | def FlipWithinDist (G : SimpleGraph V) (P : Setoid V) (r : β) (u v : V) : Prop := |
| 61 | β H : SimpleGraph V, IsFlip G P H β WithinDist H r u v |
| 62 | |
| 63 | /-- `Ball^π«_r(v)`: the vertices within distance `r` of `v` in every |
| 64 | `π«`-flip of `G`. -/ |
| 65 | def flipBall (G : SimpleGraph V) (P : Setoid V) (r : β) (v : V) : Set V := |
| 66 | {u | FlipWithinDist G P r v u} |
| 67 | |
| 68 | end Lax185574.Flips |
| 69 |
Formalization notes
"H[X, Y] = G[X, Y] or H[X, Y] = αΈ [X, Y]" says that on all pairs of distinct vertices x β X, y β Y, adjacency in H agrees with adjacency in G, or on all of them it agrees with non-adjacency in G. For X = Y this reads H[X] = G[X] or H[X] = αΈ [X], which is the intended meaning. The parts X and Y are named by vertices a and b with X = π«(a) and Y = π«(b).
The bound dist_π«(u, v) β€ r is : in every π«-flip, some walk from u to v has length at most r. Distances are measured by walks, as in , so the maximum of the paper is never needed as a number, and an infinite distance in some flip is allowed. The ball is the set of vertices u with dist_π«(v, u) β€ r, which is the intersection form of the paper. The ball Ball^S_r(v) is and gets no separate name. An s-flip is a π«-flip with , which is spelled out where it is used.
Used by
From Mathlib
none
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments