OAI/Probability/InvariantIsing/Fields/FieldL1.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The scalar value is one-half Lipschitz in the L1 distance of finite field paths.

  1. lemma OAI.InvariantIsing.field_weighted_difference_bound line 12
  2. theorem OAI.InvariantIsing.abs_fieldValue_sub_le_L1 line 34

    Source documentation

    Uniform in the sizes and relative positions of the two finite partitions.

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

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

  3. lemma OAI.InvariantIsing.fieldValue_eq_of_ae line 49