OAI/Probability/Contingency/AcceptedChain.lean

GitHub source file

53 declarations, 0 contain sorry, 0 declared as axioms

Accepted Chain.

  1. structure OAI.Contingency.FiniteChain.AcceptedData line 19
  2. def OAI.Contingency.FiniteChain.AcceptedData.total line 33
  3. theorem OAI.Contingency.FiniteChain.AcceptedData.total_pos line 36
  4. def OAI.Contingency.FiniteChain.AcceptedData.rate line 40
  5. def OAI.Contingency.FiniteChain.AcceptedData.kernel line 42
  6. theorem OAI.Contingency.FiniteChain.AcceptedData.rate_nonneg line 45
  7. theorem OAI.Contingency.FiniteChain.AcceptedData.rate_sum line 49
  8. theorem OAI.Contingency.FiniteChain.AcceptedData.rate_self line 56
  9. def OAI.Contingency.FiniteChain.AcceptedData.chain line 58
  10. theorem OAI.Contingency.FiniteChain.AcceptedData.chain_pi line 92
  11. theorem OAI.Contingency.FiniteChain.AcceptedData.chain_P line 93
  12. theorem OAI.Contingency.FiniteChain.AcceptedData.offdiagonal_flow line 95
  13. theorem OAI.Contingency.FiniteChain.AcceptedData.energy_formula line 100
  14. theorem OAI.Contingency.FiniteChain.AcceptedData.variance_formula line 114
  15. def OAI.Contingency.FiniteChain.Chain.mass line 139
  16. def OAI.Contingency.FiniteChain.Chain.cut line 140
  17. def OAI.Contingency.FiniteChain.Chain.variationEnergy line 142
  18. def OAI.Contingency.FiniteChain.Chain.positiveSupport line 145
  19. theorem OAI.Contingency.FiniteChain.Chain.mass_mono line 148
  20. theorem OAI.Contingency.FiniteChain.Chain.mass_nonneg line 152
  21. theorem OAI.Contingency.FiniteChain.Chain.mass_le_one line 156
  22. theorem OAI.Contingency.FiniteChain.Chain.cut_as_restricted line 160
  23. theorem OAI.Contingency.FiniteChain.Chain.indicator_energy line 167
  24. theorem OAI.Contingency.FiniteChain.Chain.coarea line 183
  25. theorem OAI.Contingency.FiniteChain.Chain.variation_square_cauchy line 281
  26. theorem OAI.Contingency.FiniteChain.Chain.small_support_poincare line 311
  27. theorem OAI.Contingency.FiniteChain.Chain.median_exists line 347
  28. theorem OAI.Contingency.FiniteChain.Chain.variance_le_constant line 401
  29. theorem OAI.Contingency.FiniteChain.Chain.positive_negative_squares line 414
  30. theorem OAI.Contingency.FiniteChain.Chain.positive_negative_edge line 419
  31. theorem OAI.Contingency.FiniteChain.Chain.cheeger_poincare line 436
  32. def OAI.Contingency.Grid.Adj line 487
  33. theorem OAI.Contingency.Grid.adj_symm line 489
  34. theorem OAI.Contingency.Grid.adj_irrefl line 492
  35. def OAI.Contingency.Grid.axis line 496
  36. theorem OAI.Contingency.Grid.axis_spec line 498
  37. def OAI.Contingency.Grid.signedAxis line 501
  38. theorem OAI.Contingency.Grid.signedAxis_injective line 505
  39. theorem OAI.Contingency.Grid.neighbor_card line 527
  40. def OAI.Contingency.Grid.edgeWeight line 533
  41. theorem OAI.Contingency.Grid.edgeWeight_nonneg line 537
  42. theorem OAI.Contingency.Grid.edgeWeight_sum line 544
  43. def OAI.Contingency.Grid.metropolis line 564
  44. theorem OAI.Contingency.Grid.border_sum line 592
  45. theorem OAI.Contingency.Grid.metropolis_cut line 610
  46. def OAI.Contingency.Dense.BinProblem.chain line 642
  47. theorem OAI.Contingency.Dense.BinProblem.chain_mass line 646
  48. theorem OAI.Contingency.Dense.BinProblem.chain_cut line 650
  49. def OAI.Contingency.Dense.BinProblem.kappa line 655
  50. theorem OAI.Contingency.Dense.BinProblem.kappa_pos line 657
  51. theorem OAI.Contingency.Dense.BinProblem.weighted_compl line 663
  52. theorem OAI.Contingency.Dense.BinProblem.chain_conductance line 669
  53. theorem OAI.Contingency.Dense.BinProblem.chain_poincare line 704