OAI/Probability/UnimodularPercolation/Deformation/Derivatives.lean

GitHub source file

69 declarations, 0 contain sorry, 0 declared as axioms

Derivatives for bond percolation.

  1. theorem OAI.Percolation.twoPoint_neighbor_div_bound line 18
  2. theorem OAI.Percolation.neighborhood_twoPoint_bound line 30
  3. def OAI.Percolation.sizeMembership line 61
  4. def OAI.Percolation.sizeWeightedConnectionPotential line 64
  5. theorem OAI.Percolation.sizeMembership_nonneg line 67
  6. theorem OAI.Percolation.sizeMembership_le line 74
  7. theorem OAI.Percolation.measurable_sizeMembership line 81
  8. theorem OAI.Percolation.integrable_sizeMembership line 86
  9. theorem OAI.Percolation.integral_sizeMembership_le_susceptibility line 95
  10. theorem OAI.Percolation.sizeWeightedConnectionPotential_eq_finite line 103
  11. theorem OAI.Percolation.summable_sizePotential_integral_norm line 130
  12. theorem OAI.Percolation.integrable_sizeWeightedConnectionPotential line 141
  13. theorem OAI.Percolation.sizeWeightedConnectionPotential_nonneg line 159
  14. theorem OAI.Percolation.summable_twoPoint_cube_pair line 163
  15. theorem OAI.Percolation.integral_sizeWeightedConnectionPotential_le line 173
  16. theorem OAI.Percolation.deformedFreshExteriorMoment_lower line 206
  17. theorem OAI.Percolation.deformed_distinct_correlation line 263
  18. theorem OAI.Percolation.HasKernel.square_real_kernel line 303
  19. theorem OAI.Percolation.HasKernel.cube_real_kernel line 309
  20. theorem OAI.Percolation.deformed_distinct_correlation_uniform line 335
  21. theorem OAI.Percolation.incidentSupport_card_le line 365
  22. theorem OAI.Percolation.reachBall_ncard_le_pow line 373
  23. theorem OAI.Percolation.RawCorridor.interior_card_le line 398
  24. theorem OAI.Percolation.RawCorridor.blockers_ncard_le line 412
  25. theorem OAI.Percolation.walkKernel_finite_support line 434
  26. theorem OAI.Percolation.walkKernel_tsum line 442
  27. theorem OAI.Percolation.raw_integral_one line 450
  28. theorem OAI.Percolation.rawFrom_probability_sum line 468
  29. theorem OAI.Percolation.raw_probability_on_bases_sum line 483
  30. theorem OAI.Percolation.RawCorridor.base_mem_reachBall_of_retained line 511
  31. theorem OAI.Percolation.RawCorridor.counted_base_mem_cluster line 523
  32. def OAI.Percolation.rawWeightBase line 541
  33. theorem OAI.Percolation.rawWeightBase_one_le line 543
  34. theorem OAI.Percolation.RawCorridor.weight_le_uniform line 551
  35. theorem OAI.Percolation.summable_raw_selection line 589
  36. theorem OAI.Percolation.mask_le_mask_mul line 599
  37. theorem OAI.Percolation.raw_weight_sum_le_on_bases line 609
  38. theorem OAI.Percolation.corridorPenalty_le_cluster line 634
  39. theorem OAI.Percolation.raw_edge_weight_bound line 646
  40. theorem OAI.Percolation.pow_le_exp_div_self line 672
  41. theorem OAI.Percolation.exists_uniform_corridor_edge_cost line 684
  42. def OAI.Percolation.deformedDerivativeMass line 717
  43. theorem OAI.Percolation.deformedConnection_eq_zero_of_not_conn line 721
  44. theorem OAI.Percolation.deformedClusterMass_eq_sum line 727
  45. theorem OAI.Percolation.deformedDerivativeMass_eq_sum line 735
  46. theorem OAI.Percolation.measurable_deformedDerivativeMass line 743
  47. theorem OAI.Percolation.deformedDerivativeMass_nonneg line 749
  48. theorem OAI.Percolation.hasDerivAt_deformedConnection line 755
  49. theorem OAI.Percolation.hasDerivAt_deformedClusterMass line 767
  50. theorem OAI.Percolation.deformedDerivativeMass_le_square line 787
  51. theorem OAI.Percolation.integrable_deformedDerivativeMass line 806
  52. theorem OAI.Percolation.hasDerivAt_deformedSusceptibility line 834
  53. theorem OAI.Percolation.continuous_deformedConnection line 879
  54. theorem OAI.Percolation.continuous_deformedClusterMass line 884
  55. theorem OAI.Percolation.continuous_deformedDerivativeMass line 889
  56. theorem OAI.Percolation.continuousOn_integral_deformedDerivativeMass line 897
  57. theorem OAI.Percolation.continuousOn_deformedSusceptibility line 928
  58. theorem OAI.Percolation.hasDerivWithinAt_deformedSusceptibility_zero line 948
  59. theorem OAI.Percolation.RawCorridor.counted_move_terminal line 980
  60. theorem OAI.Percolation.corridorPenaltyTerm_move_bound line 1001
  61. theorem OAI.Percolation.summable_raw_edge_weights line 1034
  62. theorem OAI.Percolation.corridorPenalty_move_bound line 1047
  63. theorem OAI.Percolation.measurable_union_const line 1073
  64. theorem OAI.Percolation.measurableSet_finite_open line 1079
  65. theorem OAI.Percolation.finite_open_integral_lower line 1088
  66. theorem OAI.Percolation.corridorPenalty_move_edge_cost line 1134
  67. theorem OAI.Percolation.deformedConnection_move_lower line 1146
  68. theorem OAI.Percolation.deformedKernel_move_lower line 1182
  69. theorem OAI.Percolation.deformedSusceptibility_move_lower line 1207