OAI/Geometry/LatticeCovering/GridCounts.lean

GitHub source file

43 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SingleLatticeCovering.RealLatticeCount.convex_dilation_mono line 13
  2. theorem OAI.SingleLatticeCovering.RealLatticeCount.tendsto_real_grid_count line 28
  3. theorem OAI.SingleLatticeCovering.RealLatticeCount.tendsto_convex_grid_count line 71
  4. def OAI.SingleLatticeCovering.GridGeometry.weightedGridConfiguration line 90
  5. lemma OAI.SingleLatticeCovering.GridGeometry.weightedGridConfiguration_convex line 94
  6. lemma OAI.SingleLatticeCovering.GridGeometry.weightedGridConfiguration_closed line 111
  7. lemma OAI.SingleLatticeCovering.GridGeometry.weightedGridConfiguration_bounded line 122
  8. lemma OAI.SingleLatticeCovering.GridGeometry.weightedGridConfiguration_compact line 132
  9. lemma OAI.SingleLatticeCovering.GridGeometry.zero_mem_weightedGridConfiguration line 138
  10. theorem OAI.SingleLatticeCovering.GridLimit.primitive_configuration_limit line 157
  11. lemma OAI.SingleLatticeCovering.GridLimit.finite_scaled_lattice_inter line 182
  12. lemma OAI.SingleLatticeCovering.GridLimit.projected_grid_relation_mem line 199
  13. lemma OAI.SingleLatticeCovering.GridLimit.omitted_vertex_identity line 217
  14. theorem OAI.SingleLatticeCovering.GridLimit.circuit_count_le_primitive_grid line 237
  15. abbrev OAI.SingleLatticeCovering.SimplexYoung.V line 294
  16. def OAI.SingleLatticeCovering.SimplexYoung.simplexMean line 296
  17. def OAI.SingleLatticeCovering.SimplexYoung.simplexForm line 298
  18. lemma OAI.SingleLatticeCovering.SimplexYoung.simplexForm_zero line 302
  19. lemma OAI.SingleLatticeCovering.SimplexYoung.simplexForm_succ line 304
  20. lemma OAI.SingleLatticeCovering.SimplexYoung.sum_simplexForm line 305
  21. def OAI.SingleLatticeCovering.SimplexYoung.simplexDual line 308
  22. lemma OAI.SingleLatticeCovering.SimplexYoung.simplexDual_apply line 319
  23. lemma OAI.SingleLatticeCovering.SimplexYoung.simplexDual_form line 321
  24. lemma OAI.SingleLatticeCovering.SimplexYoung.simplexForm_dual line 325
  25. lemma OAI.SingleLatticeCovering.SimplexYoung.simplex_projection_square line 338
  26. lemma OAI.SingleLatticeCovering.SimplexYoung.det_diagonal_rankOne line 357
  27. def OAI.SingleLatticeCovering.SimplexYoung.simplexJacobian line 368
  28. lemma OAI.SingleLatticeCovering.SimplexYoung.simplexJacobian_apply line 373
  29. lemma OAI.SingleLatticeCovering.SimplexYoung.simplexJacobian_det line 378
  30. lemma OAI.SingleLatticeCovering.SimplexYoung.simplexJacobian_det_ge line 396
  31. def OAI.SingleLatticeCovering.SimplexYoung.simplexTransport line 422
  32. lemma OAI.SingleLatticeCovering.SimplexYoung.simplexTransport_injective line 425
  33. def OAI.SingleLatticeCovering.SimplexYoung.simplexDerivative line 453
  34. lemma OAI.SingleLatticeCovering.SimplexYoung.simplexTransport_hasFDerivAt line 457
  35. lemma OAI.SingleLatticeCovering.SimplexYoung.simplexDerivative_eq line 467
  36. lemma OAI.SingleLatticeCovering.SimplexYoung.simplexDerivative_det line 481
  37. lemma OAI.SingleLatticeCovering.SimplexYoung.simplex_transport_pointwise line 486
  38. def OAI.SingleLatticeCovering.SimplexYoung.simplexRoot line 510
  39. lemma OAI.SingleLatticeCovering.SimplexYoung.simplexRoot_mulVec line 514
  40. lemma OAI.SingleLatticeCovering.SimplexYoung.simplexRoot_det line 520
  41. lemma OAI.SingleLatticeCovering.SimplexYoung.simplexRoot_square line 532
  42. lemma OAI.SingleLatticeCovering.SimplexYoung.simplex_gaussian_integral line 552
  43. lemma OAI.SingleLatticeCovering.SimplexYoung.simplex_transport_integral line 593