OAI/Computability/VertexCover/Reduction/PrivateProjectionCoordinateVariance.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.VertexCover.LabelCover.spliceSeeds_at_inside line 45
  2. theorem OAI.VertexCover.LabelCover.spliceSeeds_at_outside line 50
  3. def OAI.VertexCover.LabelCover.privateFiber line 55
  4. theorem OAI.VertexCover.LabelCover.mem_privateFiber line 60
  5. theorem OAI.VertexCover.LabelCover.spliceSeeds_restrict_of_outside line 66
  6. def OAI.VertexCover.LabelCover.privateFiberEquiv line 74
  7. theorem OAI.VertexCover.LabelCover.fiberAverage_eq_finiteMean line 103
  8. theorem OAI.VertexCover.LabelCover.privateSeedProjection_fiber line 115
  9. theorem OAI.VertexCover.LabelCover.otherWeightProjection_apply line 133
  10. theorem OAI.VertexCover.LabelCover.realWeights_splice line 145
  11. theorem OAI.VertexCover.LabelCover.otherWeightProjection_separator_splice line 156
  12. theorem OAI.VertexCover.LabelCover.privateAverageProjection_separator line 176
  13. theorem OAI.VertexCover.LabelCover.outsideSum_update line 191
  14. theorem OAI.VertexCover.LabelCover.privateProjection_separator line 203
  15. theorem OAI.VertexCover.LabelCover.privateProjection_coordinate_variance line 224