OAI/Analysis/C0Absorption/Molecules.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.C0Absorption.MoleculeSpace line 16
  2. abbrev OAI.C0Absorption.Molecule line 19
  3. def OAI.C0Absorption.pairing line 21
  4. def OAI.C0Absorption.molecule line 26
  5. theorem OAI.C0Absorption.pairing_molecule line 30
  6. theorem OAI.C0Absorption.pairing_const line 34
  7. theorem OAI.C0Absorption.molecule_decomposition line 43
  8. theorem OAI.C0Absorption.molecule_self line 55
  9. theorem OAI.C0Absorption.molecule_sub_molecule line 59
  10. structure OAI.C0Absorption.AdmissibleList line 71
  11. def OAI.C0Absorption.AdmissibleList.empty line 78
  12. instance OAI.C0Absorption.(instance at line 88) line 88
  13. theorem OAI.C0Absorption.AdmissibleList.sum_abs_sub_le line 91
  14. theorem OAI.C0Absorption.finite_lp_norm_le_sum line 112
  15. def OAI.C0Absorption.AdmissibleList.eval line 124
  16. theorem OAI.C0Absorption.AdmissibleList.eval_apply line 130
  17. def OAI.C0Absorption.AdmissibleList.seminorm line 134
  18. theorem OAI.C0Absorption.AdmissibleList.seminorm_apply line 138
  19. theorem OAI.C0Absorption.AdmissibleList.seminorm_molecule_le line 142
  20. theorem OAI.C0Absorption.AdmissibleList.seminorm_le line 151
  21. def OAI.C0Absorption.sigma line 172
  22. theorem OAI.C0Absorption.list_seminorms_bddAbove line 176
  23. theorem OAI.C0Absorption.sigma_apply line 185
  24. theorem OAI.C0Absorption.sigma_molecule_le line 190
  25. theorem OAI.C0Absorption.list_le_sigma line 196
  26. theorem OAI.C0Absorption.sigma_le line 201
  27. def OAI.C0Absorption.squareVector line 215
  28. theorem OAI.C0Absorption.squareVector_apply line 220
  29. def OAI.C0Absorption.squareSeminorm line 223
  30. theorem OAI.C0Absorption.squareSeminorm_apply line 245
  31. theorem OAI.C0Absorption.squareSeminorm_sq line 248
  32. theorem OAI.C0Absorption.coordinate_le_squareSeminorm line 254
  33. theorem OAI.C0Absorption.seminorm_abs_sub_le line 260
  34. theorem OAI.C0Absorption.squareVector_sub_norm_le line 270