OAI/Probability/InvariantIsing/Fields/FieldPartitionSupport.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The scalar-field supporting inequality, independent of the finite partition.

  1. lemma OAI.InvariantIsing.fieldMagnetizationPath_step_ae line 14
  2. lemma OAI.InvariantIsing.fieldPairing_magnetization_same line 22
  3. lemma OAI.InvariantIsing.fieldPairing_magnetization_self line 37
  4. lemma OAI.InvariantIsing.field_support_same_partition line 45
  5. lemma OAI.InvariantIsing.field_eq_withHeights_of_cutList line 69
  6. lemma OAI.InvariantIsing.field_support_equal_cutList line 84
  7. theorem OAI.InvariantIsing.field_support line 92

    Source documentation

    The exact scalar supporting inequality for arbitrary finite field partitions.

    theorem field_support (h k : FieldStep) :
    fieldValue k 0 ≤ fieldValue h 0 - (1 / 2 : ℝ) *
      ∫ s, fieldMagnetizationPath h s * (fieldFunction k s - fieldFunction h s) ∂pathMeasure := by
…

    Mentions: OAI.InvariantIsing.FieldStep, OAI.InvariantIsing.fieldValue, OAI.InvariantIsing.fieldMagnetizationPath, OAI.InvariantIsing.fieldFunction