OAI/Probability/InvariantIsing/Fields/MarkEndpointIntegral.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Bounded endpoint observables of independent and shared ancestor paths.

  1. def OAI.InvariantIsing.markPairEndpoint line 12
  2. lemma OAI.InvariantIsing.measurable_markPairEndpoint line 16
  3. lemma OAI.InvariantIsing.markPairEndpoint_cons line 22
  4. lemma OAI.InvariantIsing.integral_markStateKernel line 28
  5. lemma OAI.InvariantIsing.integral_markStateParallel line 35
  6. theorem OAI.InvariantIsing.markPairPathMean_independent_endpoint line 54
  7. theorem OAI.InvariantIsing.markPairPathMean_shared_endpoint line 87