OAI/MathematicalPhysics/CriticalSK/Rayleigh.lean

GitHub source file

62 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CriticalSK.abs_spinValue line 18
  2. lemma OAI.CriticalSK.cavityOverlapCoord_abs_le_one line 20
  3. lemma OAI.CriticalSK.cavityNormalization_join line 30
  4. lemma OAI.CriticalSK.cavityOverlap_join line 35
  5. lemma OAI.CriticalSK.incident_variance_bound line 40
  6. lemma OAI.CriticalSK.incident_scaled_product line 46
  7. lemma OAI.CriticalSK.cavity_conditional_mean line 51
  8. lemma OAI.CriticalSK.cavity_conditional_pow line 61
  9. lemma OAI.CriticalSK.cavity_conditional_variance line 72
  10. lemma OAI.CriticalSK.deleteDisorder_continuous line 85
  11. lemma OAI.CriticalSK.localField_continuous line 92
  12. lemma OAI.CriticalSK.cavityNormalization_continuous line 96
  13. lemma OAI.CriticalSK.cavityOverlap_continuous line 102
  14. lemma OAI.CriticalSK.cavity_event_identity line 111
  15. lemma OAI.CriticalSK.cavity_conditional_tail line 115
  16. lemma OAI.CriticalSK.cavity_tail line 127
  17. lemma OAI.CriticalSK.all_cavity_tail line 135
  18. lemma OAI.CriticalSK.cavity_conditional_clipped line 144
  19. lemma OAI.CriticalSK.cavityClipped_measurable line 164
  20. lemma OAI.CriticalSK.cavity_clipped line 167
  21. def OAI.CriticalSK.cavityClippedCount line 175
  22. lemma OAI.CriticalSK.cavityClippedCount_nonneg line 178
  23. lemma OAI.CriticalSK.cavityClippedCount_integrable line 183
  24. lemma OAI.CriticalSK.cavityClippedCount_expectation line 191
  25. lemma OAI.CriticalSK.cavityClippedCount_tail line 207
  26. lemma OAI.CriticalSK.variance_linear_nonneg line 222
  27. lemma OAI.CriticalSK.variance_linear_norm_bound line 224
  28. lemma OAI.CriticalSK.linear_dirichlet_coeff_bound line 228
  29. def OAI.CriticalSK.restrictCoeff line 247
  30. lemma OAI.CriticalSK.restrictCoeff_sum_sq line 249
  31. lemma OAI.CriticalSK.restrictCoeff_linear line 253
  32. lemma OAI.CriticalSK.restrictCoeff_linear_sq line 257
  33. lemma OAI.CriticalSK.variance_linear_split_bound line 264
  34. lemma OAI.CriticalSK.linear_ratio_global_bound line 291
  35. lemma OAI.CriticalSK.linear_ratios_bdd line 304
  36. lemma OAI.CriticalSK.linear_ratios_nonempty line 309
  37. lemma OAI.CriticalSK.linear_ratio_le line 315
  38. lemma OAI.CriticalSK.linearRayleigh_split_bound line 319
  39. lemma OAI.CriticalSK.linearRayleigh_smallBall line 327
  40. lemma OAI.CriticalSK.variance_linear_continuous line 346
  41. lemma OAI.CriticalSK.alphaSite_continuous line 353
  42. lemma OAI.CriticalSK.dirichlet_linear_continuous line 359
  43. lemma OAI.CriticalSK.linear_ratio_continuous line 365
  44. lemma OAI.CriticalSK.linearRayleigh_eq_iSup line 369
  45. lemma OAI.CriticalSK.linearRayleigh_measurable line 380
  46. lemma OAI.CriticalSK.shift_rpow_neg_tendsto line 397
  47. lemma OAI.CriticalSK.cavity_max_rate_identity line 401
  48. lemma OAI.CriticalSK.cavity_count_rate_identity line 408
  49. lemma OAI.CriticalSK.cavity_overlap_rate_identity line 414
  50. lemma OAI.CriticalSK.cavity_overlap_rate_eventually line 424
  51. lemma OAI.CriticalSK.rayleigh_error_rate_identity line 433
  52. lemma OAI.CriticalSK.rayleigh_error_rate_eventually line 438
  53. lemma OAI.CriticalSK.cavity_max_tail_zero line 445
  54. lemma OAI.CriticalSK.cavity_count_tail_zero line 455
  55. lemma OAI.CriticalSK.cavity_overlap_tail_zero line 466
  56. lemma OAI.CriticalSK.rayleigh_cavity_good_bound line 488
  57. lemma OAI.CriticalSK.linearRayleigh_cavity_comparison line 522
  58. lemma OAI.CriticalSK.linearRayleigh_lower_tight line 541
  59. lemma OAI.CriticalSK.linearRayleigh_upper_tight line 557
  60. theorem OAI.CriticalSK.linearRayleigh_natural_scale line 581
  61. lemma OAI.CriticalSK.probability_intersection_tendsto_one line 592
  62. theorem OAI.CriticalSK.covariance_and_linear_tests line 607

    Distinct definitions of this name: ComparatorChallenges/CriticalSK.lean:127 (same statement text; different proof or body). Qualify references as OAI.CriticalSK.covariance_and_linear_tests@path.