OAI/Probability/InvariantIsing/Arrays/ReplicaProductPrimitives.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Integral primitive identities for bounded measurable replica paths. No continuity of the overlap paths is required.

  1. lemma OAI.InvariantIsing.absolutelyContinuous_tail_integral line 15
  2. lemma OAI.InvariantIsing.continuous_tail_integral line 24
  3. lemma OAI.InvariantIsing.ae_hasDerivAt_tail_integral line 33
  4. lemma OAI.InvariantIsing.integral_tail_product line 43
  5. lemma OAI.InvariantIsing.integral_head_moment line 68