OAI/Probability/UnimodularPercolation/Kernel/TraceBounds.lean

GitHub source file

85 declarations, 0 contain sorry, 0 declared as axioms

Trace Bounds for bond percolation.

  1. theorem OAI.Percolation.russoSlope_symm line 18
  2. theorem OAI.Percolation.russoSlope_aut line 27
  3. theorem OAI.Percolation.exists_russoOperator line 39
  4. theorem OAI.Percolation.russoOperator_positiveReal line 56
  5. theorem OAI.Percolation.russoOperator_invariant line 63
  6. theorem OAI.Percolation.PositiveRealMatrix.triple_hasSum line 85
  7. theorem OAI.Percolation.HasKernel.matrixCoeff_re line 108
  8. theorem OAI.Percolation.realTriangle_eq_matrixCoeff line 114
  9. theorem OAI.Percolation.rootTriangle_eq_trace line 122
  10. theorem OAI.Percolation.triangleSlope_eq_matrixCoeff line 129
  11. theorem OAI.Percolation.rootTrace_triangleSlope_cyclic line 156
  12. theorem OAI.Percolation.hasDerivAt_rootTriangle_trace line 170
  13. theorem OAI.Percolation.contactKernel_reroot line 203
  14. theorem OAI.Percolation.contact_lintegral_eq_russoOperator line 240
  15. theorem OAI.Percolation.mixedFunctional_eq_russoTrace line 266
  16. theorem OAI.Percolation.mixedFunctional_toReal_eq_russoTrace line 302
  17. theorem OAI.Percolation.rootTriangle_russo line 331
  18. theorem OAI.Percolation.realTriangle_one_le line 347
  19. theorem OAI.Percolation.rootTriangle_one_le line 356
  20. theorem OAI.Percolation.critical_mixed_trace_bound_real line 379
  21. theorem OAI.Percolation.HasKernel.norm_le_susceptibility_bound line 430
  22. lemma OAI.Percolation.sqrt_mixed_power line 442
  23. lemma OAI.Percolation.sqrt_derivative_estimate line 452
  24. def OAI.Percolation.rootTriangleSqrt line 504
  25. theorem OAI.Percolation.hasDerivAt_rootTriangleSqrt line 507
  26. theorem OAI.Percolation.critical_rootTriangleSqrt_derivative line 519
  27. lemma OAI.Percolation.trace_exponent_choices line 557
  28. lemma OAI.Percolation.trace_scale_large_term line 572
  29. lemma OAI.Percolation.trace_scale_derivative line 582
  30. lemma OAI.Percolation.hasDerivAt_gap_rpow line 609
  31. def OAI.Percolation.traceIntegratingFactor line 616
  32. lemma OAI.Percolation.hasDerivAt_traceIntegratingFactor line 619
  33. lemma OAI.Percolation.traceIntegratingFactor_bounds line 628
  34. lemma OAI.Percolation.hasDerivAt_traceComparison line 639
  35. theorem OAI.Percolation.singular_ode_subpower line 653
  36. theorem OAI.Percolation.critical_rootTriangle_subpower line 720
  37. lemma OAI.Percolation.riccati_step line 788
  38. theorem OAI.Percolation.sprinkling_iterated_bound line 804
  39. lemma OAI.Percolation.closed_power_bound line 823
  40. lemma OAI.Percolation.orParameter_gap_bound line 833
  41. theorem OAI.Percolation.operatorBounded_of_quantitative_gap line 854
  42. theorem OAI.Percolation.norm_gap_lower_of_endpoint_unbounded line 895
  43. def OAI.Percolation.maxSusceptibility line 917
  44. theorem OAI.Percolation.susceptibility_bddAbove line 920
  45. theorem OAI.Percolation.susceptibility_le_max line 928
  46. theorem OAI.Percolation.maxSusceptibility_le line 934
  47. theorem OAI.Percolation.maxSusceptibility_one_le line 940
  48. theorem OAI.Percolation.HasKernel.norm_le_maxSusceptibility line 946
  49. theorem OAI.Percolation.HasKernel.norm_one_le line 954
  50. theorem OAI.Percolation.critical_norm_inverse_lower line 973
  51. theorem OAI.Percolation.critical_normRatio_subpower line 990
  52. inductive OAI.Percolation.HoldingWalk line 1036
  53. def OAI.Percolation.HoldingWalk.withoutHolds line 1045
  54. def OAI.Percolation.HoldingWalk.vertices line 1050
  55. def OAI.Percolation.HoldingWalk.mass line 1055
  56. theorem OAI.Percolation.HoldingWalk.mass_nonneg line 1060
  57. theorem OAI.Percolation.HoldingWalk.length_vertices line 1067
  58. theorem OAI.Percolation.HoldingWalk.withoutHolds_length line 1073
  59. theorem OAI.Percolation.HoldingWalk.withoutHolds_support line 1079
  60. def OAI.Percolation.HoldingWalk.erase line 1087
  61. theorem OAI.Percolation.HoldingWalk.erase_isPath line 1090
  62. theorem OAI.Percolation.HoldingWalk.erase_length line 1093
  63. theorem OAI.Percolation.HoldingWalk.erase_support line 1097
  64. theorem OAI.Percolation.HoldingWalk.erase_edges line 1102
  65. def OAI.Percolation.corridorCounted line 1119
  66. lemma OAI.Percolation.pivotal_restrict_of_conn line 1126
  67. theorem OAI.Percolation.corridorCounted_restrict line 1140
  68. lemma OAI.Percolation.corridorCounted_symm line 1150
  69. theorem OAI.Percolation.measurableSet_corridorCounted line 1159
  70. instance OAI.Percolation.HoldingWalk.countable line 1192
  71. abbrev OAI.Percolation.RawCorridor line 1227
  72. def OAI.Percolation.RawCorridor.base line 1233
  73. def OAI.Percolation.RawCorridor.endpoint line 1234
  74. def OAI.Percolation.RawCorridor.path line 1235
  75. def OAI.Percolation.RawCorridor.interior line 1237
  76. def OAI.Percolation.RawCorridor.retained line 1239
  77. def OAI.Percolation.RawCorridor.blockers line 1240
  78. def OAI.Percolation.RawCorridor.probability line 1242
  79. def OAI.Percolation.RawCorridor.weight line 1243
  80. theorem OAI.Percolation.RawCorridor.path_isPath line 1246
  81. theorem OAI.Percolation.RawCorridor.path_length line 1248
  82. theorem OAI.Percolation.RawCorridor.retained_finite line 1250
  83. theorem OAI.Percolation.RawCorridor.blockers_finite line 1253
  84. theorem OAI.Percolation.RawCorridor.retained_disjoint_blockers line 1258
  85. theorem OAI.Percolation.RawCorridor.weight_nonneg line 1261