GraphProfile.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

The actual logarithmic graph matrix

Columns retain both their vertex and their admissible partition set. The graph metric takes values in ENat, so disconnected vertices have profile zero. The row separation proof uses an actual coordinate of this matrix; the finite field construction supplies its graph-separation hypothesis separately.

abbrev OAI.MetricEntropyDuality.GraphProfile.Columns line 28
Source documentation
Actual column indices, including the choice of partition graph.
```
abbrev Columns (X : Type uX) (𝒯 : Finset (Finset ι)) :=
…
```
def OAI.MetricEntropyDuality.GraphProfile.column line 32
Source documentation
The graph-distance column function.
```
def column (L : (i : ι) → X → Label i) (𝒯 : Finset (Finset ι)) (h : ℕ)
    (y : Columns X 𝒯) (x : X) : ℝ :=
…
```
Mentions: OAI.MetricEntropyDuality.GraphProfile.Columns
def OAI.MetricEntropyDuality.GraphProfile.row line 37
Source documentation
The actual row vector has one coordinate for every actual column.
```
def row (L : (i : ι) → X → Label i) (𝒯 : Finset (Finset ι)) (h : ℕ)
    (x : X) : Columns X 𝒯 → ℝ := fun y => column L 𝒯 h y x
```
Mentions: OAI.MetricEntropyDuality.GraphProfile.Columns, OAI.MetricEntropyDuality.GraphProfile.column
theorem OAI.MetricEntropyDuality.GraphProfile.column_nonneg line 40
theorem OAI.MetricEntropyDuality.GraphProfile.column_le_one line 45
theorem OAI.MetricEntropyDuality.GraphProfile.column_self line 50
theorem OAI.MetricEntropyDuality.GraphProfile.column_eq_zero_of_le line 57
theorem OAI.MetricEntropyDuality.GraphProfile.column_eq_sum line 65
Source documentation
Exact finite-ball expansion, with no finite-distance assumption.
```
theorem column_eq_sum (L : (i : ι) → X → Label i) (𝒯 : Finset (Finset ι))
    {h : ℕ} (hh : 0 < h) (y : Columns X 𝒯) (x : X) :
    column L 𝒯 h y x = ∑ j ∈ Finset.range h,
      if PartitionGraph.distance L y.2.val x y.1 ≤ (j : ℕ∞)
      then LogProfile.gamma h j else 0 :=
…
```
Mentions: OAI.MetricEntropyDuality.GraphProfile.Columns, OAI.MetricEntropyDuality.GraphProfile.column, OAI.MetricEntropyDuality.PartitionGraph.distance, OAI.MetricEntropyDuality.LogProfile.gamma
theorem OAI.MetricEntropyDuality.GraphProfile.exists_column_abs_eq_one line 73
Source documentation
The concrete coordinate witness consumed by the convex-body construction.
```
theorem exists_column_abs_eq_one (L : (i : ι) → X → Label i)
    (𝒯 : Finset (Finset ι)) {h : ℕ} (hh : 0 < h) (x z : X)
    (hsep : ∃ T ∈ 𝒯, (h : ℕ∞) < PartitionGraph.distance L T x z) :
    ∃ y : Columns X 𝒯, |column L 𝒯 h y x - column L 𝒯 h y z| = 1 := by
…
```
Mentions: OAI.MetricEntropyDuality.PartitionGraph.distance, OAI.MetricEntropyDuality.GraphProfile.Columns, OAI.MetricEntropyDuality.GraphProfile.column
theorem OAI.MetricEntropyDuality.GraphProfile.abs_row_sub_le_one line 89
Source documentation
All row coordinates lie in the common unit interval.
```
theorem abs_row_sub_le_one (L : (i : ι) → X → Label i)
    (𝒯 : Finset (Finset ι)) {h : ℕ} (hh : 0 < h)
    (x z : X) (y : Columns X 𝒯) :
    |row L 𝒯 h x y - row L 𝒯 h z y| ≤ 1 := by
…
```
Mentions: OAI.MetricEntropyDuality.GraphProfile.Columns, OAI.MetricEntropyDuality.GraphProfile.row
theorem OAI.MetricEntropyDuality.GraphProfile.norm_row_sub_eq_one line 102
Source documentation
The column (x,T) certifies exact unit separation, including when the chosen graph disconnects x from z.
```
theorem norm_row_sub_eq_one [Fintype X]
    (L : (i : ι) → X → Label i) (𝒯 : Finset (Finset ι))
    {h : ℕ} (hh : 0 < h) (x z : X)
    (hsep : ∃ T ∈ 𝒯, (h : ℕ∞) < PartitionGraph.distance L T x z) :
    ‖row L 𝒯 h x - row L 𝒯 h z‖ = 1 := by
…
```
Mentions: OAI.MetricEntropyDuality.PartitionGraph.distance, OAI.MetricEntropyDuality.GraphProfile.row

theorem OAI.MetricEntropyDuality.GraphProfile.dist_row_eq_one line 127

Source documentation

The norm equality also gives the usual finite-product metric equality.

theorem dist_row_eq_one [Fintype X]
    (L : (i : ι) → X → Label i) (𝒯 : Finset (Finset ι))
    {h : ℕ} (hh : 0 < h) (x z : X)
    (hsep : ∃ T ∈ 𝒯, (h : ℕ∞) < PartitionGraph.distance L T x z) :
    dist (row L 𝒯 h x) (row L 𝒯 h z) = 1 := by
…

Mentions: OAI.MetricEntropyDuality.PartitionGraph.distance, OAI.MetricEntropyDuality.GraphProfile.row