OAI/Probability/InvariantIsing/Cavity/CavityFieldPath.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

The finite field path reconstructed by the cavity covariance. Its covariance density has the continuous right-derivative value at zero.

  1. def OAI.InvariantIsing.cavityFieldDensity line 17
  2. def OAI.InvariantIsing.cavityFieldPrimitive line 21
  3. def OAI.InvariantIsing.cavityFieldDiagonal line 25
  4. lemma OAI.InvariantIsing.continuous_cavityFieldDensity line 29
  5. lemma OAI.InvariantIsing.cavityFieldPrimitive_nonneg line 34
  6. lemma OAI.InvariantIsing.cavityFieldPrimitive_mono line 40
  7. lemma OAI.InvariantIsing.cavityFieldPrimitive_sub line 47
  8. def OAI.InvariantIsing.cavityFieldStep line 57
  9. lemma OAI.InvariantIsing.cavityFieldStep_on_cell line 71