OAI/Analysis/MetricEntropy/Basic.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

Literal finite-dimensional convex bodies and covering numbers

The coordinate space carries its ordinary finite product topology and sup norm. Polar membership uses the actual real coordinate pairing. Covering centers are unrestricted ambient vectors. coveringNumber is the least finite cover size; the natural-number empty-infimum convention is zero when no finite cover exists. The geometric applications prove Coverable before using attainment, positivity, or a lower bound, so that convention never substitutes for a genuine minimum.

  1. def OAI.MetricEntropyDuality.l1Norm line 24
  2. def OAI.MetricEntropyDuality.l1Ball line 27
  3. def OAI.MetricEntropyDuality.row line 30
  4. def OAI.MetricEntropyDuality.columnCombination line 33
  5. def OAI.MetricEntropyDuality.UniformClose line 37
  6. def OAI.MetricEntropyDuality.UniformApproximation line 41

    Source documentation

    The approximation list may contain functions outside the column hull.

    def UniformApproximation {X : Type uX} {Y : Type uY} [Fintype Y]
    (g : Y → X → ℝ) (ε : ℝ) (A : Finset (RealSpace X)) : Prop :=
…

    Mentions: OAI.MetricEntropyDuality.RealSpace

  7. def OAI.MetricEntropyDuality.absRowHull line 45
  8. def OAI.MetricEntropyDuality.matrixBody line 48
  9. theorem OAI.MetricEntropyDuality.pairing_zero_left line 55
  10. theorem OAI.MetricEntropyDuality.pairing_zero_right line 58
  11. theorem OAI.MetricEntropyDuality.pairing_comm line 61
  12. theorem OAI.MetricEntropyDuality.pairing_add_left line 64
  13. theorem OAI.MetricEntropyDuality.pairing_add_right line 68
  14. theorem OAI.MetricEntropyDuality.pairing_sub_left line 72
  15. theorem OAI.MetricEntropyDuality.pairing_sub_right line 76
  16. theorem OAI.MetricEntropyDuality.pairing_smul_left line 80
  17. theorem OAI.MetricEntropyDuality.pairing_smul_right line 84
  18. theorem OAI.MetricEntropyDuality.pairing_neg_left line 88
  19. theorem OAI.MetricEntropyDuality.pairing_neg_right line 92
  20. theorem OAI.MetricEntropyDuality.l1Norm_nonneg line 96
  21. theorem OAI.MetricEntropyDuality.l1Norm_zero line 99
  22. theorem OAI.MetricEntropyDuality.l1Norm_neg line 102
  23. theorem OAI.MetricEntropyDuality.l1Norm_sub_le line 105
  24. theorem OAI.MetricEntropyDuality.zero_mem_cube line 115
  25. theorem OAI.MetricEntropyDuality.zero_mem_l1Ball line 118
  26. theorem OAI.MetricEntropyDuality.UniformClose.symm line 121
  27. theorem OAI.MetricEntropyDuality.columnCombination_sub line 126
  28. theorem OAI.MetricEntropyDuality.columnCombination_zero line 132
  29. theorem OAI.MetricEntropyDuality.pairing_row_eq_columnCombination line 137