OAI/Geometry/LatticeCovering/Transport.lean

GitHub source file

52 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.SingleLatticeCovering.SharpYoung.PositiveDensity line 15
  2. instance OAI.SingleLatticeCovering.SharpYoung.(instance at line 22) line 22
  3. def OAI.SingleLatticeCovering.SharpYoung.densityCDF line 24
  4. lemma OAI.SingleLatticeCovering.SharpYoung.densityCDF_hasDerivAt line 26
  5. lemma OAI.SingleLatticeCovering.SharpYoung.densityCDF_continuous line 39
  6. lemma OAI.SingleLatticeCovering.SharpYoung.densityCDF_strictMono line 42
  7. lemma OAI.SingleLatticeCovering.SharpYoung.densityCDF_add_tail line 48
  8. lemma OAI.SingleLatticeCovering.SharpYoung.densityCDF_mem_Ioo line 52
  9. lemma OAI.SingleLatticeCovering.SharpYoung.densityCDF_tendsto_bot line 61
  10. lemma OAI.SingleLatticeCovering.SharpYoung.densityCDF_tendsto_top line 64
  11. lemma OAI.SingleLatticeCovering.SharpYoung.densityCDF_surjOn line 73
  12. def OAI.SingleLatticeCovering.SharpYoung.densityCDFIso line 78
  13. lemma OAI.SingleLatticeCovering.SharpYoung.densityCDFIso_apply line 85
  14. def OAI.SingleLatticeCovering.SharpYoung.densityTransport line 89
  15. lemma OAI.SingleLatticeCovering.SharpYoung.densityCDF_transport line 92
  16. lemma OAI.SingleLatticeCovering.SharpYoung.densityTransport_hasDerivAt line 97
  17. def OAI.SingleLatticeCovering.SharpYoung.normalizedGaussianDensity line 104
  18. lemma OAI.SingleLatticeCovering.SharpYoung.gaussian_transport_density line 118
  19. def OAI.SingleLatticeCovering.SimplexYoung.simplexConstant line 135
  20. lemma OAI.SingleLatticeCovering.SimplexYoung.simplexConstant_nonneg line 138
  21. lemma OAI.SingleLatticeCovering.SimplexYoung.simplex_positiveDensity_integral line 141
  22. lemma OAI.SingleLatticeCovering.SimplexYoung.integral_pos_of_continuous_density line 179
  23. def OAI.SingleLatticeCovering.SimplexYoung.normalizePositiveDensity line 188
  24. lemma OAI.SingleLatticeCovering.SimplexYoung.simplex_positive_integral line 197
  25. lemma OAI.SingleLatticeCovering.SimplexYoung.simplex_nonneg_integral line 221
  26. lemma OAI.SingleLatticeCovering.SharpYoung.continuous_finTail line 273
  27. lemma OAI.SingleLatticeCovering.SharpYoung.hasCompactSupport_finCons line 277
  28. lemma OAI.SingleLatticeCovering.SharpYoung.hasCompactSupport_finSlice line 288
  29. def OAI.SingleLatticeCovering.SharpYoung.finMarginal line 296
  30. lemma OAI.SingleLatticeCovering.SharpYoung.hasCompactSupport_finMarginal line 299
  31. lemma OAI.SingleLatticeCovering.SharpYoung.continuous_finMarginal line 308
  32. lemma OAI.SingleLatticeCovering.SharpYoung.finMarginal_nonneg line 317
  33. lemma OAI.SingleLatticeCovering.SharpYoung.integral_finMarginal line 320
  34. lemma OAI.SingleLatticeCovering.SharpYoung.lintegral_finCons line 332
  35. def OAI.SingleLatticeCovering.SimplexYoung.simplexSpatial line 352
  36. lemma OAI.SingleLatticeCovering.SimplexYoung.continuous_simplexSpatial line 355
  37. lemma OAI.SingleLatticeCovering.SimplexYoung.simplexSpatial_cons line 360
  38. lemma OAI.SingleLatticeCovering.SimplexYoung.simplex_cc_integral line 368
  39. def OAI.SingleLatticeCovering.SimplexYoung.simplexConfiguration line 437
  40. lemma OAI.SingleLatticeCovering.SimplexYoung.simplexConfiguration_measurable line 440
  41. lemma OAI.SingleLatticeCovering.SimplexYoung.simplex_measure_le_cc line 448
  42. lemma OAI.SingleLatticeCovering.SimplexYoung.volume_simplexConfiguration_le line 467
  43. def OAI.SingleLatticeCovering.SimplexYoung.weightedSimplexConfiguration line 513
  44. def OAI.SingleLatticeCovering.SimplexYoung.simplexDiagonal line 517
  45. lemma OAI.SingleLatticeCovering.SimplexYoung.simplexDiagonal_apply line 521
  46. lemma OAI.SingleLatticeCovering.SimplexYoung.simplexDiagonal_det line 525
  47. def OAI.SingleLatticeCovering.SimplexYoung.scaledCircuitFamily line 533
  48. lemma OAI.SingleLatticeCovering.SimplexYoung.scaledCircuitFamily_compact line 536
  49. lemma OAI.SingleLatticeCovering.SimplexYoung.weightedSimplexConfiguration_preimage line 542
  50. lemma OAI.SingleLatticeCovering.SimplexYoung.volume_scaledCircuitFamily line 561
  51. theorem OAI.SingleLatticeCovering.SimplexYoung.volume_weightedSimplexConfiguration_le line 572
  52. lemma OAI.SingleLatticeCovering.SimplexYoung.weightedCircuitFactor line 600