OAI/Analysis/NuclearUltrapower/SOSSemantics.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.NuclearUltrapower.SOS.eval_append line 12
  2. theorem OAI.NuclearUltrapower.SOS.eval_flatMap line 17
  3. theorem OAI.NuclearUltrapower.SOS.eval_flatten line 24
  4. theorem OAI.NuclearUltrapower.SOS.list_sum_comm line 31
  5. theorem OAI.NuclearUltrapower.SOS.sum_getD line 39
  6. theorem OAI.NuclearUltrapower.SOS.eval_buckets line 53
  7. theorem OAI.NuclearUltrapower.SOS.support_addHead_iff line 73
  8. theorem OAI.NuclearUltrapower.SOS.support_compress_iff line 81
  9. theorem OAI.NuclearUltrapower.SOS.support_normalize_iff line 87
  10. theorem OAI.NuclearUltrapower.SOS.eval_scale line 95
  11. theorem OAI.NuclearUltrapower.SOS.eval_mul line 103
  12. def OAI.NuclearUltrapower.SOS.toMatrix line 130
  13. theorem OAI.NuclearUltrapower.SOS.toMatrix_one line 132
  14. theorem OAI.NuclearUltrapower.SOS.toMatrix_mul line 136
  15. theorem OAI.NuclearUltrapower.SOS.toMatrix_inv line 141
  16. abbrev OAI.NuclearUltrapower.SOS.SL line 147
  17. def OAI.NuclearUltrapower.SOS.interpret line 150

    Source documentation

    Total interpretation of a label; the certificate will establish det=1 at every label used.

    def interpret (m : Mat3) : SL :=
…

    Mentions: OAI.NuclearUltrapower.SOS.Mat3, OAI.NuclearUltrapower.SOS.SL

  18. theorem OAI.NuclearUltrapower.SOS.interpret_coe line 153
  19. theorem OAI.NuclearUltrapower.SOS.interpret_one line 157
  20. theorem OAI.NuclearUltrapower.SOS.interpret_mul line 162
  21. theorem OAI.NuclearUltrapower.SOS.interpret_inv line 168
  22. theorem OAI.NuclearUltrapower.SOS.intL1_flatten line 179
  23. def OAI.NuclearUltrapower.SOS.augmentation line 187
  24. theorem OAI.NuclearUltrapower.SOS.augmentation_flatten line 189
  25. def OAI.NuclearUltrapower.SOS.residual line 197
  26. theorem OAI.NuclearUltrapower.SOS.row_lengths line 199
  27. theorem OAI.NuclearUltrapower.SOS.row_length_bound line 203
  28. theorem OAI.NuclearUltrapower.SOS.row_normalizations line 210
  29. theorem OAI.NuclearUltrapower.SOS.residual_eval line 214
  30. theorem OAI.NuclearUltrapower.SOS.residual_l1 line 222
  31. theorem OAI.NuclearUltrapower.SOS.residual_augmentation line 226