OAI/Probability/InvariantIsing/Magnetic/MagneticSquareInverseConvex.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Every finite conditional square mean is convex in the inverse mean coordinate. This is derived by induction through the actual Gaussian steps.

  1. lemma OAI.InvariantIsing.magneticScalarSquareFourJet_zero_toJet line 14
  2. lemma OAI.InvariantIsing.magneticScalarSquareFourJet_succ_toJet line 23
  3. lemma OAI.InvariantIsing.magneticSquareJet_weighted_nonneg line 36
  4. theorem OAI.InvariantIsing.magneticScalarSquare_inverse_convex line 47