OAI/Probability/InvariantIsing/Arrays/TensorWardMeasurability.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Joint measurability and bounded integrability of the actual finite principal Ward term and its Gaussian correction.

  1. lemma OAI.InvariantIsing.measurable_finiteGibbs line 17
  2. lemma OAI.InvariantIsing.measurable_gibbsPairAverage line 24
  3. lemma OAI.InvariantIsing.measurable_gibbsTripleAverage line 32
  4. lemma OAI.InvariantIsing.measurable_gaussianWardCorrection_joint line 42
  5. lemma OAI.InvariantIsing.measurable_tensorRestrictionHamiltonian line 53
  6. lemma OAI.InvariantIsing.measurable_tensorNamespacedPlaneCross line 62
  7. lemma OAI.InvariantIsing.measurable_tensorRestrictionPairCovarianceDerivative line 81
  8. lemma OAI.InvariantIsing.measurable_tensorRestrictionOffVariation line 100
  9. lemma OAI.InvariantIsing.integrable_tensorRestrictionOffVariation line 125
  10. def OAI.InvariantIsing.tensorRestrictionOffCorrection line 164
  11. lemma OAI.InvariantIsing.measurable_tensorRestrictionOffCorrection line 174
  12. lemma OAI.InvariantIsing.tensorRestrictionOffCorrection_abs_le line 195
  13. lemma OAI.InvariantIsing.integrable_tensorRestrictionOffCorrection line 224