OAI/Analysis/Triangular/Energy/Mixtures.lean

GitHub source file

106 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.TriangularUniversal.b line 9
  2. def OAI.TriangularUniversal.nodeResidues line 11
  3. def OAI.TriangularUniversal.IsPositiveNode line 13
  4. lemma OAI.TriangularUniversal.sqrt_three_pos line 16
  5. lemma OAI.TriangularUniversal.scale_pos line 17
  6. lemma OAI.TriangularUniversal.b_pos line 18
  7. lemma OAI.TriangularUniversal.triangularPoint_coord_zero line 20
  8. lemma OAI.TriangularUniversal.triangularPoint_coord_one line 24
  9. lemma OAI.TriangularUniversal.triangularPoint_norm_sq line 28
  10. lemma OAI.TriangularUniversal.triangularPoint_injective line 41
  11. lemma OAI.TriangularUniversal.triangularPoint_zero line 63
  12. lemma OAI.TriangularUniversal.triangularPoint_sub line 67
  13. lemma OAI.TriangularUniversal.eisenstein_mod_twelve line 72
  14. lemma OAI.TriangularUniversal.eisenstein_mod_twelve_int line 77
  15. lemma OAI.TriangularUniversal.triangular_shell_node line 98
  16. lemma OAI.TriangularUniversal.triangularLattice_sub line 129
  17. lemma OAI.TriangularUniversal.diskPoints_subset line 135
  18. lemma OAI.TriangularUniversal.finite_lattice_row_le line 143
  19. lemma OAI.TriangularUniversal.lattice_disk_energy_le line 167
  20. lemma OAI.TriangularUniversal.lattice_energy_upper line 190
  21. def OAI.TriangularUniversal.triangularEquiv line 195
  22. def OAI.TriangularUniversal.triangularBasis line 217
  23. def OAI.TriangularUniversal.triangularModule line 220
  24. lemma OAI.TriangularUniversal.triangularPoint_equiv line 223
  25. lemma OAI.TriangularUniversal.triangularModule_coe line 226
  26. instance OAI.TriangularUniversal.(instance at line 252) line 252
  27. instance OAI.TriangularUniversal.(instance at line 255) line 255
  28. lemma OAI.TriangularUniversal.triangular_locallyFinite line 258
  29. lemma OAI.TriangularUniversal.triangularBasis_apply line 263
  30. lemma OAI.TriangularUniversal.triangular_det line 267
  31. lemma OAI.TriangularUniversal.triangular_covolume line 279
  32. lemma OAI.TriangularUniversal.diskCount_eq_card line 290
  33. lemma OAI.TriangularUniversal.norm_square_sublevel line 296
  34. lemma OAI.TriangularUniversal.triangular_count_asymptotic line 303
  35. lemma OAI.TriangularUniversal.triangular_densityOne line 332
  36. lemma OAI.TriangularUniversal.mem_diskPoints_iff line 338
  37. lemma OAI.TriangularUniversal.triangular_count_pos line 342
  38. lemma OAI.TriangularUniversal.lattice_interior_count_ratio line 347
  39. lemma OAI.TriangularUniversal.lattice_interior_count_ratio_ennreal line 375
  40. abbrev OAI.TriangularUniversal.NonzeroSite line 388
  41. lemma OAI.TriangularUniversal.finite_lattice_row_ge line 390
  42. lemma OAI.TriangularUniversal.finite_lattice_disk_energy_ge line 420
  43. lemma OAI.TriangularUniversal.lattice_energy_lower line 446
  44. lemma OAI.TriangularUniversal.lattice_energy_eq line 461
  45. def OAI.TriangularUniversal.PositiveMixture.difference line 472
  46. def OAI.TriangularUniversal.PositiveMixture.momentFunctional line 476
  47. lemma OAI.TriangularUniversal.PositiveMixture.moment_monomial line 479
  48. lemma OAI.TriangularUniversal.PositiveMixture.moment_pow line 483
  49. lemma OAI.TriangularUniversal.PositiveMixture.moment_difference line 487
  50. lemma OAI.TriangularUniversal.PositiveMixture.moment_bernstein line 496
  51. def OAI.TriangularUniversal.PositiveMixture.weight line 504
  52. lemma OAI.TriangularUniversal.PositiveMixture.weight_nonneg line 507
  53. lemma OAI.TriangularUniversal.PositiveMixture.weight_sum line 510
  54. def OAI.TriangularUniversal.PositiveMixture.bernsteinBasis line 516
  55. lemma OAI.TriangularUniversal.PositiveMixture.bernsteinBasis_sum line 519
  56. lemma OAI.TriangularUniversal.PositiveMixture.bernsteinBasis_nonneg line 530
  57. lemma OAI.TriangularUniversal.PositiveMixture.choose_ratio line 535
  58. lemma OAI.TriangularUniversal.PositiveMixture.bernstein_monomial line 546
  59. lemma OAI.TriangularUniversal.PositiveMixture.weighted_binomial_moment line 580
  60. abbrev OAI.TriangularUniversal.PositiveMixture.I line 591
  61. def OAI.TriangularUniversal.PositiveMixture.coordinate line 593
  62. def OAI.TriangularUniversal.PositiveMixture.falling line 595
  63. lemma OAI.TriangularUniversal.PositiveMixture.falling_tendsto line 598
  64. lemma OAI.TriangularUniversal.PositiveMixture.falling_grid line 609
  65. def OAI.TriangularUniversal.PositiveMixture.gridMeasure line 637
  66. instance OAI.TriangularUniversal.PositiveMixture.gridMeasure_finite line 640
  67. def OAI.TriangularUniversal.PositiveMixture.gridFiniteMeasure line 646
  68. lemma OAI.TriangularUniversal.PositiveMixture.gridMeasure_mass line 649
  69. lemma OAI.TriangularUniversal.PositiveMixture.gridFiniteMeasure_mass line 658
  70. lemma OAI.TriangularUniversal.PositiveMixture.integral_grid line 666
  71. lemma OAI.TriangularUniversal.PositiveMixture.integral_falling line 676
  72. lemma OAI.TriangularUniversal.PositiveMixture.grid_moments_tendsto line 685
  73. theorem OAI.TriangularUniversal.PositiveMixture.hausdorff line 701
  74. def OAI.TriangularUniversal.PositiveMixture.CM line 718
  75. lemma OAI.TriangularUniversal.PositiveMixture.CM.deriv_differentiableOn line 722
  76. lemma OAI.TriangularUniversal.PositiveMixture.CM.signed_antitone line 728
  77. lemma OAI.TriangularUniversal.PositiveMixture.CM.shift line 741
  78. lemma OAI.TriangularUniversal.PositiveMixture.CM.sub_shift line 749
  79. lemma OAI.TriangularUniversal.PositiveMixture.difference_shift line 761
  80. lemma OAI.TriangularUniversal.PositiveMixture.CM.sample_difference line 767
  81. abbrev OAI.TriangularUniversal.PositiveMixture.Positive line 781
  82. def OAI.TriangularUniversal.PositiveMixture.powerTest line 783
  83. lemma OAI.TriangularUniversal.PositiveMixture.continuous_powerTest line 786
  84. def OAI.TriangularUniversal.PositiveMixture.unitPower line 791
  85. lemma OAI.TriangularUniversal.PositiveMixture.mass_map_unitPower line 795
  86. lemma OAI.TriangularUniversal.PositiveMixture.integral_power_map line 799
  87. def OAI.TriangularUniversal.PositiveMixture.gridTime line 813
  88. lemma OAI.TriangularUniversal.PositiveMixture.gridTime_pos line 815
  89. lemma OAI.TriangularUniversal.PositiveMixture.gridTime_tendsto line 819
  90. theorem OAI.TriangularUniversal.PositiveMixture.mixture_of_differences line 829
  91. theorem OAI.TriangularUniversal.PositiveMixture.CM.shifted_mixture line 889
  92. def OAI.TriangularUniversal.powerPotential line 906
  93. lemma OAI.TriangularUniversal.powerPotential_continuous line 908
  94. lemma OAI.TriangularUniversal.measurable_diskEnergy_power line 912
  95. lemma OAI.TriangularUniversal.lintegral_power_eq line 922
  96. lemma OAI.TriangularUniversal.lintegral_diskEnergy_power line 931
  97. lemma OAI.TriangularUniversal.mixture_energy_lower line 961
  98. instance OAI.TriangularUniversal.nonzeroSite_countable line 969
  99. lemma OAI.TriangularUniversal.lintegral_latticeEnergy_power line 972
  100. theorem OAI.TriangularUniversal.shifted_mixture_energy line 984
  101. lemma OAI.TriangularUniversal.potential_antitone line 998
  102. lemma OAI.TriangularUniversal.diskEnergy_mono line 1002
  103. lemma OAI.TriangularUniversal.energy_mono line 1009
  104. lemma OAI.TriangularUniversal.latticeEnergy_mono line 1013
  105. lemma OAI.TriangularUniversal.shifted_energy_le line 1019
  106. lemma OAI.TriangularUniversal.latticeEnergy_shift_iSup line 1026