OAI/Probability/InvariantIsing/Fields/FieldRealVariance.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Real-variance notation for the scalar recursion. Outside the positive variance cone the existing Gaussian transform uses zero noise; these spatial identities remain valid there as well.

  1. lemma OAI.InvariantIsing.field_sqrt_toNNReal line 15
  2. lemma OAI.InvariantIsing.field_gaussianTransform_eq_operator line 19
  3. lemma OAI.InvariantIsing.field_gaussianTiltAverage_eq_transition line 28
  4. lemma OAI.InvariantIsing.field_gaussianTiltAverage_bound line 36
  5. lemma OAI.InvariantIsing.field_gaussianTransform_hasDerivAt line 43
  6. lemma OAI.InvariantIsing.field_gaussianTiltAverage_hasDerivAt line 52