PolarCover.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

Polar covers from arbitrary uniform approximation lists

The functions on the approximation list need not be column combinations. For every nonempty coefficient fiber we choose an actual vector in the coefficient ball; empty fibers receive zero. The resulting list has exactly the original number of slots, with no factor depending on the dimension.

def OAI.MetricEntropyDuality.coefficientRepresentative line 29
Source documentation
An actual coefficient vector in the fiber of a list function, or zero when this fiber is empty. No inverse of the column-combination map is used.
```
def coefficientRepresentative (g : Y → X → ℝ) (ε : ℝ) (f : RealSpace X) :
    RealSpace Y := by
…
```
Mentions: OAI.MetricEntropyDuality.RealSpace
theorem OAI.MetricEntropyDuality.coefficientRepresentative_mem line 35
theorem OAI.MetricEntropyDuality.coefficientRepresentative_close line 43
theorem OAI.MetricEntropyDuality.UniformClose.of_same_center line 51
Source documentation
Two functions within the same error of one arbitrary center are within twice that error of each other.
```
theorem UniformClose.of_same_center {ε : ℝ} {f h r : RealSpace X}
    (hf : UniformClose ε f h) (hr : UniformClose ε r h) :
    UniformClose (2 * ε) f r := by
…
```
Mentions: OAI.MetricEntropyDuality.RealSpace, OAI.MetricEntropyDuality.UniformClose
theorem OAI.MetricEntropyDuality.UniformApproximation.nonempty line 62
Source documentation
The approximation hypothesis itself rules out an empty list, since the coefficient ball always contains zero.
```
theorem UniformApproximation.nonempty {g : Y → X → ℝ} {ε : ℝ}
    {A : Finset (RealSpace X)} (hA : UniformApproximation g ε A) : A.Nonempty := by
…
```
Mentions: OAI.MetricEntropyDuality.RealSpace, OAI.MetricEntropyDuality.UniformApproximation
theorem OAI.MetricEntropyDuality.exists_coefficient_representatives line 70
Source documentation
Choose one actual coefficient-ball representative for each original list slot. Every coefficient vector is close to one such representative both after the column map and in the coefficient ℓ¹ norm.
```
theorem exists_coefficient_representatives (g : Y → X → ℝ) (ε : ℝ)
    (A : Finset (RealSpace X)) (hA : UniformApproximation g ε A) :
    ∃ centers : Fin A.card → RealSpace Y,
      (∀ j, centers j ∈ l1Ball Y) ∧
      ∀ lam ∈ l1Ball Y, ∃ j,
        UniformClose (2 * ε) (columnCombination g lam) (columnCombination g (centers j)) ∧
        l1Norm (lam - centers j) ≤ 2 := by
…
```
Mentions: OAI.MetricEntropyDuality.RealSpace, OAI.MetricEntropyDuality.UniformApproximation, OAI.MetricEntropyDuality.l1Ball, OAI.MetricEntropyDuality.UniformClose, OAI.MetricEntropyDuality.columnCombination, OAI.MetricEntropyDuality.l1Norm
theorem OAI.MetricEntropyDuality.exists_l1Ball_polar_cover line 101
Source documentation
The selected coefficient vectors give an actual ambient translate cover of the whole coefficient ball at the specified polar scale.
```
theorem exists_l1Ball_polar_cover (g : Y → X → ℝ) {ε t : ℝ}
    (hε : 0 ≤ ε) (ht : 0 < t) (A : Finset (RealSpace X))
    (hA : UniformApproximation g ε A) :
    ∃ centers : Fin A.card → RealSpace Y,
      (∀ j, centers j ∈ l1Ball Y) ∧
      Covers (l1Ball Y) ((6 * ε + 2 * t) • polar (matrixBody g t)) centers := by
…
```
Mentions: OAI.MetricEntropyDuality.RealSpace, OAI.MetricEntropyDuality.UniformApproximation, OAI.MetricEntropyDuality.l1Ball, OAI.MetricEntropyDuality.Covers, OAI.MetricEntropyDuality.polar, OAI.MetricEntropyDuality.matrixBody
theorem OAI.MetricEntropyDuality.exists_cube_polar_cover line 118
Source documentation
The same explicit finite list covers the literal polar of the cube.
```
theorem exists_cube_polar_cover (g : Y → X → ℝ) {ε t : ℝ}
    (hε : 0 ≤ ε) (ht : 0 < t) (A : Finset (RealSpace X))
    (hA : UniformApproximation g ε A) :
    ∃ centers : Fin A.card → RealSpace Y,
      (∀ j, centers j ∈ l1Ball Y) ∧
      Covers (polar (cube Y)) ((6 * ε + 2 * t) • polar (matrixBody g t)) centers := by
…
```
Mentions: OAI.MetricEntropyDuality.RealSpace, OAI.MetricEntropyDuality.UniformApproximation, OAI.MetricEntropyDuality.l1Ball, OAI.MetricEntropyDuality.Covers, OAI.MetricEntropyDuality.polar, OAI.MetricEntropyDuality.cube, OAI.MetricEntropyDuality.matrixBody
theorem OAI.MetricEntropyDuality.cube_polar_coverable line 128
Source documentation
Finiteness is supplied by an actual list, independently of the convention used for an empty natural infimum in the covering-number definition.
```
theorem cube_polar_coverable (g : Y → X → ℝ) {ε t : ℝ}
    (hε : 0 ≤ ε) (ht : 0 < t) (A : Finset (RealSpace X))
    (hA : UniformApproximation g ε A) :
    Coverable (polar (cube Y)) ((6 * ε + 2 * t) • polar (matrixBody g t)) := by
…
```
Mentions: OAI.MetricEntropyDuality.RealSpace, OAI.MetricEntropyDuality.UniformApproximation, OAI.MetricEntropyDuality.Coverable, OAI.MetricEntropyDuality.polar, OAI.MetricEntropyDuality.cube, OAI.MetricEntropyDuality.matrixBody
theorem OAI.MetricEntropyDuality.polar_coveringNumber_le line 137
Source documentation
The least number of arbitrary ambient translates is bounded by the original approximation-list cardinal, without a dimension or center factor.
```
theorem polar_coveringNumber_le (g : Y → X → ℝ) {ε t : ℝ}
    (hε : 0 ≤ ε) (ht : 0 < t) (A : Finset (RealSpace X))
    (hA : UniformApproximation g ε A) :
    coveringNumber (polar (cube Y)) ((6 * ε + 2 * t) • polar (matrixBody g t)) ≤ A.card := by
…
```
Mentions: OAI.MetricEntropyDuality.RealSpace, OAI.MetricEntropyDuality.UniformApproximation, OAI.MetricEntropyDuality.coveringNumber, OAI.MetricEntropyDuality.polar, OAI.MetricEntropyDuality.cube, OAI.MetricEntropyDuality.matrixBody