OAI/Probability/InvariantIsing/Arrays/TensorFieldTailBridge.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The contact field directions are bounded continuous tests of the actual spectral array, so their expectations pass to the synchronized limit.

  1. def OAI.InvariantIsing.spectralSpinDepthTail line 16
  2. lemma OAI.InvariantIsing.continuous_spectralSpinDepthTail line 19
  3. lemma OAI.InvariantIsing.tensorNamespacedArrayLaw_field_tail line 26
  4. lemma OAI.InvariantIsing.spectralSpinDepthTail_weak_limit line 48