OAI/Analysis/NuclearUltrapower/IntegralCertificate.lean

GitHub source file

45 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.NuclearUltrapower.SL3Certificate.dot_nil_left line 11
  2. theorem OAI.NuclearUltrapower.SL3Certificate.dot_nil_right line 12
  3. theorem OAI.NuclearUltrapower.SL3Certificate.dot_eq_sum_getD line 14
  4. theorem OAI.NuclearUltrapower.SL3Certificate.star_list_sum line 32
  5. theorem OAI.NuclearUltrapower.SL3Certificate.list_sum_finset line 38
  6. theorem OAI.NuclearUltrapower.SL3Certificate.list_gram_identity line 45
  7. theorem OAI.NuclearUltrapower.SL3Certificate.list_gram_nonneg line 72
  8. def OAI.NuclearUltrapower.SOS.gramData line 84
  9. theorem OAI.NuclearUltrapower.SOS.gramData_eq line 85
  10. theorem OAI.NuclearUltrapower.SOS.gramData_roots line 86
  11. def OAI.NuclearUltrapower.SOS.gramPolyRow line 92
  12. theorem OAI.NuclearUltrapower.SOS.residualRows_decomp line 95
  13. def OAI.NuclearUltrapower.SOS.rootPairs line 98
  14. theorem OAI.NuclearUltrapower.SOS.columns_length line 100
  15. theorem OAI.NuclearUltrapower.SOS.columns_bound line 102
  16. def OAI.NuclearUltrapower.SOS.gramValue line 112
  17. theorem OAI.NuclearUltrapower.SOS.gramValue_nonneg line 116
  18. theorem OAI.NuclearUltrapower.SOS.eval_gram_rows line 125
  19. theorem OAI.NuclearUltrapower.SOS.mem_getD_flatten line 158
  20. theorem OAI.NuclearUltrapower.SOS.bucket_support_original line 167
  21. theorem OAI.NuclearUltrapower.SOS.delta_good line 191
  22. theorem OAI.NuclearUltrapower.SOS.residualRow0_good line 197
  23. theorem OAI.NuclearUltrapower.SOS.residualRow1_good line 203
  24. theorem OAI.NuclearUltrapower.SOS.gramPolyRow_good line 207
  25. theorem OAI.NuclearUltrapower.SOS.residualRows_good line 212
  26. theorem OAI.NuclearUltrapower.SOS.residual_good line 222
  27. theorem OAI.NuclearUltrapower.SOS.ElementarySpectral.residual_value line 243
  28. theorem OAI.NuclearUltrapower.SOS.ElementarySpectral.residual_to_certificate line 263
  29. theorem OAI.NuclearUltrapower.SOS.ElementarySpectral.certificate_value line 271
  30. theorem OAI.NuclearUltrapower.SOS.ElementarySpectral.operator_certificate line 284
  31. def OAI.NuclearUltrapower.SOS.ElementarySpectral.deltaOp line 295
  32. def OAI.NuclearUltrapower.SOS.ElementarySpectral.residualInE line 298
  33. theorem OAI.NuclearUltrapower.SOS.ElementarySpectral.residualInE_aug line 300
  34. theorem OAI.NuclearUltrapower.SOS.ElementarySpectral.residualInE_l1 line 303
  35. theorem OAI.NuclearUltrapower.SOS.ElementarySpectral.residualInE_support line 306
  36. theorem OAI.NuclearUltrapower.SOS.ElementarySpectral.residualInE_operator line 312
  37. def OAI.NuclearUltrapower.SOS.ElementarySpectral.gramOp line 318
  38. theorem OAI.NuclearUltrapower.SOS.ElementarySpectral.deltaOp_nonneg line 321
  39. theorem OAI.NuclearUltrapower.SOS.ElementarySpectral.gramOp_nonneg line 323
  40. theorem OAI.NuclearUltrapower.SOS.ElementarySpectral.deltaOp_energy line 326
  41. theorem OAI.NuclearUltrapower.SOS.residual_value_generic line 340
  42. theorem OAI.NuclearUltrapower.SOS.ElementarySpectral.residual_value_native line 363
  43. theorem OAI.NuclearUltrapower.SOS.ElementarySpectral.deltaOp_certificate line 392
  44. theorem OAI.NuclearUltrapower.SOS.ElementarySpectral.deltaOp_sq_gap line 402
  45. theorem OAI.NuclearUltrapower.SOS.ElementarySpectral.deltaOp_gap line 408