OAI/Combinatorics/IndependentSets/Reduction/SamplerParameters.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.LargeIndependentSets.SamplerParameters line 13
  2. instance OAI.LargeIndependentSets.SamplerParameters.(instance at line 26) line 26
  3. lemma OAI.LargeIndependentSets.SamplerParameters.even line 29
  4. abbrev OAI.LargeIndependentSets.SamplerParameters.law line 35
  5. abbrev OAI.LargeIndependentSets.SamplerParameters.Vertices line 38
  6. def OAI.LargeIndependentSets.SamplerParameters.location line 41
  7. def OAI.LargeIndependentSets.SamplerParameters.graph line 45
  8. theorem OAI.LargeIndependentSets.SamplerParameters.completeness line 49
  9. def OAI.LargeIndependentSets.SamplerParameters.functions line 57
  10. lemma OAI.LargeIndependentSets.SamplerParameters.functions_lipschitz line 62
  11. lemma OAI.LargeIndependentSets.SamplerParameters.functions_bounded line 67
  12. lemma OAI.LargeIndependentSets.SamplerParameters.functions_odd line 73
  13. lemma OAI.LargeIndependentSets.SamplerParameters.functions_compatibility line 79
  14. theorem OAI.LargeIndependentSets.SamplerParameters.density_le_fibers line 100
  15. theorem OAI.LargeIndependentSets.finite_source_soundness line 129