CompressionLevels.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

Graph-ball comparison at one compression level

Columns omitted by the common index and retained columns left uncovered each contribute at most θ. Assigned columns are compared using the actual partition graph and replacement pivots with the same selected label. Graph distances remain extended distances throughout.

def OAI.MetricEntropyDuality.CompressionLevels.ballIndicator line 28
Source documentation
The real indicator of a finite-radius ball in the actual partition graph.
```
def ballIndicator (L : (i : ι) → X → Label i) (T : Finset ι) (j : ℕ)
    (x v : X) : ℝ := if PartitionGraph.near L T j x v then 1 else 0
```
Mentions: OAI.MetricEntropyDuality.PartitionGraph.near
theorem OAI.MetricEntropyDuality.CompressionLevels.ballIndicator_nonneg line 31
theorem OAI.MetricEntropyDuality.CompressionLevels.ballIndicator_le_one line 36
def OAI.MetricEntropyDuality.CompressionLevels.assignedIndicator line 42
Source documentation
Unassigned columns contribute zero; assigned columns use replacement pivots.
```
def assignedIndicator (L : (i : ι) → X → Label i) (T : Y → Finset ι)
    (rep : K → X) (assignment : Y → Option K) (j : ℕ) (x : X) (y : Y) : ℝ :=
…
```
theorem OAI.MetricEntropyDuality.CompressionLevels.assignedIndicator_nonneg line 48

theorem OAI.MetricEntropyDuality.CompressionLevels.ballIndicator_le_assignedIndicator_add line 57

Source documentation

Pointwise accounting for assigned, omitted, and uncovered columns.

theorem ballIndicator_le_assignedIndicator_add
    (L : (i : ι) → X → Label i) (v : Y → X) (T : Y → Finset ι)
    (i : ι) (j : ℕ) (centers rep : K → X) (assignment : Y → Option K)
    (hassign : ∀ y k, assignment y = some k →
      i ∈ T y ∧ PartitionGraph.near L (T y) j (centers k) (v y))
    (hrep : ∀ k, L i (rep k) = L i (centers k)) (x : X) (y : Y) :
    ballIndicator L (T y) j x (v y) ≤
      assignedIndicator L T rep assignment j x y +
        (if i ∉ T y then 1 else 0) +
        (if i ∈ T y ∧ PartitionGraph.near L (T y) j x (v y) ∧
          assignment y = none then 1 else 0) := by
…

Mentions: OAI.MetricEntropyDuality.PartitionGraph.near, OAI.MetricEntropyDuality.CompressionLevels.ballIndicator, OAI.MetricEntropyDuality.CompressionLevels.assignedIndicator

theorem OAI.MetricEntropyDuality.CompressionLevels.assignedIndicator_le_ballIndicator line 85

Source documentation

Every assigned replacement ball lies in the original ball of radius 3*j+2.

theorem assignedIndicator_le_ballIndicator
    (L : (i : ι) → X → Label i) (v : Y → X) (T : Y → Finset ι)
    (i : ι) (j : ℕ) (centers rep : K → X) (assignment : Y → Option K)
    (hassign : ∀ y k, assignment y = some k →
      i ∈ T y ∧ PartitionGraph.near L (T y) j (centers k) (v y))
    (hrep : ∀ k, L i (rep k) = L i (centers k)) (x : X) (y : Y) :
    assignedIndicator L T rep assignment j x y ≤
      ballIndicator L (T y) (3 * j + 2) x (v y) := by
…

Mentions: OAI.MetricEntropyDuality.PartitionGraph.near, OAI.MetricEntropyDuality.CompressionLevels.assignedIndicator, OAI.MetricEntropyDuality.CompressionLevels.ballIndicator

def OAI.MetricEntropyDuality.CompressionLevels.levelValue line 111

Source documentation

The original mixture at one ball radius.

def levelValue (L : (i : ι) → X → Label i) (v : Y → X) (T : Y → Finset ι)
    (μ : Y → ℝ) (j : ℕ) (x : X) : ℝ :=
…

def OAI.MetricEntropyDuality.CompressionLevels.assignedValue line 116

Source documentation

The assigned mixture after pivot replacement.

def assignedValue (L : (i : ι) → X → Label i) (T : Y → Finset ι)
    (rep : K → X) (assignment : Y → Option K) (μ : Y → ℝ) (j : ℕ) (x : X) : ℝ :=
…

theorem OAI.MetricEntropyDuality.CompressionLevels.levelValue_sub_two_mul_le_assignedValue line 121

Source documentation

The lower comparison loses only omitted mass and uncovered retained mass.

theorem levelValue_sub_two_mul_le_assignedValue
    (L : (i : ι) → X → Label i) (v : Y → X) (T : Y → Finset ι)
    (μ : Y → ℝ) (hμ : ∀ y, 0 ≤ μ y) (i : ι) (j : ℕ)
    (centers rep : K → X) (assignment : Y → Option K)
    (hassign : ∀ y k, assignment y = some k →
      i ∈ T y ∧ PartitionGraph.near L (T y) j (centers k) (v y))
    (hrep : ∀ k, L i (rep k) = L i (centers k)) {θ : ℝ}
    (homit : (∑ y ∈ Finset.univ.filter (fun y => i ∉ T y), μ y) ≤ θ)
    (hrem : ∀ x, (∑ y ∈ Finset.univ.filter (fun y =>
      i ∈ T y ∧ PartitionGraph.near L (T y) j x (v y) ∧
        assignment y = none), μ y) ≤ θ) (x : X) :
    levelValue L v T μ j x - 2 * θ ≤ assignedValue L T rep assignment μ j x := by
…

Mentions: OAI.MetricEntropyDuality.PartitionGraph.near, OAI.MetricEntropyDuality.CompressionLevels.levelValue, OAI.MetricEntropyDuality.CompressionLevels.assignedValue

theorem OAI.MetricEntropyDuality.CompressionLevels.assignedValue_le_levelValue line 151

Source documentation

The upper comparison uses the genuine radius 3*j+2 in each column graph.

theorem assignedValue_le_levelValue
    (L : (i : ι) → X → Label i) (v : Y → X) (T : Y → Finset ι)
    (μ : Y → ℝ) (hμ : ∀ y, 0 ≤ μ y) (i : ι) (j : ℕ)
    (centers rep : K → X) (assignment : Y → Option K)
    (hassign : ∀ y k, assignment y = some k →
      i ∈ T y ∧ PartitionGraph.near L (T y) j (centers k) (v y))
    (hrep : ∀ k, L i (rep k) = L i (centers k)) (x : X) :
    assignedValue L T rep assignment μ j x ≤ levelValue L v T μ (3 * j + 2) x := by
…

Mentions: OAI.MetricEntropyDuality.PartitionGraph.near, OAI.MetricEntropyDuality.CompressionLevels.assignedValue, OAI.MetricEntropyDuality.CompressionLevels.levelValue