OAI/Probability/Ising/FieldUpdate.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.BufferedIsing.DSS.insertSpin line 15

    Source documentation

    The spin at the removed site is inserted without discarding any edge interaction.

    def insertSpin (v : V) (b : Bool) (η : {u : V // u ≠ v} → Bool) : V → Bool :=
…
  2. lemma OAI.BufferedIsing.DSS.insertSpin_self line 19
  3. lemma OAI.BufferedIsing.DSS.insertSpin_other line 23
  4. lemma OAI.BufferedIsing.DSS.sum_insert line 27
  5. lemma OAI.BufferedIsing.DSS.sum_remove line 33
  6. def OAI.BufferedIsing.DSS.removedField line 41

    Source documentation

    Conditional field induced by an actual fixed spin.

    def removedField (J : V → V → ℝ) (h : V → ℝ) (v : V) (b : Bool)
    (u : {u : V // u ≠ v}) : ℝ := h u + (J v u + J u v) * sgn b

    Mentions: OAI.BufferedIsing.DSS.sgn

  7. def OAI.BufferedIsing.DSS.removedCoupling line 44
  8. lemma OAI.BufferedIsing.DSS.hamiltonian_insert line 47
  9. lemma OAI.BufferedIsing.DSS.mass_insert line 67
  10. def OAI.BufferedIsing.DSS.pinMean line 74

    Source documentation

    Conditional mean at a fixed-spin site; defined on actual remaining spins.

    def pinMean (J : V → V → ℝ) (h : V → ℝ) (v : V) (b : Bool) (o : V) : ℝ :=
…
  11. lemma OAI.BufferedIsing.DSS.pinMean_self line 77
  12. lemma OAI.BufferedIsing.DSS.pinMean_other line 81
  13. lemma OAI.BufferedIsing.DSS.pinMean_mono line 89
  14. lemma OAI.BufferedIsing.DSS.average_mul_part line 100
  15. def OAI.BufferedIsing.DSS.pinPart line 104
  16. lemma OAI.BufferedIsing.DSS.pinPart_pos line 107
  17. lemma OAI.BufferedIsing.DSS.part_split line 110
  18. lemma OAI.BufferedIsing.DSS.mean_split line 117
  19. lemma OAI.BufferedIsing.DSS.mean_self_split line 130
  20. lemma OAI.BufferedIsing.DSS.mean_affine line 136
  21. def OAI.BufferedIsing.DSS.fieldAt line 146

    Source documentation

    A single finite field increment.

    def fieldAt (v : V) (t : ℝ) : V → ℝ := fun u => if u = v then t else 0
…
  22. lemma OAI.BufferedIsing.DSS.fieldAt_self line 149
  23. lemma OAI.BufferedIsing.DSS.fieldAt_other line 152
  24. lemma OAI.BufferedIsing.DSS.removedField_shift line 156
  25. lemma OAI.BufferedIsing.DSS.pinMean_shift line 161
  26. lemma OAI.BufferedIsing.DSS.pinPart_shift line 165
  27. lemma OAI.BufferedIsing.DSS.mean_field_update line 171
  28. lemma OAI.BufferedIsing.DSS.hamiltonian_flip line 188
  29. lemma OAI.BufferedIsing.DSS.mass_flip line 192
  30. def OAI.BufferedIsing.DSS.flipEquiv line 196
  31. lemma OAI.BufferedIsing.DSS.part_neg line 202
  32. lemma OAI.BufferedIsing.DSS.mean_neg line 207
  33. lemma OAI.BufferedIsing.DSS.mean_zero line 214
  34. lemma OAI.BufferedIsing.DSS.mean_nonneg line 219
  35. lemma OAI.BufferedIsing.DSS.fieldAt_zero line 224
  36. lemma OAI.BufferedIsing.DSS.mean_mixture_identity line 228
  37. lemma OAI.BufferedIsing.DSS.mean_mixture_le line 239
  38. lemma OAI.BufferedIsing.DSS.mean_mixture_ge line 250
  39. lemma OAI.BufferedIsing.DSS.mean_mixture_eq line 261