OAI/Probability/InvariantIsing/Fields/FieldEndpointIntegrability.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Integrability of linear-growth vector observables under the actual canonical endpoint law, uniformly allowing zero-variance increments.

  1. lemma OAI.InvariantIsing.integrable_linearGrowth_pi line 15
  2. lemma OAI.InvariantIsing.fieldTailEndpointKernel_integrable_id line 35
  3. lemma OAI.InvariantIsing.fieldVectorTailEndpointKernel_integrable line 51