OAI/Analysis/SegmentLenses/AtomicBalls.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

Atomic polar descriptions of finite unit balls

  1. theorem OAI.SegmentLenses.SegmentFamily.ext line 21
  2. abbrev OAI.SegmentLenses.LocalFamily line 29
  3. instance OAI.SegmentLenses.localFamilyFinite line 31
  4. instance OAI.SegmentLenses.localFamilyFintype line 37
  5. abbrev OAI.SegmentLenses.FamilyCoefficients line 40
  6. abbrev OAI.SegmentLenses.LocalCoefficients line 44
  7. def OAI.SegmentLenses.familyValue line 46
  8. theorem OAI.SegmentLenses.familyValue_apply line 51
  9. def OAI.SegmentLenses.localValue line 57
  10. def OAI.SegmentLenses.coefficientBudget line 62
  11. theorem OAI.SegmentLenses.continuous_coefficientBudget line 64
  12. theorem OAI.SegmentLenses.coefficientBudget_nonneg line 69
  13. theorem OAI.SegmentLenses.norm_le_coefficientBudget line 72
  14. theorem OAI.SegmentLenses.compact_coefficientBall line 78
  15. theorem OAI.SegmentLenses.convex_coefficientBall line 85
  16. def OAI.SegmentLenses.atomicBody line 103
  17. theorem OAI.SegmentLenses.compact_atomicBody line 106
  18. theorem OAI.SegmentLenses.convex_atomicBody line 110
  19. theorem OAI.SegmentLenses.zero_mem_atomicBody line 113
  20. theorem OAI.SegmentLenses.familyValue_mem_atomicBody line 118
  21. def OAI.SegmentLenses.Test.ofFinite line 143
  22. theorem OAI.SegmentLenses.Test.coeff_ofFinite line 146
  23. theorem OAI.SegmentLenses.Test.support_ofFinite line 152
  24. theorem OAI.SegmentLenses.Test.coe_ofFinite line 158
  25. theorem OAI.SegmentLenses.dual_apply_ofFinite line 164
  26. def OAI.SegmentLenses.polarTest line 169
  27. theorem OAI.SegmentLenses.polarTest_pairing line 172
  28. theorem OAI.SegmentLenses.polarTest_familyValue line 176
  29. theorem OAI.SegmentLenses.norm_normalized_le line 194
  30. theorem OAI.SegmentLenses.normalized_pairing line 200
  31. theorem OAI.SegmentLenses.mem_atomicBody_of_norm_le_one line 219