OAI/Probability/FreeIsing/Ising/OrientedGaussianTail.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem367.IsingOrientedPath.terminalAttenuation line 20
  2. theorem OAI.Problem367.IsingOrientedPath.measurable_terminalAttenuation line 25
  3. theorem OAI.Problem367.IsingOrientedPath.attenuation_eq_terminal line 32
  4. def OAI.Problem367.IsingOrientedPath.terminalExtensionAverage line 36
  5. theorem OAI.Problem367.IsingOrientedPath.measurable_terminalExtensionAverage line 41
  6. theorem OAI.Problem367.IsingOrientedPath.extensionAverage_identDistrib_gaussian line 49
  7. theorem OAI.Problem367.IsingOrientedPath.terminalAttenuation_inward_sq_eq_rootPathProduct line 62
  8. theorem OAI.Problem367.IsingOrientedPath.terminalAttenuation_outward_sq_eq_rootPathProduct line 78
  9. def OAI.Problem367.IsingOrientedPath.orientedGaussianFactor line 90
  10. theorem OAI.Problem367.IsingOrientedPath.terminalAttenuation_sq_eq_rootPathProduct line 96
  11. def OAI.Problem367.IsingOrientedPath.restrictedAverage line 106
  12. theorem OAI.Problem367.IsingOrientedPath.measurable_restrictedAverage line 110
  13. theorem OAI.Problem367.IsingOrientedPath.restrictedAverage_identDistrib_gaussian line 117
  14. def OAI.Problem367.IsingOrientedPath.orientationCutCost line 144
  15. theorem OAI.Problem367.IsingOrientedPath.measure_restrictedAverage_ge_le_double_exp line 147