The Observation Theory EncyclopediaFrom TSKAboutBy kindBy chapterBy Lean fileLedgerProvenance

graph concept

DefinitionA set of nodes and a set of edges joining pairs of them. A neighbourhood graph joins each row of a dataset to its nearest rows. Chapter 0 section 0.10.
ExampleFour nodes joined in a square have four edges, and every node has degree 2.
BookData Mining as Observation, draft 0.2, commit f3914f0; entry id graph, kind concept.
Statusno ledger row names this entry. Corrections: none recorded.
Defining equation

Book equation 0.19.

Assumptions and scope
  • A set of nodes and a set of edges joining pairs of them. A neighbourhood graph joins each row to its k nearest rows, so every node has exactly k out-neighbours. The mutual form keeps an edge only when each node is among the other’s neighbours, is symmetric, is a subgraph of the directed form, and gives no node more than k mutual neighbours.
  • The Laplacian of the graph carries the dimension in its eigenvalue count and the geodesic ranking in its low eigenvectors’ angles, which is what chapters 3 and 9 read.
Prior artnone recorded
Evidencelean/DataMiningAsObservation/Graph.lean
Reviewednot yet reviewed; generated 2026-09-10 from records at the commits on the provenance page.
Nodes and the edges that join pairs of them.

Equation

Book equation 0.19.

\[L=I-D^{-1/2}AD^{-1/2},\qquad D=\operatorname{diag}(d_1,\dots,d_n),\qquad L\,u_k=\lambda_k u_k,\ \ 0=\lambda_1\le\lambda_2\le\cdots.\]

Book equation 0.20.

\[\Psi_i=\left(\frac{u_k(i)}{\sqrt{\lambda_k\,d_i}}\right)_{k\ge2},\qquad \|\Psi_i-\Psi_j\|^{2}=R(i,j)=\frac{C(i,j)}{\operatorname{vol}(G)}.\]

Conditions

Conditions are curated in entries.toml rather than read from a record.

Ledger

none

First stated

Chapter 0 section 0.10 of Data Mining as Observation, with the neighbourhood graphs of the-angular-observer and the recognizer battery.

Measurements

none

Failures and corrections

none

Invariance envelope

none declared

Machine checked

lean/DataMiningAsObservation/Graph.lean, theorems outDegree, mutual_symm, mutual_sub, mutualNbrs_card_le, mem_mutualNbrs, at observation-data-mining f3914f0; what the check covers is stated in the book’s appendix C.

Used in

Data Mining as Observation primer L, chapters 0, 3, 9, 10, 11.

Related

degree; Laplacian; geodesic distance; spectral embedding; manifold.

See also

Ledger rows that cite the entry’s records without naming it: GO-3, NEG-1.

Sources-table rows that share a record with the entry without naming it: chapter 3 section 3.2, chapter 3 section 3.3, chapter 9 section 9.1, chapter 9 section 9.2, chapter 11 section 11.1.

Status

Generated 2026-09-10 by encyclopedia/generate.py; book at observation-data-mining f3914f0; the commit of every record is listed in the encyclopedia’s provenance.

← Gram and Schmidtharness →