OAI/Computability/VertexCover/Analysis/Restriction.lean

GitHub source file

58 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.VertexCover.Restriction.EnergyForm line 44
  2. def OAI.VertexCover.Restriction.EnergyForm.energy line 52
  3. theorem OAI.VertexCover.Restriction.EnergyForm.energy_zero line 54
  4. theorem OAI.VertexCover.Restriction.EnergyForm.energy_nonneg line 55
  5. theorem OAI.VertexCover.Restriction.EnergyForm.energy_add line 57
  6. theorem OAI.VertexCover.Restriction.EnergyForm.energy_sub line 63
  7. structure OAI.VertexCover.Restriction.EnergyForm.Projection line 69
  8. instance OAI.VertexCover.Restriction.EnergyForm.Projection.(instance at line 76) line 76
  9. theorem OAI.VertexCover.Restriction.EnergyForm.Projection.apply_idem line 78
  10. theorem OAI.VertexCover.Restriction.EnergyForm.Projection.map_zero line 79
  11. theorem OAI.VertexCover.Restriction.EnergyForm.Projection.map_add line 80
  12. theorem OAI.VertexCover.Restriction.EnergyForm.Projection.map_sub line 82
  13. theorem OAI.VertexCover.Restriction.EnergyForm.Projection.map_smul line 84
  14. theorem OAI.VertexCover.Restriction.EnergyForm.Projection.ext line 87
  15. def OAI.VertexCover.Restriction.EnergyForm.Projection.ident line 96
  16. theorem OAI.VertexCover.Restriction.EnergyForm.Projection.ident_apply line 101
  17. def OAI.VertexCover.Restriction.EnergyForm.Projection.zero line 103
  18. theorem OAI.VertexCover.Restriction.EnergyForm.Projection.zero_apply line 108
  19. def OAI.VertexCover.Restriction.EnergyForm.Projection.residual line 110
  20. theorem OAI.VertexCover.Restriction.EnergyForm.Projection.residual_apply line 117
  21. theorem OAI.VertexCover.Restriction.EnergyForm.Projection.residual_residual line 118
  22. theorem OAI.VertexCover.Restriction.EnergyForm.Projection.inner_image line 122
  23. theorem OAI.VertexCover.Restriction.EnergyForm.Projection.pythagoras line 125
  24. theorem OAI.VertexCover.Restriction.EnergyForm.Projection.energy_le line 130
  25. def OAI.VertexCover.Restriction.EnergyForm.Projection.comp line 135
  26. theorem OAI.VertexCover.Restriction.EnergyForm.Projection.comp_apply line 144
  27. theorem OAI.VertexCover.Restriction.EnergyForm.Projection.residual_commute line 146
  28. theorem OAI.VertexCover.Restriction.EnergyForm.Projection.comp_loss_le line 150
  29. theorem OAI.VertexCover.Restriction.EnergyForm.Projection.residual_le_of_nested line 161
  30. def OAI.VertexCover.Restriction.EnergyForm.Projection.productMap line 174
  31. theorem OAI.VertexCover.Restriction.EnergyForm.Projection.productMap_nil line 178
  32. theorem OAI.VertexCover.Restriction.EnergyForm.Projection.productMap_cons line 180
  33. theorem OAI.VertexCover.Restriction.EnergyForm.Projection.productMap_append line 184
  34. theorem OAI.VertexCover.Restriction.EnergyForm.Projection.productMap_commute line 191
  35. theorem OAI.VertexCover.Restriction.EnergyForm.Projection.productMap_fixed_of_mem line 199
  36. def OAI.VertexCover.Restriction.EnergyForm.Projection.product line 210
  37. theorem OAI.VertexCover.Restriction.EnergyForm.Projection.product_apply line 228
  38. theorem OAI.VertexCover.Restriction.EnergyForm.Projection.product_loss_le line 231
  39. def OAI.VertexCover.Restriction.EnergyForm.Projection.difference line 247
  40. theorem OAI.VertexCover.Restriction.EnergyForm.Projection.difference_apply line 253
  41. theorem OAI.VertexCover.Restriction.EnergyForm.Projection.difference_energy_sum line 257
  42. theorem OAI.VertexCover.Restriction.EnergyForm.Projection.difference_energy_sum_le line 272
  43. theorem OAI.VertexCover.Restriction.EnergyForm.Projection.difference_commute line 279
  44. theorem OAI.VertexCover.Restriction.EnergyForm.Projection.difference_residual_budget line 285
  45. theorem OAI.VertexCover.Restriction.EnergyForm.Projection.difference_retained_le line 297
  46. theorem OAI.VertexCover.Restriction.EnergyForm.Projection.productMap_map line 304
  47. def OAI.VertexCover.Restriction.EnergyForm.Projection.natExtension line 311
  48. theorem OAI.VertexCover.Restriction.EnergyForm.Projection.natExtension_fin line 314
  49. theorem OAI.VertexCover.Restriction.EnergyForm.Projection.natExtension_commute line 317
  50. theorem OAI.VertexCover.Restriction.EnergyForm.Projection.natExtension_commute_of line 325
  51. theorem OAI.VertexCover.Restriction.EnergyForm.Projection.productMap_range_natExtension line 331
  52. def OAI.VertexCover.Restriction.EnergyForm.Projection.finDifference line 341
  53. theorem OAI.VertexCover.Restriction.EnergyForm.Projection.finDifference_energy_sum line 345
  54. theorem OAI.VertexCover.Restriction.EnergyForm.Projection.finDifference_residual_budget line 353
  55. theorem OAI.VertexCover.Restriction.EnergyForm.Projection.finDifference_retained_le line 363
  56. theorem OAI.VertexCover.Restriction.EnergyForm.Projection.finDifference_centered line 370
  57. theorem OAI.VertexCover.Restriction.EnergyForm.Projection.finDifference_commute line 376
  58. theorem OAI.VertexCover.Restriction.EnergyForm.Projection.product_loss_finset line 383