CoordinateTransport.lean`

29 declarations, 0 contain sorry, 0 declared as axioms

Relabelling finite real coordinates

The coordinate map is a linear homeomorphism of the full ambient spaces. It transports all translation centers, rather than restricting them to the body being covered. Consequently equality of covering numbers follows from equality of the sets of admissible natural cover counts.

def OAI.MetricEntropyDuality.coordinateEquiv line 30
Source documentation
Relabel coordinates using e; no coordinate is removed or adjoined.
```
def coordinateEquiv (e : ι ≃ κ) : (ι → ℝ) ≃L[ℝ] (κ → ℝ) where
…
```
theorem OAI.MetricEntropyDuality.coordinateEquiv_apply line 40
theorem OAI.MetricEntropyDuality.coordinateEquiv_symm_apply line 43
theorem OAI.MetricEntropyDuality.coordinateEquiv_symm line 46
theorem OAI.MetricEntropyDuality.coordinate_image_smul line 51
theorem OAI.MetricEntropyDuality.coordinate_isCompact_image line 55
theorem OAI.MetricEntropyDuality.coordinate_convex_image line 59
theorem OAI.MetricEntropyDuality.coordinate_interior_nonempty line 70
Source documentation
This is interior in the full ambient function space.
```
theorem coordinate_interior_nonempty (e : ι ≃ κ) (A : Set (ι → ℝ)) :
    (interior (coordinateEquiv e '' A)).Nonempty ↔ (interior A).Nonempty := by
…
```
Mentions: OAI.MetricEntropyDuality.coordinateEquiv
theorem OAI.MetricEntropyDuality.mem_coordinate_image_iff line 77
theorem OAI.MetricEntropyDuality.covers_coordinate_image line 89
Source documentation
Arbitrary ambient center lists are carried to arbitrary ambient center lists. No requirement that centers belong to either covered set is added.
```
theorem covers_coordinate_image (e : ι ≃ κ) {M : ℕ}
    (A B : Set (RealSpace ι)) (c : Fin M → RealSpace ι) :
    Covers (coordinateEquiv e '' A) (coordinateEquiv e '' B)
      (fun j => coordinateEquiv e (c j)) ↔ Covers A B c := by
…
```
Mentions: OAI.MetricEntropyDuality.RealSpace, OAI.MetricEntropyDuality.Covers, OAI.MetricEntropyDuality.coordinateEquiv
theorem OAI.MetricEntropyDuality.exists_cover_coordinate_image line 104
theorem OAI.MetricEntropyDuality.coordinate_cover_counts line 118
theorem OAI.MetricEntropyDuality.coverable_coordinate_image line 125
theorem OAI.MetricEntropyDuality.coveringNumber_coordinate_image line 132
Source documentation
Equality holds even before existence of a finite cover is established: the two defining sets of natural counts are literally equal.
```
theorem coveringNumber_coordinate_image (e : ι ≃ κ) (A B : Set (RealSpace ι)) :
    coveringNumber (coordinateEquiv e '' A) (coordinateEquiv e '' B) =
      coveringNumber A B := by
…
```
Mentions: OAI.MetricEntropyDuality.RealSpace, OAI.MetricEntropyDuality.coveringNumber, OAI.MetricEntropyDuality.coordinateEquiv
theorem OAI.MetricEntropyDuality.coordinate_cube line 138
theorem OAI.MetricEntropyDuality.pairing_coordinateEquiv line 153
theorem OAI.MetricEntropyDuality.l1Norm_coordinateEquiv line 158
theorem OAI.MetricEntropyDuality.coordinate_l1Ball line 163
theorem OAI.MetricEntropyDuality.coordinate_polar line 172
Source documentation
Coordinate permutations preserve the literal pairing polar, with both the body and its dual coordinates transported by the same map.
```
theorem coordinate_polar (e : ι ≃ κ) (K : Set (RealSpace ι)) :
    coordinateEquiv e '' polar K = polar (coordinateEquiv e '' K) := by
…
```
Mentions: OAI.MetricEntropyDuality.RealSpace, OAI.MetricEntropyDuality.coordinateEquiv, OAI.MetricEntropyDuality.polar
theorem OAI.MetricEntropyDuality.IsSymmetricConvexBody.coordinate_image line 189
theorem OAI.MetricEntropyDuality.coordinate_body_iff line 199
theorem OAI.MetricEntropyDuality.coveringNumber_polar_cube_coordinate_image line 209
Source documentation
The exact dual covering number in the final theorem is unchanged, for every scalar, with no convexity or covering premise needed for transport.
```
theorem coveringNumber_polar_cube_coordinate_image (e : ι ≃ κ)
    (K : Set (RealSpace ι)) (a : ℝ) :
    coveringNumber (polar (cube κ)) (a • polar (coordinateEquiv e '' K)) =
      coveringNumber (polar (cube ι)) (a • polar K) := by
…
```
Mentions: OAI.MetricEntropyDuality.RealSpace, OAI.MetricEntropyDuality.coveringNumber, OAI.MetricEntropyDuality.polar, OAI.MetricEntropyDuality.cube, OAI.MetricEntropyDuality.coordinateEquiv
def OAI.MetricEntropyDuality.coordinatesToFin line 221
Source documentation
The terminal ambient-space identification is a genuine linear homeomorphism, not a cardinality-only relabelling.
```
def coordinatesToFin [Fintype ι] : (ι → ℝ) ≃L[ℝ] (Fin (Fintype.card ι) → ℝ) :=
…
```
theorem OAI.MetricEntropyDuality.coordinate_dimension_pos line 224
theorem OAI.MetricEntropyDuality.coordinatesToFin_cube line 227
theorem OAI.MetricEntropyDuality.coordinatesToFin_body_iff line 231
theorem OAI.MetricEntropyDuality.coordinatesToFin_coveringNumber_cube line 236
theorem OAI.MetricEntropyDuality.coordinatesToFin_coveringNumber_polar_cube line 243

theorem OAI.MetricEntropyDuality.finite_coordinate_realization line 253

Source documentation

A positive ordinary dimension and the exact geometric and covering identities for the coordinate equivalence ℝ^Y ≃ ℝ^n. Every body is transported by one explicit ambient linear homeomorphism.

theorem finite_coordinate_realization [Fintype ι] [Nonempty ι] :
    ∃ n : ℕ, 0 < n ∧ ∃ E : RealSpace ι ≃L[ℝ] RealSpace (Fin n),
      E '' cube ι = cube (Fin n) ∧
      (∀ K : Set (RealSpace ι),
        IsSymmetricConvexBody (E '' K) ↔ IsSymmetricConvexBody K) ∧
      (∀ K : Set (RealSpace ι),
        coveringNumber (E '' K) (cube (Fin n)) = coveringNumber K (cube ι)) ∧
      (∀ (K : Set (RealSpace ι)) (a : ℝ),
        coveringNumber (polar (cube (Fin n))) (a • polar (E '' K)) =
          coveringNumber (polar (cube ι)) (a • polar K)) := by
…

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