OAI/Probability/InvariantIsing/Fields/FieldZeroIncrement.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Inserting a zero covariance increment preserves the scalar Ising value and spin mean. Its adjacent overlap levels are the same.

  1. lemma OAI.InvariantIsing.fieldScalarValue_insert_zero line 14
  2. lemma OAI.InvariantIsing.fieldScalarMean_insert_zero line 20
  3. def OAI.InvariantIsing.fieldScalarSquareAt line 33

    Source documentation

    The natural-index form of a scalar square. All indices used by the finite field are at most the length; the terminal extension avoids casts in zero-increment insertion.

    def fieldScalarSquareAt : List (ℝ × ℝ≥0) → (ℝ → ℝ) → (ℝ → ℝ) → ℕ → ℝ → ℝ
  | [], _, b, _ => fun z => (b z) ^ 2
  | av :: L, F, b, 0 => fun z => (fieldScalarMean (av :: L) F b z) ^ 2
  | av :: L, F, b, i + 1 =>
      fieldSpinTransition av.1 av.2 (fieldScalarValue L F) (fieldScalarSquareAt L F b i)

    Mentions: OAI.InvariantIsing.fieldScalarMean, OAI.InvariantIsing.fieldSpinTransition, OAI.InvariantIsing.fieldScalarValue

  4. lemma OAI.InvariantIsing.fieldScalarSquareAt_eq line 39
  5. lemma OAI.InvariantIsing.fieldScalarSquareAt_insert_zero line 52