OAI/Probability/FreeIsing/Conditioning/PlantedInformation.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem367.PlantedInformation.observationSigma line 16
  2. theorem OAI.Problem367.PlantedInformation.measurable_spinSign line 20
  3. theorem OAI.Problem367.PlantedInformation.spinSign_memLp line 24
  4. theorem OAI.Problem367.PlantedInformation.observationSigma_le line 29
  5. theorem OAI.Problem367.PlantedInformation.observation_stronglyMeasurable line 35
  6. theorem OAI.Problem367.PlantedInformation.noise_hasLaw line 39
  7. theorem OAI.Problem367.PlantedInformation.noise_iIndepFun line 46
  8. theorem OAI.Problem367.PlantedInformation.spin_noise_indep line 54
  9. theorem OAI.Problem367.PlantedInformation.integral_spin_mul_spin line 62
  10. theorem OAI.Problem367.PlantedInformation.critical_information_of_spin_sums line 72