OAI/Probability/InvariantIsing/Fields/FieldScalarChain.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Actual one-dimensional backward values, physical conditional spin means, and conditional second moments for a finite list of field increments.

  1. def OAI.InvariantIsing.fieldScalarValue line 15
  2. def OAI.InvariantIsing.fieldScalarMean line 18
  3. lemma OAI.InvariantIsing.fieldScalarValue_regular line 22
  4. lemma OAI.InvariantIsing.fieldScalarMean_regular line 32
  5. def OAI.InvariantIsing.fieldScalarSquares line 48

    Source documentation

    The entry indexed by i is the conditional expectation of the square of the physical spin mean at level i, given the starting position.

    def fieldScalarSquares : (L : List (ℝ × ℝ≥0)) → (ℝ → ℝ) → (ℝ → ℝ) →
    Fin (L.length + 1) → ℝ → ℝ
  | [], _, a => fun _ z => (a z) ^ 2
  | av :: L, F, a => Fin.cons (fun z => (fieldScalarMean (av :: L) F a z) ^ 2)
      (fun i => fieldSpinTransition av.1 av.2 (fieldScalarValue L F) (fieldScalarSquares L F a i))

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

  6. lemma OAI.InvariantIsing.fieldScalarSquares_zero line 54
  7. lemma OAI.InvariantIsing.fieldScalarSquares_regular line 58