OAI/MathematicalPhysics/CriticalSK/TriNoise.lean

GitHub source file

63 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CriticalSK.scaleLength line 42
2. def OAI.CriticalSK.scaleRoot line 44
3. def OAI.CriticalSK.scaleEnergy line 46
4. lemma OAI.CriticalSK.scaleLength_pos line 48
5. lemma OAI.CriticalSK.scaleRoot_pos line 52
6. lemma OAI.CriticalSK.scaleEnergy_pos line 56
7. lemma OAI.CriticalSK.scale_length_root_eq_one line 58
8. lemma OAI.CriticalSK.scale_last line 64
9. lemma OAI.CriticalSK.scale_length_root line 69
10. lemma OAI.CriticalSK.scaleEnergy_step line 79
11. lemma OAI.CriticalSK.energy_first_scale line 84
12. lemma OAI.CriticalSK.scale_shell_geometry line 102
13. lemma OAI.CriticalSK.dyadic_cube_scale line 120
14. lemma OAI.CriticalSK.natural_le_exponential_quarter line 141
15. lemma OAI.CriticalSK.block_scale_factor line 152
16. lemma OAI.CriticalSK.scale_block_factor line 177
17. lemma OAI.CriticalSK.scale_weight_absorption line 184
18. lemma OAI.CriticalSK.good_scale_prefix line 227
19. lemma OAI.CriticalSK.selected_scale_form_bound line 240
20. lemma OAI.CriticalSK.centered_square_form_good line 261
21. lemma OAI.CriticalSK.centered_product_form_good line 283
22. lemma OAI.CriticalSK.edgeCoeff_sqrt_div line 306
23. lemma OAI.CriticalSK.chi_scaled_bias_bound line 314
24. lemma OAI.CriticalSK.weighted_neighbor_sum line 359
25. lemma OAI.CriticalSK.weighted_edge_form line 380
26. lemma OAI.CriticalSK.chi_mean_form_bias line 418
27. def OAI.CriticalSK.entryVariance line 436
28. lemma OAI.CriticalSK.entryVariance_pos line 438
29. lemma OAI.CriticalSK.subGaussian_enlarge line 442
30. lemma OAI.CriticalSK.diagonalRows_common_subGaussian line 448
31. abbrev OAI.CriticalSK.TriSample line 456
32. def OAI.CriticalSK.triLaw line 458
33. instance OAI.CriticalSK.(instance at line 460) line 460
34. def OAI.CriticalSK.entryBad line 464
35. def OAI.CriticalSK.triBad line 468
36. lemma OAI.CriticalSK.entryBad_measurable line 472
37. lemma OAI.CriticalSK.triBad_measurable line 476
38. lemma OAI.CriticalSK.triBad_probability line 480
39. def OAI.CriticalSK.triForm line 503
40. lemma OAI.CriticalSK.triForm_decomposition line 508
41. def OAI.CriticalSK.formError line 535
42. lemma OAI.CriticalSK.triForm_good line 540
43. instance OAI.CriticalSK.(instance at line 576) line 576
44. instance OAI.CriticalSK.(instance at line 580) line 580
45. instance OAI.CriticalSK.(instance at line 584) line 584
46. instance OAI.CriticalSK.(instance at line 588) line 588
47. instance OAI.CriticalSK.(instance at line 592) line 592
48. instance OAI.CriticalSK.(instance at line 596) line 596
49. instance OAI.CriticalSK.(instance at line 600) line 600
50. instance OAI.CriticalSK.(instance at line 604) line 604
51. instance OAI.CriticalSK.(instance at line 608) line 608
52. instance OAI.CriticalSK.(instance at line 612) line 612
53. instance OAI.CriticalSK.(instance at line 616) line 616
54. instance OAI.CriticalSK.(instance at line 620) line 620
55. instance OAI.CriticalSK.(instance at line 624) line 624
56. instance OAI.CriticalSK.(instance at line 628) line 628
57. instance OAI.CriticalSK.(instance at line 632) line 632
58. instance OAI.CriticalSK.(instance at line 636) line 636
59. instance OAI.CriticalSK.(instance at line 640) line 640
60. instance OAI.CriticalSK.(instance at line 644) line 644
61. instance OAI.CriticalSK.(instance at line 648) line 648
62. instance OAI.CriticalSK.(instance at line 652) line 652
63. instance OAI.CriticalSK.(instance at line 656) line 656