OAI/NumberTheory/OrdinaryCorrelations/HighTrace/BitWeight.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.OrdinaryCorrelations.NumericalSubtrees.bitWeight line 16
  2. def OAI.OrdinaryCorrelations.NumericalSubtrees.Demand line 19
  3. lemma OAI.OrdinaryCorrelations.NumericalSubtrees.bitWeight_nonneg line 22
  4. lemma OAI.OrdinaryCorrelations.NumericalSubtrees.sum_bitWeight line 29
  5. lemma OAI.OrdinaryCorrelations.NumericalSubtrees.demand_product line 38
  6. theorem OAI.OrdinaryCorrelations.NumericalSubtrees.demand_weight line 55
  7. def OAI.OrdinaryCorrelations.NumericalSubtrees.Grows line 80
  8. def OAI.OrdinaryCorrelations.NumericalSubtrees.reached line 84
  9. def OAI.OrdinaryCorrelations.NumericalSubtrees.outgoing line 87
  10. lemma OAI.OrdinaryCorrelations.NumericalSubtrees.grows_edge_origins line 90
  11. lemma OAI.OrdinaryCorrelations.NumericalSubtrees.grows_outgoing line 96
  12. theorem OAI.OrdinaryCorrelations.NumericalSubtrees.grows_demands_disjoint line 101
  13. def OAI.OrdinaryCorrelations.NumericalSubtrees.shapes line 133
  14. lemma OAI.OrdinaryCorrelations.NumericalSubtrees.mem_shapes line 136
  15. lemma OAI.OrdinaryCorrelations.NumericalSubtrees.empty_mem_shapes line 141
  16. lemma OAI.OrdinaryCorrelations.NumericalSubtrees.sum_demands_pointwise line 145
  17. lemma OAI.OrdinaryCorrelations.NumericalSubtrees.sum_shape_weights line 166
  18. lemma OAI.OrdinaryCorrelations.NumericalSubtrees.outgoing_card line 181
  19. lemma OAI.OrdinaryCorrelations.NumericalSubtrees.reached_empty line 186
  20. lemma OAI.OrdinaryCorrelations.NumericalSubtrees.sum_nonempty_shape_weights line 189
  21. lemma OAI.OrdinaryCorrelations.NumericalSubtrees.grows_min_origin line 199
  22. lemma OAI.OrdinaryCorrelations.NumericalSubtrees.reached_eq_edgeVertices line 205
  23. theorem OAI.OrdinaryCorrelations.NumericalSubtrees.numerical_subtree_sum_le line 220