SignedCompression.lean`

18 declarations, 0 contain sorry, 0 declared as axioms

Signed compression and actual coefficient-ball clusters

A common finite approximation list for nonnegative combinations of mass at most one gives a difference list for the literal l1Ball. A chosen pair of positive approximants labels each actual coefficient vector; equal labels give a uniform diameter bound. The list may have centers outside the column hull, while the fibers consist of actual coefficient vectors.

def OAI.MetricEntropyDuality.SignedCompression.positivePart line 27
def OAI.MetricEntropyDuality.SignedCompression.negativePart line 29
theorem OAI.MetricEntropyDuality.SignedCompression.positivePart_nonneg line 32
theorem OAI.MetricEntropyDuality.SignedCompression.negativePart_nonneg line 36
theorem OAI.MetricEntropyDuality.SignedCompression.parts_sub line 40
theorem OAI.MetricEntropyDuality.SignedCompression.sum_positivePart_le_one line 48
theorem OAI.MetricEntropyDuality.SignedCompression.sum_negativePart_le_one line 57
theorem OAI.MetricEntropyDuality.SignedCompression.sub_close line 66
def OAI.MetricEntropyDuality.SignedCompression.differenceList line 79
Source documentation
The literal difference list, including any duplicated outputs only once.
```
def differenceList (A : Finset (RealSpace X)) : Finset (RealSpace X) := by
…
```
Mentions: OAI.MetricEntropyDuality.RealSpace
theorem OAI.MetricEntropyDuality.SignedCompression.differenceList_card_le line 83
abbrev OAI.MetricEntropyDuality.SignedCompression.Code line 91
Source documentation
A pair of members of the positive approximation list.
```
abbrev Code (A : Finset (RealSpace X)) := {a // a ∈ A} × {a // a ∈ A}
```
Mentions: OAI.MetricEntropyDuality.RealSpace
def OAI.MetricEntropyDuality.SignedCompression.decode line 93
theorem OAI.MetricEntropyDuality.SignedCompression.card_code line 96
theorem OAI.MetricEntropyDuality.SignedCompression.decode_mem_differenceList line 101
def OAI.MetricEntropyDuality.SignedCompression.PositiveApproximation line 110
Source documentation
The positive compression premise, stated on the actual coefficients.
```
def PositiveApproximation : Prop :=
…
```
theorem OAI.MetricEntropyDuality.SignedCompression.exists_code_approximation line 114
theorem OAI.MetricEntropyDuality.SignedCompression.uniformApproximation line 129
Source documentation
Signed combinations are approximated by the actual finite difference list.
```
theorem uniformApproximation (hpos : PositiveApproximation g θ A) :
    UniformApproximation g (6 * θ) (differenceList A) := by
…
```
Mentions: OAI.MetricEntropyDuality.SignedCompression.PositiveApproximation, OAI.MetricEntropyDuality.UniformApproximation, OAI.MetricEntropyDuality.SignedCompression.differenceList
theorem OAI.MetricEntropyDuality.SignedCompression.exists_code line 137
Source documentation
Every coefficient vector receives a finite pair code. Its nonempty fibers form clusters of actual vectors in the coefficient ball, with diameter 12θ.
```
theorem exists_code (hpos : PositiveApproximation g θ A) :
    ∃ c : l1Ball Y → Code A,
      (∀ lam, UniformClose (6 * θ) (columnCombination g lam.val) (decode (c lam))) ∧
      ∀ lam lam', c lam = c lam' →
        UniformClose (12 * θ) (columnCombination g lam.val) (columnCombination g lam'.val) := by
…
```
Mentions: OAI.MetricEntropyDuality.SignedCompression.PositiveApproximation, OAI.MetricEntropyDuality.l1Ball, OAI.MetricEntropyDuality.SignedCompression.Code, OAI.MetricEntropyDuality.UniformClose, OAI.MetricEntropyDuality.columnCombination, OAI.MetricEntropyDuality.SignedCompression.decode