OAI/Probability/FreeIsing/Ising/RootGaussianCut.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem367.IsingRootGaussianCut.terminalAttenuation line 20
  2. theorem OAI.Problem367.IsingRootGaussianCut.measurable_terminalAttenuation line 26
  3. theorem OAI.Problem367.IsingRootGaussianCut.terminalAttenuation_eq_forward_product line 34
  4. def OAI.Problem367.IsingRootGaussianCut.terminalExtensionAverage line 48
  5. theorem OAI.Problem367.IsingRootGaussianCut.measurable_terminalExtensionAverage line 53
  6. theorem OAI.Problem367.IsingRootGaussianCut.extensionAverage_eq_terminal line 61
  7. theorem OAI.Problem367.IsingRootGaussianCut.terminalExtensionAverage_eq_forward_average line 67
  8. theorem OAI.Problem367.IsingRootGaussianCut.extensionAverage_identDistrib_gaussian line 83
  9. theorem OAI.Problem367.IsingRootGaussianCut.integral_root_weight_mul_pow_le_gaussian_cut line 96