OAI/Probability/UnimodularPercolation/Deformation/AveragedDecrease.lean

GitHub source file

70 declarations, 0 contain sorry, 0 declared as axioms

Averaged Decrease for bond percolation.

  1. theorem OAI.Percolation.preimage_diff_singleton line 17
  2. theorem OAI.Percolation.corridorCounted_aut line 22
  3. theorem OAI.Percolation.RawCorridor.aut_counted line 48
  4. theorem OAI.Percolation.corridorPenaltyTerm_aut line 61
  5. theorem OAI.Percolation.corridorPenalty_aut line 68
  6. theorem OAI.Percolation.deformedConnection_aut line 88
  7. theorem OAI.Percolation.deformedKernel_aut line 96
  8. theorem OAI.Percolation.deformedSusceptibility_aut line 106
  9. def OAI.Percolation.corridorDerivativeContribution line 117
  10. theorem OAI.Percolation.corridorDerivativeContribution_nonneg line 122
  11. theorem OAI.Percolation.corridorDerivativeContribution_aut line 127
  12. theorem OAI.Percolation.derivative_field_summable line 153
  13. theorem OAI.Percolation.derivative_field_sum line 179
  14. theorem OAI.Percolation.derivative_contribution_sum line 190
  15. theorem OAI.Percolation.raw_from_sum_eq_masked line 225
  16. def OAI.Percolation.derivativeTransportMass line 240
  17. theorem OAI.Percolation.derivativeTransportMass_nonneg line 245
  18. theorem OAI.Percolation.derivativeTransportMass_aut line 250
  19. theorem OAI.Percolation.summable_swapped_real line 280
  20. theorem OAI.Percolation.derivativeTransportMass_row line 285
  21. theorem OAI.Percolation.derivativeTransportMass_column line 304
  22. theorem OAI.Percolation.averaged_derivative_transport line 341
  23. def OAI.Percolation.averagedDeformedSusceptibility line 360
  24. theorem OAI.Percolation.hasDerivAt_averagedDeformedSusceptibility line 364
  25. def OAI.Percolation.rawPathAverage line 390
  26. theorem OAI.Percolation.rawPathAverage_mono line 395
  27. theorem OAI.Percolation.rawPathAverage_sub line 409
  28. theorem OAI.Percolation.rawPathAverage_const_mul line 425
  29. def OAI.Percolation.retainedSusceptibilityProduct line 431
  30. theorem OAI.Percolation.raw_derivative_template_row_lower line 451
  31. theorem OAI.Percolation.averaged_derivative_raw_lower line 481
  32. theorem OAI.Percolation.rawPathAverage_operator_trace line 526
  33. theorem OAI.Percolation.rawPathAverage_operator_le_norm line 554
  34. theorem OAI.Percolation.exists_uniform_averaged_decrease line 602
  35. theorem OAI.Percolation.exists_uniform_deformed_row_comparison line 652
  36. def OAI.Percolation.segmentOrbit line 713
  37. theorem OAI.Percolation.segmentOrbit_aut_iff line 717
  38. theorem OAI.Percolation.finite_segmentAnchors line 729
  39. def OAI.Percolation.segmentAnchors line 738
  40. theorem OAI.Percolation.mem_segmentAnchors line 742
  41. theorem OAI.Percolation.segmentAnchors_nonempty_iff line 747
  42. def OAI.Percolation.segmentAut line 768
  43. theorem OAI.Percolation.segmentAnchors_map line 774
  44. theorem OAI.Percolation.segmentAnchors_card_aut line 791
  45. def OAI.Percolation.anchoredPositionKernel line 799
  46. theorem OAI.Percolation.anchoredPositionKernel_nonneg line 804
  47. theorem OAI.Percolation.anchoredPositionKernel_aut line 811
  48. theorem OAI.Percolation.anchoredPositionKernel_hasSum line 831
  49. theorem OAI.Percolation.anchoredPositionKernel_eq_zero_off_ball line 850
  50. theorem OAI.Percolation.anchoredPositionKernel_eq_zero_off_orbits line 862
  51. theorem OAI.Percolation.anchoredPositionKernel_columnSummable line 887
  52. theorem OAI.Percolation.anchoredPositionKernel_column_orbit line 902
  53. theorem OAI.Percolation.anchoredPositionKernel_column_mass line 920
  54. theorem OAI.Percolation.anchoredPositionKernel_column_ratio line 948
  55. theorem OAI.Percolation.exists_operator_of_unit_row_column_bound line 976
  56. theorem OAI.Percolation.exists_anchoredPositionOperator line 1054
  57. theorem OAI.Percolation.exists_anchoredPositionOperator_uniform line 1080
  58. def OAI.Percolation.HoldingWalk.snocHold line 1119
  59. def OAI.Percolation.HoldingWalk.snocStep line 1125
  60. def OAI.Percolation.HoldingWalk.reverse line 1132
  61. theorem OAI.Percolation.HoldingWalk.reverse_snocHold line 1137
  62. theorem OAI.Percolation.HoldingWalk.reverse_snocStep line 1144
  63. theorem OAI.Percolation.HoldingWalk.reverse_reverse line 1151
  64. def OAI.Percolation.HoldingWalk.reverseEquiv line 1157
  65. theorem OAI.Percolation.HoldingWalk.mass_snocHold line 1163
  66. theorem OAI.Percolation.HoldingWalk.mass_snocStep line 1170
  67. theorem OAI.Percolation.HoldingWalk.mass_reverse line 1177
  68. theorem OAI.Percolation.HoldingWalk.vertices_snocHold line 1184
  69. theorem OAI.Percolation.HoldingWalk.vertices_snocStep line 1191
  70. theorem OAI.Percolation.HoldingWalk.vertices_reverse line 1198