OAI/Analysis/C0Absorption/Finite.lean

GitHub source file

48 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.C0Absorption.sparseC0 line 17
  2. theorem OAI.C0Absorption.sparseC0_apply line 24
  3. theorem OAI.C0Absorption.sparseC0_outside line 27
  4. theorem OAI.C0Absorption.sparseC0_norm_le line 30
  5. def OAI.C0Absorption.sparseC0L line 40
  6. theorem OAI.C0Absorption.sparseC0_norm line 61
  7. def OAI.C0Absorption.sparseC0Isometry line 68
  8. abbrev OAI.C0Absorption.FLevel line 74
  9. abbrev OAI.C0Absorption.FLabel line 75
  10. abbrev OAI.C0Absorption.FCoord line 76
  11. abbrev OAI.C0Absorption.FInput line 77
  12. def OAI.C0Absorption.fLabel line 79
  13. theorem OAI.C0Absorption.fLabel_injective line 81
  14. def OAI.C0Absorption.fCoord line 92
  15. theorem OAI.C0Absorption.fCoord_injective line 94
  16. def OAI.C0Absorption.finiteEmbed line 101
  17. theorem OAI.C0Absorption.finiteEmbed_apply line 103
  18. theorem OAI.C0Absorption.finiteEmbed_row line 106
  19. theorem OAI.C0Absorption.finiteEmbed_block line 109
  20. theorem OAI.C0Absorption.finiteEmbed_row_outside line 112
  21. theorem OAI.C0Absorption.finiteEmbed_block_outside line 119
  22. def OAI.C0Absorption.finiteRow line 144
  23. theorem OAI.C0Absorption.finiteRow_eq line 147
  24. theorem OAI.C0Absorption.finiteRow_bound line 152
  25. def OAI.C0Absorption.finPred line 157
  26. def OAI.C0Absorption.finitePrev line 159
  27. theorem OAI.C0Absorption.finitePrev_eq line 162
  28. def OAI.C0Absorption.finiteFrozenFunction line 170
  29. theorem OAI.C0Absorption.finiteFrozen_row line 175
  30. theorem OAI.C0Absorption.finiteFrozen_block line 178
  31. theorem OAI.C0Absorption.finiteFrozen_bound line 187
  32. def OAI.C0Absorption.finiteFrozen line 195
  33. def OAI.C0Absorption.finiteNext line 212
  34. theorem OAI.C0Absorption.finiteNext_bound line 215
  35. def OAI.C0Absorption.finiteInverseFunction line 221
  36. theorem OAI.C0Absorption.finiteInverse_row line 226
  37. theorem OAI.C0Absorption.finiteInverse_block line 229
  38. theorem OAI.C0Absorption.finiteInverse_bound line 232
  39. theorem OAI.C0Absorption.finiteRow_inverse line 247
  40. theorem OAI.C0Absorption.finitePrev_inverse line 255
  41. theorem OAI.C0Absorption.finiteFrozen_inverse line 272
  42. theorem OAI.C0Absorption.finiteRow_frozen line 285
  43. theorem OAI.C0Absorption.finiteNext_frozen line 294
  44. theorem OAI.C0Absorption.finiteInverse_frozen line 305
  45. def OAI.C0Absorption.finiteEquiv line 317
  46. theorem OAI.C0Absorption.finiteEquiv_symm_apply line 324
  47. theorem OAI.C0Absorption.finiteFrozen_lower line 330
  48. theorem OAI.C0Absorption.finiteEquiv_symm_norm line 333