OAI/Probability/InvariantIsing/Fields/FieldScalarComposition.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Exact concatenation and linear propagation identities for the finite scalar field recursion. The exponents may include the zero root level.

  1. lemma OAI.InvariantIsing.fieldScalarValue_append line 15
  2. lemma OAI.InvariantIsing.fieldScalarMean_append line 19
  3. lemma OAI.InvariantIsing.fieldScalarMean_const_mul line 27
  4. def OAI.InvariantIsing.fieldAppendIndex line 37

    Source documentation

    Index of a level in the suffix, after an unchanged prefix.

    def fieldAppendIndex (P S : List (ℝ × ℝ≥0)) (i : Fin (S.length + 1)) :
    Fin ((P ++ S).length + 1) :=
…
  5. lemma OAI.InvariantIsing.fieldScalarSquares_append line 41
  6. lemma OAI.InvariantIsing.fieldConstantPrefix_test_regular line 61
  7. lemma OAI.InvariantIsing.fieldConstantPrefix_test_affine line 83
  8. lemma OAI.InvariantIsing.fieldScalarSquares_congr_list line 114