OAI/Probability/FreeIsing/Posterior/Fields.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem367.FinitePosterior.fieldEnergy line 13
  2. def OAI.Problem367.FinitePosterior.fieldMean line 16
  3. def OAI.Problem367.FinitePosterior.fieldMass line 21
  4. lemma OAI.Problem367.FinitePosterior.fieldMean_eq_sum_fieldMass line 24
  5. lemma OAI.Problem367.FinitePosterior.fieldMean_along_line line 29
  6. lemma OAI.Problem367.FinitePosterior.mean_fieldEnergy_zero line 42
  7. lemma OAI.Problem367.FinitePosterior.fieldPartition_pos line 48
  8. lemma OAI.Problem367.FinitePosterior.fieldMass_pos line 52
  9. theorem OAI.Problem367.FinitePosterior.continuous_fieldMean line 56
  10. lemma OAI.Problem367.FinitePosterior.fieldMean_const line 67
  11. lemma OAI.Problem367.FinitePosterior.fieldMean_spin_mem_Ioo line 71
  12. theorem OAI.Problem367.FinitePosterior.hasDerivAt_fieldMean line 79
  13. theorem OAI.Problem367.FinitePosterior.hasDerivAt_fieldMean_coordinate line 90