OAI/Probability/InvariantIsing/Arrays/TensorFieldDerivativeIntegrability.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Integrability of the tensor pressure before varying its linear field. Gaussian CGF bounds suffice; no concentration input is used.

  1. lemma OAI.InvariantIsing.randomCoefficient_log_partition_integrable line 16
  2. lemma OAI.InvariantIsing.tensorDeterministicLog_eq line 56
  3. lemma OAI.InvariantIsing.tensorDeterministicLog_abs_le line 68
  4. def OAI.InvariantIsing.tensorDeterministicEnergy line 86
  5. lemma OAI.InvariantIsing.measurable_tensorDeterministicEnergy line 90
  6. lemma OAI.InvariantIsing.tensorDeterministicLog_integrable line 100
  7. lemma OAI.InvariantIsing.measurable_tensorNamespacedPathFields line 125
  8. theorem OAI.InvariantIsing.tensorNamespacedLog_integrable line 142
  9. lemma OAI.InvariantIsing.tensorNamespacedPressure_integrable line 166