OAI/Probability/UnimodularPercolation/Kernel/Spectral.lean

GitHub source file

90 declarations, 0 contain sorry, 0 declared as axioms

Isoperimetric energy, symmetric walks and invariant operator traces.

  1. def OAI.Percolation.levelIndicator line 19
  2. theorem OAI.Percolation.levelIndicator_eq line 21
  3. theorem OAI.Percolation.integrable_levelIndicator line 26
  4. theorem OAI.Percolation.integral_levelIndicator line 32
  5. theorem OAI.Percolation.abs_sub_levelIndicator line 37
  6. theorem OAI.Percolation.integrable_abs_sub_levelIndicator line 63
  7. theorem OAI.Percolation.integral_abs_sub_levelIndicator line 67
  8. theorem OAI.Percolation.finite_coarea_lower_bound line 75
  9. theorem OAI.Percolation.hV_mul_card_le line 110
  10. theorem OAI.Percolation.finite_vertexBoundary line 123
  11. def OAI.Percolation.neighbors line 129
  12. theorem OAI.Percolation.mem_neighbors line 132
  13. def OAI.Percolation.neighborClosure line 135
  14. theorem OAI.Percolation.subset_neighborClosure line 138
  15. theorem OAI.Percolation.neighbor_mem_neighborClosure line 141
  16. def OAI.Percolation.finiteAdjPairs line 146
  17. theorem OAI.Percolation.mem_finiteAdjPairs line 149
  18. theorem OAI.Percolation.adj_symm line 153
  19. theorem OAI.Percolation.sum_swap_finiteAdjPairs line 157
  20. theorem OAI.Percolation.finiteAdjPairs_cut_bound line 173
  21. theorem OAI.Percolation.bondGraph_coarea line 216
  22. theorem OAI.Percolation.neighbors_card_le_degree line 224
  23. theorem OAI.Percolation.finiteAdjPairs_source_sum_le line 236
  24. theorem OAI.Percolation.finiteAdjPairs_square_sum_le line 255
  25. theorem OAI.Percolation.bondGraph_cheeger_energy line 284
  26. theorem OAI.Percolation.finiteEmbedding_inner_left line 323
  27. theorem OAI.Percolation.finiteEmbedding_inner_right line 328
  28. theorem OAI.Percolation.finiteEmbedding_norm_sq line 333
  29. theorem OAI.Percolation.kernel_finiteEmbedding line 342
  30. theorem OAI.Percolation.symmetric_of_symmetric_kernel line 352
  31. theorem OAI.Percolation.norm_le_of_finite_quadratic line 371
  32. theorem OAI.Percolation.abs_inner_kernel_finite_le line 388
  33. def OAI.Percolation.walkKernel line 413
  34. theorem OAI.Percolation.walkKernel_symmetric line 418
  35. theorem OAI.Percolation.walkKernel_nonneg line 425
  36. theorem OAI.Percolation.walkKernel_row_sum line 434
  37. theorem OAI.Percolation.walkKernel_row_bound line 451
  38. theorem OAI.Percolation.exists_walk_operator line 468
  39. theorem OAI.Percolation.finiteAdjPairs_sum line 481
  40. theorem OAI.Percolation.finiteAdjPairs_source_sum line 486
  41. theorem OAI.Percolation.finiteAdjPairs_product_sum line 507
  42. theorem OAI.Percolation.walkKernel_energy line 524
  43. theorem OAI.Percolation.walkKernel_quadratic_bound line 572
  44. theorem OAI.Percolation.walk_operator_norm_lt_one line 592
  45. theorem OAI.Percolation.exists_strict_walk_operator line 623
  46. theorem OAI.Percolation.equivalenceMatrix_posSemidef line 647
  47. theorem OAI.Percolation.connection_quadratic_nonneg line 660
  48. theorem OAI.Percolation.conn_indicator_integrable line 687
  49. theorem OAI.Percolation.twoPoint_eq_integral line 692
  50. theorem OAI.Percolation.twoPoint_quadratic_nonneg line 699
  51. theorem OAI.Percolation.HasKernel.isPositive line 720
  52. def OAI.Percolation.permuteHilbert line 766
  53. theorem OAI.Percolation.permuteHilbert_apply line 782
  54. theorem OAI.Percolation.permuteHilbert_single line 785
  55. def OAI.Percolation.matrixCoeff line 791
  56. theorem OAI.Percolation.matrixCoeff_eq_inner line 794
  57. theorem OAI.Percolation.operator_kernel_hasSum line 798
  58. theorem OAI.Percolation.matrixCoeff_mul line 813
  59. theorem OAI.Percolation.matrixCoeff_adjoint line 817
  60. theorem OAI.Percolation.matrixCoeff_invariant_iff line 826
  61. theorem OAI.Percolation.matrixCoeff_sqrt_invariant line 856
  62. theorem OAI.Percolation.matrixCoeff_mul_invariant line 863
  63. theorem OAI.Percolation.matrixCoeff_nonneg line 872
  64. theorem OAI.Percolation.matrixCoeff_mono line 877
  65. def OAI.Percolation.rootTrace line 887
  66. theorem OAI.Percolation.rootTrace_add line 890
  67. theorem OAI.Percolation.rootTrace_smul line 894
  68. theorem OAI.Percolation.rootTrace_nonneg line 898
  69. theorem OAI.Percolation.rootTrace_mono line 903
  70. theorem OAI.Percolation.rootTrace_one line 910
  71. def OAI.Percolation.KernelInvariant line 916
  72. theorem OAI.Percolation.KernelInvariant.mul line 919
  73. theorem OAI.Percolation.KernelInvariant.star line 926
  74. theorem OAI.Percolation.KernelInvariant.sqrt line 932
  75. def OAI.Percolation.RootTransport line 940
  76. theorem OAI.Percolation.rootTrace_cyclic line 947
  77. theorem OAI.Percolation.rootTrace_diag_le line 960
  78. theorem OAI.Percolation.rootTrace_real_smul line 987
  79. theorem OAI.Percolation.rootTrace_positive_mul_le line 992
  80. theorem OAI.Percolation.rootTrace_conjugate_le line 1016
  81. theorem OAI.Percolation.matrixCoeff_gram line 1035
  82. theorem OAI.Percolation.matrixCoeff_gram_norm_sq_le line 1043
  83. theorem OAI.Percolation.matrixCoeff_positive_product_norm_sq_le line 1053
  84. theorem OAI.Percolation.matrixCoeff_smoothing line 1065
  85. def OAI.Percolation.vertexAut line 1105
  86. theorem OAI.Percolation.twoPoint_aut line 1107
  87. theorem OAI.Percolation.HasKernel.invariant line 1118
  88. theorem OAI.Percolation.KernelInvariant.one line 1125
  89. theorem OAI.Percolation.KernelInvariant.pow line 1131
  90. theorem OAI.Percolation.twoPoint_operator_smoothing line 1140