OAI/NumberTheory/Ostmann/Arithmetic/OneSidedGraphFactor.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Separating a one-sided graph edge from the bounded unary factors

  1. def OAI.Ostmann.twoVertexLabels line 11
  2. def OAI.Ostmann.finiteEdgeWeight line 16
  3. def OAI.Ostmann.fixedGraphFactor line 20
  4. def OAI.Ostmann.longGraphFactor line 25
  5. def OAI.Ostmann.shortGraphFactor line 31
  6. theorem OAI.Ostmann.one_sided_graph_factorization line 37
  7. theorem OAI.Ostmann.norm_mul_le_one' line 50
  8. theorem OAI.Ostmann.norm_prod_le_one' line 54
  9. theorem OAI.Ostmann.fixedGraphFactor_norm line 59
  10. theorem OAI.Ostmann.longGraphFactor_norm line 68
  11. theorem OAI.Ostmann.shortGraphFactor_norm line 77