OAI/MathematicalPhysics/CriticalSK/CubeRestriction.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CriticalSK.rotatedCubePair line 73
  2. lemma OAI.CriticalSK.rotatedCubePair_continuous line 79
  3. lemma OAI.CriticalSK.rotatedCubePair_haar line 88
  4. lemma OAI.CriticalSK.rotatedCubePair_lattice line 111
  5. lemma OAI.CriticalSK.squaredPairMoment_mono_abs line 122
  6. lemma OAI.CriticalSK.sphereOverlap_density_weighted_moment line 128
  7. lemma OAI.CriticalSK.orthogonal_radial_integral line 138
  8. lemma OAI.CriticalSK.sphereRestricted_as_tilted line 158
  9. def OAI.CriticalSK.rotatedCubeRestricted line 178
  10. lemma OAI.CriticalSK.rotatedCubeRestricted_measurable line 184
  11. lemma OAI.CriticalSK.rotatedCubeRestricted_nonneg line 195
  12. lemma OAI.CriticalSK.rotatedCubeRestricted_le line 200
  13. lemma OAI.CriticalSK.rotatedCubeRestricted_integrable line 210
  14. lemma OAI.CriticalSK.rotatedCubeRestricted_first_moment line 218
  15. lemma OAI.CriticalSK.divided_mass_variance_bound line 250
  16. lemma OAI.CriticalSK.normalized_pair_event_bound line 264
  17. lemma OAI.CriticalSK.integral_dominates_event line 282
  18. lemma OAI.CriticalSK.rotatedCubePartition_pos line 290
  19. def OAI.CriticalSK.rotatedCubeSmallBall line 296
  20. lemma OAI.CriticalSK.rotatedCubeSmallBall_measurable line 300
  21. lemma OAI.CriticalSK.rotatedCubeSmallBall_nonneg line 304
  22. lemma OAI.CriticalSK.rotatedCubeSmallBall_le_one line 308
  23. lemma OAI.CriticalSK.rotatedCubeSmallBall_integrable line 312
  24. lemma OAI.CriticalSK.rotatedCubeSmallBall_expectation line 319
  25. def OAI.CriticalSK.rotatedCubeOverlap line 341
  26. lemma OAI.CriticalSK.rotatedCubePair_square_nonneg line 345
  27. lemma OAI.CriticalSK.rotatedCubeOverlap_probability line 350