OAI/Probability/InvariantIsing/Arrays/TensorDiagonalWardMeasurability.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Joint integrability for the actual finite diagonal Ward identity.

  1. def OAI.InvariantIsing.tensorRestrictionDiagonalPrincipalVariation line 16
  2. lemma OAI.InvariantIsing.measurable_tensorRestrictionDiagonalPrincipalVariation line 25
  3. lemma OAI.InvariantIsing.integrable_tensorRestrictionDiagonalPrincipalVariation line 42
  4. def OAI.InvariantIsing.tensorRestrictionDiagonalCorrection line 63
  5. lemma OAI.InvariantIsing.measurable_tensorRestrictionDiagonalCorrection line 71
  6. lemma OAI.InvariantIsing.tensorRestrictionDiagonalCorrection_abs_le line 86
  7. lemma OAI.InvariantIsing.integrable_tensorRestrictionDiagonalCorrection line 110