OAI/Probability/FreeIsing/Ising/CanonicalPosteriorStops.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.Problem367.IsingObservationFactor.continuous_real_tanh line 14
  2. def OAI.Problem367.IsingObservationFactor.continuousPosterior line 17
  3. lemma OAI.Problem367.IsingObservationFactor.continuousPosterior_progressive line 20
  4. lemma OAI.Problem367.IsingObservationFactor.continuousPosterior_interior line 25
  5. lemma OAI.Problem367.IsingObservationFactor.artanh_continuousPosterior line 29
  6. theorem OAI.Problem367.IsingObservationFactor.continuousPosterior_modification line 34
  7. lemma OAI.Problem367.IsingObservationFactor.copyProjection_measurePreserving line 45
  8. def OAI.Problem367.IsingObservationFactor.copyContinuousField line 57
  9. def OAI.Problem367.IsingObservationFactor.copyContinuousPosterior line 60
  10. lemma OAI.Problem367.IsingObservationFactor.copyContinuousField_progressive line 63
  11. lemma OAI.Problem367.IsingObservationFactor.copyContinuousPosterior_progressive line 74
  12. theorem OAI.Problem367.IsingObservationFactor.copyContinuousPosterior_modification line 80
  13. theorem OAI.Problem367.IsingObservationFactor.copyContinuousPosterior_compact line 92
  14. def OAI.Problem367.IsingObservationFactor.copyResponseEnergy line 106
  15. lemma OAI.Problem367.IsingObservationFactor.copyResponseEnergy_progressive line 110
  16. theorem OAI.Problem367.IsingObservationFactor.copyResponseEnergy_integrable line 119
  17. def OAI.Problem367.IsingObservationFactor.commonResponseCompensator line 128
  18. lemma OAI.Problem367.IsingObservationFactor.commonResponseCompensator_progressive line 133
  19. theorem OAI.Problem367.IsingObservationFactor.commonResponseCompensator_continuous line 139
  20. def OAI.Problem367.IsingObservationFactor.commonPosteriorExit line 150
  21. theorem OAI.Problem367.IsingObservationFactor.isLocalizingSequence_commonPosteriorExit line 155
  22. theorem OAI.Problem367.IsingObservationFactor.ae_eventually_le_commonPosteriorExit line 169