MatrixToBody.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

The actual matrix-to-body conversion

The separated points are the actual three-times-scaled rows. The primal minimum has a finite-cover witness from compactness, and the dual cover has actual coefficient-ball centers with exactly the approximation-list count. The final wrapper uses a coordinate linear homeomorphism to obtain Fin n.

theorem OAI.MetricEntropyDuality.matrixBody_primal_lower line 28
Source documentation
A separated row family supplies the exact primal packing lower bound.
```
theorem matrixBody_primal_lower (g : Y → X → ℝ) (t : ℝ)
    (hsep : ∀ x x', x ≠ x' → ∃ y, 1 ≤ |g y x - g y x'|) :
    Fintype.card X ≤ coveringNumber (matrixBody g t) (cube Y) := by
…
```
Mentions: OAI.MetricEntropyDuality.coveringNumber, OAI.MetricEntropyDuality.matrixBody, OAI.MetricEntropyDuality.cube
theorem OAI.MetricEntropyDuality.smul_polar_mono line 43
Source documentation
Increasing a positive polar scale increases the actual covering body.
```
theorem smul_polar_mono {ι : Type uι} [Fintype ι]
    (K : Set (RealSpace ι)) {c d : ℝ} (hc : 0 < c) (hcd : c ≤ d) :
    c • polar K ⊆ d • polar K := by
…
```
Mentions: OAI.MetricEntropyDuality.RealSpace, OAI.MetricEntropyDuality.polar

theorem OAI.MetricEntropyDuality.polar_cover_enlarge line 52

Source documentation

The same finite polar cover is valid at every larger positive scale.

theorem polar_cover_enlarge {ι : Type uι} [Fintype ι]
    (K : Set (RealSpace ι)) {c d : ℝ} (hc : 0 < c) (hcd : c ≤ d)
    (hfin : Coverable (polar (cube ι)) (c • polar K)) :
    Coverable (polar (cube ι)) (d • polar K) ∧
      coveringNumber (polar (cube ι)) (d • polar K) ≤
        coveringNumber (polar (cube ι)) (c • polar K) := by
…

Mentions: OAI.MetricEntropyDuality.RealSpace, OAI.MetricEntropyDuality.Coverable, OAI.MetricEntropyDuality.polar, OAI.MetricEntropyDuality.cube, OAI.MetricEntropyDuality.coveringNumber

theorem OAI.MetricEntropyDuality.matrix_to_body line 63

Source documentation

Complete geometric conversion for actual real columns. No compactness, support, polar-cover, or covering-minimum hypothesis is assumed.

theorem matrix_to_body [Nonempty X] (g : Y → X → ℝ) {ε t : ℝ}
    (hε : 0 ≤ ε) (ht : 0 < t)
    (hsep : ∀ x x', x ≠ x' → ∃ y, 1 ≤ |g y x - g y x'|)
    (A : Finset (RealSpace X)) (hA : UniformApproximation g ε A) :
    IsSymmetricConvexBody (matrixBody g t) ∧
      IsSymmetricConvexBody (cube Y) ∧
      Coverable (matrixBody g t) (cube Y) ∧
      Coverable (polar (cube Y)) ((6 * ε + 2 * t) • polar (matrixBody g t)) ∧
      Fintype.card X ≤ coveringNumber (matrixBody g t) (cube Y) ∧
      coveringNumber (polar (cube Y))
        ((6 * ε + 2 * t) • polar (matrixBody g t)) ≤ A.card := by
…

Mentions: OAI.MetricEntropyDuality.RealSpace, OAI.MetricEntropyDuality.UniformApproximation, OAI.MetricEntropyDuality.IsSymmetricConvexBody, OAI.MetricEntropyDuality.matrixBody, OAI.MetricEntropyDuality.cube, OAI.MetricEntropyDuality.Coverable, OAI.MetricEntropyDuality.polar, OAI.MetricEntropyDuality.coveringNumber

theorem OAI.MetricEntropyDuality.matrix_to_body_fin line 81

Source documentation

The actual geometric conversion in the ordinary positive dimension card Y, with all covering centers transported in the same ambient space.

theorem matrix_to_body_fin [Nonempty X] [Nonempty Y]
    (g : Y → X → ℝ) {ε t : ℝ} (hε : 0 ≤ ε) (ht : 0 < t)
    (hsep : ∀ x x', x ≠ x' → ∃ y, 1 ≤ |g y x - g y x'|)
    (A : Finset (RealSpace X)) (hA : UniformApproximation g ε A) :
    0 < Fintype.card Y ∧
      ∃ K : Set (RealSpace (Fin (Fintype.card Y))),
        IsSymmetricConvexBody K ∧
        IsSymmetricConvexBody (cube (Fin (Fintype.card Y))) ∧
        Coverable K (cube (Fin (Fintype.card Y))) ∧
        Coverable (polar (cube (Fin (Fintype.card Y)))) ((6 * ε + 2 * t) • polar K) ∧
        Fintype.card X ≤ coveringNumber K (cube (Fin (Fintype.card Y))) ∧
        coveringNumber (polar (cube (Fin (Fintype.card Y))))
…

Mentions: OAI.MetricEntropyDuality.RealSpace, OAI.MetricEntropyDuality.UniformApproximation, OAI.MetricEntropyDuality.IsSymmetricConvexBody, OAI.MetricEntropyDuality.cube, OAI.MetricEntropyDuality.Coverable, OAI.MetricEntropyDuality.polar, OAI.MetricEntropyDuality.coveringNumber