OAI/Analysis/ForestSpace/FullDual.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.ForestSpace.headJ_finite_eq_sum line 16
  2. theorem OAI.ForestSpace.exists_headJ_approx line 26
  3. theorem OAI.ForestSpace.eq_zero_of_coordinates_zero line 44
  4. theorem OAI.ForestSpace.coordinateSubspace_eq_top_of_reflexive line 56
  5. theorem OAI.ForestSpace.forest_coordinateSubspace_eq_top line 80
  6. def OAI.ForestSpace.fullDualEquiv line 83
  7. theorem OAI.ForestSpace.reflexive_main_fullDual line 88
  8. theorem OAI.ForestSpace.separable_main_fullDual line 91
  9. theorem OAI.ForestSpace.infiniteDimensional_main_fullDual line 95
  10. theorem OAI.ForestSpace.exists_main_head_approx line 101
  11. def OAI.ForestSpace.mainFiniteCoordinates line 115
  12. theorem OAI.ForestSpace.mainFiniteCoordinates_kernel_finite line 118
  13. theorem OAI.ForestSpace.main_P_eq_zero_of_mem_ker line 122
  14. theorem OAI.ForestSpace.main_average_modulus line 132
  15. theorem OAI.ForestSpace.main_auc_modulus_zero line 153
  16. theorem OAI.ForestSpace.main_no_equivalent_AUC line 173