OAI/Probability/UnimodularPercolation/Kernel/ScaleBudget.lean

GitHub source file

65 declarations, 0 contain sorry, 0 declared as axioms

Scale Budget for bond percolation.

  1. theorem OAI.Percolation.integral_tsum_of_finite_support line 18
  2. theorem OAI.Percolation.binOrbitTransportMass_local line 27
  3. theorem OAI.Percolation.binOrbitTransportMass_integrable line 42
  4. theorem OAI.Percolation.binOrbitTransportMass_outside line 46
  5. def OAI.Percolation.binOrbitTransport line 50
  6. theorem OAI.Percolation.binOrbitTransport_covariant line 53
  7. theorem OAI.Percolation.binOrbitTransport_outside line 63
  8. theorem OAI.Percolation.binOrbitTransportMass_outside_column line 67
  9. theorem OAI.Percolation.binOrbitTransport_row_integral line 74
  10. theorem OAI.Percolation.integral_binOrbitRowMass line 83
  11. theorem OAI.Percolation.binOrbitTransport_column line 103
  12. theorem OAI.Percolation.binOrbitTransport_row_lower line 125
  13. theorem OAI.Percolation.weighted_binOrbitRow_lower line 156
  14. theorem OAI.Percolation.exists_binOrbitRow_lower line 185
  15. theorem OAI.Percolation.summable_dyadic_of_scaled_bound line 214
  16. theorem OAI.Percolation.unbounded_scaled_dyadic line 232
  17. theorem OAI.Percolation.late_record_of_unbounded line 241
  18. theorem OAI.Percolation.finite_family_unbounded_choice line 256
  19. theorem OAI.Percolation.record_dyadic_bounds line 265
  20. theorem OAI.Percolation.clusterWindowProbability_split line 294
  21. def OAI.Percolation.weightedWindowProbability line 316
  22. theorem OAI.Percolation.weightedWindowProbability_nonneg line 320
  23. theorem OAI.Percolation.weightedWindowProbability_split line 326
  24. def OAI.Percolation.dyadicBinProbability line 334
  25. theorem OAI.Percolation.orbit_dyadic_scales line 340
  26. theorem OAI.Percolation.measurable_cluster_ncard line 396
  27. theorem OAI.Percolation.integrable_cluster_power_of_dyadic line 432
  28. theorem OAI.Percolation.integrable_cluster_power_of_weighted_dyadic line 496
  29. theorem OAI.Percolation.orbit_scales_of_divergent_moment line 526
  30. def OAI.Percolation.logarithmicChainLength line 554
  31. theorem OAI.Percolation.logarithmicChainLength_bounds line 556
  32. theorem OAI.Percolation.tendsto_logarithmicChainLength line 565
  33. theorem OAI.Percolation.tendsto_log_div_chainLength line 569
  34. theorem OAI.Percolation.tendsto_chainLength_div_scale line 585
  35. theorem OAI.Percolation.eventually_chain_volume_small line 598
  36. theorem OAI.Percolation.amplificationMomentFactor_ge_four line 619
  37. theorem OAI.Percolation.amplificationMomentFactor_cubic line 626
  38. theorem OAI.Percolation.tendsto_log_amplificationMomentFactor_div line 654
  39. theorem OAI.Percolation.eventually_inverseCodeMass_budget line 687
  40. theorem OAI.Percolation.code_bound_of_logarithmic_chain line 706
  41. theorem OAI.Percolation.tendsto_rpow_mul_stretched_exp line 720
  42. theorem OAI.Percolation.eventually_amplification_goodness_decay line 738
  43. theorem OAI.Percolation.log_inv_success_le line 790
  44. theorem OAI.Percolation.log_inv_norm_ge line 802
  45. theorem OAI.Percolation.eventually_amplification_log_estimates line 812
  46. theorem OAI.Percolation.LocalEndpointRule.asymptotic_amplification_step line 878
  47. theorem OAI.Percolation.weightedWindowProbability_term_le line 959
  48. theorem OAI.Percolation.orbit_scale_window_bound line 965
  49. theorem OAI.Percolation.tendsto_dyadic_scale line 984
  50. structure OAI.Percolation.EndpointProfile line 999
  51. def OAI.Percolation.EndpointProfile.U line 1011
  52. def OAI.Percolation.EndpointProfile.m line 1012
  53. def OAI.Percolation.EndpointProfile.H line 1013
  54. def OAI.Percolation.EndpointProfile.cost line 1014
  55. theorem OAI.Percolation.EndpointProfile.U_nonneg line 1016
  56. theorem OAI.Percolation.EndpointProfile.m_pos line 1022
  57. theorem OAI.Percolation.EndpointProfile.cost_pos line 1025
  58. theorem OAI.Percolation.EndpointProfile.exp_cost_identity line 1029
  59. theorem OAI.Percolation.starting_endpoint_profile line 1041
  60. theorem OAI.Percolation.EndpointProfile.amplify_at_scales line 1075
  61. def OAI.Percolation.amplificationContraction line 1143
  62. theorem OAI.Percolation.exists_amplification_contraction line 1146
  63. theorem OAI.Percolation.amplification_cost_contraction line 1164
  64. theorem OAI.Percolation.EndpointProfile.cost_contraction line 1184
  65. theorem OAI.Percolation.EndpointProfile.total_cost_le line 1196