OAI/Analysis/ForestSpace/Reflexivity.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.ForestSpace.reflexive_of_equiv line 16
  2. theorem OAI.ForestSpace.reflexive_dual line 31
  3. theorem OAI.ForestSpace.reflexive_hilbert line 39
  4. def OAI.ForestSpace.l2DualMap line 54
  5. theorem OAI.ForestSpace.l2DualMap_apply line 58
  6. theorem OAI.ForestSpace.l2DualMap_single_right line 61
  7. theorem OAI.ForestSpace.l2DualMap_single_left line 68
  8. def OAI.ForestSpace.l2Restriction line 75
  9. theorem OAI.ForestSpace.l2_norm_sum_unit_le line 78
  10. theorem OAI.ForestSpace.l2_restriction_summable line 95
  11. theorem OAI.ForestSpace.l2DualMap_surjective line 120
  12. theorem OAI.ForestSpace.reflexive_l2 line 130
  13. theorem OAI.ForestSpace.completion_equiv_of_bounds line 158
  14. theorem OAI.ForestSpace.denseRange_lp_of_singles line 181
  15. def OAI.ForestSpace.rawL2Linear line 197
  16. theorem OAI.ForestSpace.rawL2Linear_apply line 207
  17. theorem OAI.ForestSpace.rawL2_norm_sq line 210
  18. theorem OAI.ForestSpace.rawL2_norm_le line 220
  19. def OAI.ForestSpace.rawL2 line 225
  20. theorem OAI.ForestSpace.rawL2_apply line 228
  21. theorem OAI.ForestSpace.sum_sq_le_support line 231
  22. theorem OAI.ForestSpace.rho_le_card_bound line 242
  23. theorem OAI.ForestSpace.rawL2_dense line 265
  24. theorem OAI.ForestSpace.reflexive_J_of_segment_card_bound line 273
  25. abbrev OAI.ForestSpace.Component line 279
  26. theorem OAI.ForestSpace.component_segment_card line 281
  27. theorem OAI.ForestSpace.reflexive_component line 300