OAI/Probability/InvariantIsing/Fields/FieldScalarOverlap.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The scalar field's actual level overlaps. Their ordering is the conditional Jensen inequality, and zero increments give exact ties.

  1. lemma OAI.InvariantIsing.fieldScalarSquares_monotone line 14
  2. lemma OAI.InvariantIsing.fieldScalarSquares_tied_increment line 49
  3. def OAI.InvariantIsing.fieldScalarOverlaps line 74

    Source documentation

    Root Gaussian averaging produces the level second moments B_i.

    def fieldScalarOverlaps (L : List (ℝ × ℝ≥0)) (root : ℝ≥0)
    (F a : ℝ → ℝ) (i : Fin (L.length + 1)) : ℝ :=
…
  4. lemma OAI.InvariantIsing.fieldScalarOverlaps_mem_unit line 78
  5. lemma OAI.InvariantIsing.fieldScalarOverlaps_monotone line 92
  6. lemma OAI.InvariantIsing.fieldScalarOverlaps_tied_increment line 104