OAI/Geometry/LatticeCovering/CircuitVolumes.lean

GitHub source file

43 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SingleLatticeCovering.SimplexYoung.volume_weightedSimplexConfiguration_sharp line 23
  2. lemma OAI.SingleLatticeCovering.SimplexYoung.tsum_int_inv_sq_le_four line 39
  3. lemma OAI.SingleLatticeCovering.SimplexYoung.int_circuit_weight_le_sq line 52
  4. lemma OAI.SingleLatticeCovering.SimplexYoung.tsum_ennreal_int_circuit_weight_le line 61
  5. lemma OAI.SingleLatticeCovering.SimplexYoung.tsum_ennreal_fin_prod line 71
  6. theorem OAI.SingleLatticeCovering.SimplexYoung.tsum_integerCircuitWeight_le line 84
  7. def OAI.SingleLatticeCovering.SimplexYoung.integerCircuitVolumeSum line 99
  8. theorem OAI.SingleLatticeCovering.SimplexYoung.integerCircuitVolumeSum_le line 106
  9. lemma OAI.SingleLatticeCovering.SimplexYoung.rationalCircuitFactor line 145
  10. def OAI.SingleLatticeCovering.SimplexYoung.rationalCircuitVolume line 167
  11. lemma OAI.SingleLatticeCovering.SimplexYoung.rationalCircuitVolume_le line 172
  12. def OAI.SingleLatticeCovering.SimplexYoung.rationalCircuitVolumeSum line 195
  13. theorem OAI.SingleLatticeCovering.SimplexYoung.rationalCircuitVolumeSum_le line 198
  14. lemma OAI.SingleLatticeCovering.SimplexYoung.affine_three_product_abs_ge_two line 233
  15. lemma OAI.SingleLatticeCovering.SimplexYoung.prod_circuit_weight_with_saving line 263
  16. theorem OAI.SingleLatticeCovering.SimplexYoung.tsum_affine_three_weight_le line 278
  17. lemma OAI.SingleLatticeCovering.SimplexYoung.two_neg_third_le line 299
  18. lemma OAI.SingleLatticeCovering.SimplexYoung.simplexConstant_sq line 311
  19. lemma OAI.SingleLatticeCovering.SimplexYoung.rank_two_saved_constant line 327
  20. lemma OAI.SingleLatticeCovering.SimplexYoung.rank_two_saved_power line 336
  21. def OAI.SingleLatticeCovering.SimplexYoung.affineCircuitVolumeSum line 351
  22. theorem OAI.SingleLatticeCovering.SimplexYoung.affineRankTwoCircuitVolumeSum_le line 356
  23. def OAI.SingleLatticeCovering.GridCoordinates.flatten line 414
  24. lemma OAI.SingleLatticeCovering.GridCoordinates.flatten_unit_preimage line 422
  25. theorem OAI.SingleLatticeCovering.GridCoordinates.flatten_measurePreserving line 433
  26. lemma OAI.SingleLatticeCovering.CircuitVolume.configuration_preimage line 458
  27. lemma OAI.SingleLatticeCovering.CircuitVolume.configuration_volume line 461
  28. lemma OAI.SingleLatticeCovering.CircuitVolume.rationalCircuitVolume_toReal line 468
  29. lemma OAI.SingleLatticeCovering.CircuitVolume.summable_rationalCircuitVolume_toReal line 477
  30. lemma OAI.SingleLatticeCovering.CircuitVolume.affineCircuitVolumeSum_ne_top line 483
  31. def OAI.SingleLatticeCovering.CircuitVolume.PrimitiveAffineCoefficients line 493
  32. lemma OAI.SingleLatticeCovering.CircuitVolume.primitive_volume_sum_le line 496
  33. lemma OAI.SingleLatticeCovering.CircuitPacking.colored_packing_bound line 531
  34. lemma OAI.SingleLatticeCovering.CircuitPacking.fundamental_translate_disjoint line 566
  35. lemma OAI.SingleLatticeCovering.CircuitPacking.fundamental_coord_bound line 586
  36. lemma OAI.SingleLatticeCovering.CircuitPacking.sublattice_index_ne_zero line 603
  37. lemma OAI.SingleLatticeCovering.CircuitPacking.fundamental_volume line 615
  38. lemma OAI.SingleLatticeCovering.CircuitPacking.cancel_packing_ratio line 623
  39. lemma OAI.SingleLatticeCovering.CircuitPacking.sublattice_card_ratio line 632
  40. lemma OAI.SingleLatticeCovering.CircuitPacking.lattice_coset_packing line 646
  41. theorem OAI.SingleLatticeCovering.CircuitPacking.short_basis_lattice_packing line 676
  42. lemma OAI.SingleLatticeCovering.CircuitPacking.volume_symmetric_box line 696
  43. lemma OAI.SingleLatticeCovering.CircuitPacking.short_basis_lattice_count line 703