OAI/MathematicalPhysics/CriticalSK/CubeOverlap.lean

GitHub source file

73 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CriticalSK.latticeOverlap line 54
  2. def OAI.CriticalSK.cubeOverlapMass line 56
  3. lemma OAI.CriticalSK.cubeOverlapMass_nonneg line 58
  4. lemma OAI.CriticalSK.latticeOverlap_mul line 61
  5. lemma OAI.CriticalSK.binomial_exp_term line 68
  6. lemma OAI.CriticalSK.cubeOverlapMass_exp_bound line 74
  7. lemma OAI.CriticalSK.cubeOverlapMass_chernoff line 90
  8. def OAI.CriticalSK.binaryEntropyRate line 108
  9. lemma OAI.CriticalSK.log_cubic_error line 111
  10. lemma OAI.CriticalSK.binaryEntropyRate_taylor line 127
  11. lemma OAI.CriticalSK.log_square_error line 155
  12. lemma OAI.CriticalSK.entropy_error_tendsto line 167
  13. def OAI.CriticalSK.stirlingLogError line 180
  14. lemma OAI.CriticalSK.stirlingLogError_tendsto line 182
  15. lemma OAI.CriticalSK.log_factorial_stirling_exact line 189
  16. lemma OAI.CriticalSK.latticeOverlap_interior line 198
  17. lemma OAI.CriticalSK.latticeOverlap_halves line 208
  18. lemma OAI.CriticalSK.log_cubeOverlapMass_exact line 216
  19. lemma OAI.CriticalSK.cubeOverlapMass_pos line 247
  20. lemma OAI.CriticalSK.cubeOverlapMass_local_limit line 251
  21. def OAI.CriticalSK.scaledOverlapShape line 302
  22. lemma OAI.CriticalSK.sqrt_sub_le_exp line 305
  23. lemma OAI.CriticalSK.scaledOverlapShape_nonneg line 312
  24. lemma OAI.CriticalSK.scaledOverlapShape_bound line 315
  25. lemma OAI.CriticalSK.sqrt_nat_pow line 331
  26. lemma OAI.CriticalSK.sqrt_exp_half line 336
  27. lemma OAI.CriticalSK.scaledOverlapShape_tendsto line 342
  28. lemma OAI.CriticalSK.scaledOverlapShape_integrable line 368
  29. lemma OAI.CriticalSK.scaledOverlapShape_integral_tendsto line 372
  30. lemma OAI.CriticalSK.scaledOverlapShape_eq line 385
  31. lemma OAI.CriticalSK.overlapShape_normalizer_tendsto line 391
  32. lemma OAI.CriticalSK.sphereOverlapShape_pos line 402
  33. lemma OAI.CriticalSK.sphereOverlapShape_log_error line 409
  34. lemma OAI.CriticalSK.sphereOverlapShape_local_limit line 432
  35. def OAI.CriticalSK.sphereOverlapDensity line 451
  36. lemma OAI.CriticalSK.local_overlap_constant line 454
  37. lemma OAI.CriticalSK.local_overlap_const_pos line 460
  38. lemma OAI.CriticalSK.cube_sphere_overlap_local_ratio line 462
  39. lemma OAI.CriticalSK.latticeOverlap_center_bound line 489
  40. lemma OAI.CriticalSK.cube_sphere_overlap_uniform line 508
  41. lemma OAI.CriticalSK.sphereOverlapShape_continuous line 550
  42. lemma OAI.CriticalSK.sphereOverlapShape_nonneg line 554
  43. lemma OAI.CriticalSK.sphereOverlapShape_eq_zero line 558
  44. lemma OAI.CriticalSK.sphereOverlapShape_integrable line 563
  45. lemma OAI.CriticalSK.overlapShape_normalizer_pos line 573
  46. lemma OAI.CriticalSK.sphereOverlapShape_log_variation line 586
  47. lemma OAI.CriticalSK.sphereOverlapDensity_variation line 619
  48. def OAI.CriticalSK.outwardBinLeft line 632
  49. def OAI.CriticalSK.outwardBin line 634
  50. lemma OAI.CriticalSK.outwardBin_distance line 636
  51. lemma OAI.CriticalSK.outwardBin_separated line 654
  52. lemma OAI.CriticalSK.outwardBin_disjoint line 659
  53. lemma OAI.CriticalSK.sphereOverlapDensity_nonneg line 668
  54. lemma OAI.CriticalSK.sphereOverlapDensity_continuous line 671
  55. lemma OAI.CriticalSK.sphereOverlapDensity_mul_integrable line 674
  56. lemma OAI.CriticalSK.outwardBin_integral_const line 687
  57. lemma OAI.CriticalSK.outwardBin_integral_lower line 692
  58. lemma OAI.CriticalSK.latticeOverlap_spacing line 710
  59. lemma OAI.CriticalSK.outwardBin_lattice_disjoint line 719
  60. lemma OAI.CriticalSK.outwardBin_sum_integral_le line 727
  61. lemma OAI.CriticalSK.central_overlap_sum_bound line 737
  62. lemma OAI.CriticalSK.overlap_bin_error_tendsto line 766
  63. lemma OAI.CriticalSK.central_overlap_uniform_bound line 789
  64. def OAI.CriticalSK.overlapCentralCutoff line 827
  65. lemma OAI.CriticalSK.overlapCentralCutoff_tendsto line 829
  66. lemma OAI.CriticalSK.overlapCentralCutoff_fourth line 832
  67. lemma OAI.CriticalSK.overlapCentralCutoff_min line 847
  68. lemma OAI.CriticalSK.integral_shape_on_Ioo line 855
  69. lemma OAI.CriticalSK.overlapShapeMeasure_real_univ line 869
  70. lemma OAI.CriticalSK.normalizedOverlapShape_integral line 876
  71. lemma OAI.CriticalSK.sphereOverlap_density_second_moment line 890
  72. lemma OAI.CriticalSK.rotatedCubePartition_second_lattice line 897
  73. lemma OAI.CriticalSK.normalized_integral_square line 907