OAI/Computability/VertexCover/Reduction/AverageCommute.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.VertexCover.Restriction.EnergyForm.continuous_integrable line 49
  2. theorem OAI.VertexCover.Restriction.EnergyForm.continuous_mul_integrable line 52
  3. def OAI.VertexCover.Restriction.EnergyForm.integral line 57
  4. theorem OAI.VertexCover.Restriction.EnergyForm.integral_form line 84
  5. theorem OAI.VertexCover.Restriction.EnergyForm.integral_energy line 87
  6. def OAI.VertexCover.Restriction.EnergyForm.Projection.updateFunction line 100
  7. theorem OAI.VertexCover.Restriction.EnergyForm.Projection.updateFunction_apply line 106
  8. theorem OAI.VertexCover.Restriction.EnergyForm.Projection.updateFunction_integrable line 110
  9. def OAI.VertexCover.Restriction.EnergyForm.Projection.averageMap line 115
  10. theorem OAI.VertexCover.Restriction.EnergyForm.Projection.averageMap_apply line 135
  11. theorem OAI.VertexCover.Restriction.EnergyForm.Projection.average_update line 140
  12. theorem OAI.VertexCover.Restriction.EnergyForm.Projection.average_idem line 145
  13. theorem OAI.VertexCover.Restriction.EnergyForm.Projection.integral_average_mul_fixed line 151
  14. def OAI.VertexCover.Restriction.EnergyForm.Projection.average line 169
  15. theorem OAI.VertexCover.Restriction.EnergyForm.Projection.average_apply line 192
  16. theorem OAI.VertexCover.Restriction.EnergyForm.Projection.average_invariant line 195
  17. theorem OAI.VertexCover.Restriction.EnergyForm.Projection.average_commute line 198