OAI/Probability/InvariantIsing/Magnetic/RestrictedDepthPair.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Preservation of the common-level law by the published finite-field terminal tilt, including the independent scalar-field spins.

  1. lemma OAI.InvariantIsing.restricted_leaf_depth_pair_conditioning line 15
  2. lemma OAI.InvariantIsing.restricted_published_depth_test line 49
  3. def OAI.InvariantIsing.restrictedFieldDepthPairIntegrand line 60
  4. def OAI.InvariantIsing.restrictedFieldDepthPairMean line 68
  5. lemma OAI.InvariantIsing.measurable_restrictedFieldDepthPairIntegrand line 71
  6. lemma OAI.InvariantIsing.measurable_restrictedFieldDepthPairMean line 93
  7. theorem OAI.InvariantIsing.restricted_field_depth_pair_evaluation line 97