OAI/Combinatorics/SumProduct/Alignment/MicrocellSaturation01.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.RawSmallCells.finite_event line 17
  2. theorem OAI.RawSmallCells.cover_cost line 28
  3. def OAI.RawSmallCells.partialCells line 60
  4. lemma OAI.RawSmallCells.partial_cover line 63
  5. theorem OAI.RawSmallCells.partial_cost line 85
  6. lemma OAI.RawSmallCells.partial_cost_simple line 97
  7. theorem OAI.RawSmallCells.eventually_partial line 106
  8. theorem OAI.RawPartitionSuccess.finite_partition line 133
  9. theorem OAI.RawPartitionSuccess.raw_partition line 176
  10. def OAI.MicrocellSaturation.good line 233
  11. def OAI.MicrocellSaturation.label line 237
  12. lemma OAI.MicrocellSaturation.quotient_window line 239
  13. lemma OAI.MicrocellSaturation.saturated line 247
  14. lemma OAI.MicrocellSaturation.enlarged_cell_stable line 268
  15. lemma OAI.MicrocellSaturation.law_restrict_units line 281
  16. theorem OAI.MicrocellSaturation.bad_conditioning_bound line 293
  17. lemma OAI.MicrocellSaturation.conditioned_fiber line 323
  18. lemma OAI.MicrocellSaturation.label_unit line 349
  19. theorem OAI.MicrocellSaturation.global_success line 360