OAI/Probability/InvariantIsing/Fields/FieldMagnetization.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Actual magnetization-overlap path for a finite scalar Ising field.

  1. def OAI.InvariantIsing.scalarFieldIncrements line 15

    Source documentation

    The non-root Gaussian increments in the given field step.

    def scalarFieldIncrements (h : FieldStep) : List (ℝ × ℝ≥0) :=
…

    Mentions: OAI.InvariantIsing.FieldStep

  2. lemma OAI.InvariantIsing.scalarFieldIncrements_length line 19
  3. lemma OAI.InvariantIsing.scalarFieldIncrements_positive line 22
  4. lemma OAI.InvariantIsing.scalarFieldIncrements_value line 28
  5. lemma OAI.InvariantIsing.fieldValue_scalar_chain line 37
  6. def OAI.InvariantIsing.fieldMagnetizationLevel line 48

    Source documentation

    The physical squared conditional spin means, averaged over the root Gaussian. These are the B_i(h) of the field derivative formula.

    def fieldMagnetizationLevel (h : FieldStep) (i : Fin (h.depth + 1)) : ℝ :=
…

    Mentions: OAI.InvariantIsing.FieldStep

  7. lemma OAI.InvariantIsing.measurable_field_tanh line 53
  8. lemma OAI.InvariantIsing.fieldMagnetizationLevel_mem_unit line 58
  9. lemma OAI.InvariantIsing.fieldMagnetizationLevel_monotone line 63
  10. def OAI.InvariantIsing.fieldMagnetizationPath line 73

    Source documentation

    A globally defined admissible representative on the field partition.

    def fieldMagnetizationPath (h : FieldStep) : InvariantIsing.OverlapPath :=
…

    Mentions: OAI.InvariantIsing.FieldStep, OAI.InvariantIsing.OverlapPath

  11. lemma OAI.InvariantIsing.fieldMagnetizationPath_on_cell line 77
  12. lemma OAI.InvariantIsing.fieldMagnetizationLevel_tied line 82