OAI/Probability/InvariantIsing/Fields/FieldPublishedEvaluation.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Evaluating the finite published endpoint law on physical spin means.

  1. def OAI.InvariantIsing.fieldDepthLevel line 13
  2. lemma OAI.InvariantIsing.fieldDepthLevel_common line 16
  3. def OAI.InvariantIsing.fieldEndpointCoordinateTest line 21
  4. lemma OAI.InvariantIsing.measurable_fieldEndpointCoordinateTest line 26
  5. lemma OAI.InvariantIsing.fieldEndpointCoordinateTest_bound line 34
  6. theorem OAI.InvariantIsing.field_published_coordinate_test line 47
  7. lemma OAI.InvariantIsing.field_root_average_squares line 69
  8. lemma OAI.InvariantIsing.measurable_fieldCommonLevel line 85
  9. theorem OAI.InvariantIsing.field_published_rooted_coordinate_test line 93