OAI/Probability/FreeIsing/Factors/Observable.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem367.FactorObservable.field line 16
  2. lemma OAI.Problem367.FactorObservable.measurable_field line 20
  3. lemma OAI.Problem367.FactorObservable.equivariant_field line 24
  4. lemma OAI.Problem367.FactorObservable.memLp_field line 34
  5. def OAI.Problem367.FactorObservable.spinLp line 39
  6. lemma OAI.Problem367.FactorObservable.coe_spinLp line 42
  7. lemma OAI.Problem367.FactorObservable.norm_spinLp line 47
  8. lemma OAI.Problem367.FactorObservable.integral_spinLp line 60
  9. lemma OAI.Problem367.FactorObservable.spinLp_mem_centered line 66
  10. def OAI.Problem367.FactorObservable.centeredSpinLp line 72
  11. lemma OAI.Problem367.FactorObservable.centeredSpinLp_coe line 77
  12. lemma OAI.Problem367.FactorObservable.norm_centeredSpinLp line 81
  13. lemma OAI.Problem367.FactorObservable.koopman_spinLp line 85
  14. lemma OAI.Problem367.FactorObservable.inner_spinLp line 98
  15. lemma OAI.Problem367.FactorObservable.inner_spinLp_root line 107
  16. lemma OAI.Problem367.FactorObservable.inner_centeredSpinLp_root line 116
  17. lemma OAI.Problem367.FactorObservable.inner_koopman_spinLp_root line 123
  18. lemma OAI.Problem367.FactorObservable.centeredAverage_centeredSpinLp line 135
  19. theorem OAI.Problem367.IsFactorOfIID.exists_centered_observable line 152