SupportPolar.lean`

23 declarations, 0 contain sorry, 0 declared as axioms

Exact support and polar calculations

Both summands of the matrix body have explicit maximizing points. Consequently the support equalities below are equalities to attained finite suprema, not uses of the convention for an empty or unbounded real supremum.

def OAI.MetricEntropyDuality.supportFunction line 25
def OAI.MetricEntropyDuality.signVector line 28
theorem OAI.MetricEntropyDuality.signVector_mem_cube line 30
theorem OAI.MetricEntropyDuality.pairing_signVector line 35
theorem OAI.MetricEntropyDuality.pairing_cube_le line 43
theorem OAI.MetricEntropyDuality.supportFunction_cube line 53
theorem OAI.MetricEntropyDuality.polar_cube line 61
theorem OAI.MetricEntropyDuality.mem_smul_polar_iff line 72
Source documentation
This formulation does not require boundedness, symmetry, or attainment.
```
theorem mem_smul_polar_iff [Fintype ι] (K : Set (RealSpace ι)) (δ : RealSpace ι)
    {c : ℝ} (hc : 0 < c) :
    δ ∈ c • polar K ↔ ∀ z ∈ K, pairing z δ ≤ c := by
…
```
Mentions: OAI.MetricEntropyDuality.RealSpace, OAI.MetricEntropyDuality.polar, OAI.MetricEntropyDuality.pairing
theorem OAI.MetricEntropyDuality.row_mem_absRowHull line 88
theorem OAI.MetricEntropyDuality.neg_row_mem_absRowHull line 91
theorem OAI.MetricEntropyDuality.convex_pairing_le line 94
theorem OAI.MetricEntropyDuality.pairing_absRowHull_le_of_bounds line 104
def OAI.MetricEntropyDuality.rowSupport line 117
Source documentation
The row maximum is over the actual nonempty finite row index set.
```
def rowSupport [Fintype X] [Nonempty X] [Fintype Y]
    (g : Y → X → ℝ) (δ : RealSpace Y) : ℝ :=
…
```
Mentions: OAI.MetricEntropyDuality.RealSpace
theorem OAI.MetricEntropyDuality.abs_pairing_row_le_rowSupport line 121
theorem OAI.MetricEntropyDuality.rowSupport_attained line 126
theorem OAI.MetricEntropyDuality.rowSupport_nonneg line 134
theorem OAI.MetricEntropyDuality.absRowHull_support_attained line 140
theorem OAI.MetricEntropyDuality.supportFunction_absRowHull line 150
theorem OAI.MetricEntropyDuality.matrixBody_pairing_le_of_bounds line 161
Source documentation
The quantitative pointwise estimate consumed by the polar covering proof.
```
theorem matrixBody_pairing_le_of_bounds [Fintype Y]
    (g : Y → X → ℝ) (δ : RealSpace Y) {t M L : ℝ} (ht : 0 ≤ t)
    (hM : ∀ x, |pairing (row g x) δ| ≤ M) (hL : l1Norm δ ≤ L)
    {z : RealSpace Y} (hz : z ∈ matrixBody g t) : pairing z δ ≤ 3 * M + t * L := by
…
```
Mentions: OAI.MetricEntropyDuality.RealSpace, OAI.MetricEntropyDuality.pairing, OAI.MetricEntropyDuality.row, OAI.MetricEntropyDuality.l1Norm, OAI.MetricEntropyDuality.matrixBody
theorem OAI.MetricEntropyDuality.matrixBody_support_attained line 173
theorem OAI.MetricEntropyDuality.supportFunction_matrixBody line 182
theorem OAI.MetricEntropyDuality.mem_smul_polar_matrixBody_of_bounds line 193
theorem OAI.MetricEntropyDuality.mem_smul_polar_matrixBody_iff line 201