OAI/Probability/InvariantIsing/Fields/PriorContactContinuity.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Joint continuity of the constrained-prior contact pressure, including zero covariance increments and both complete perturbation amplitudes.

  1. def OAI.InvariantIsing.priorContactPressure line 14
  2. lemma OAI.InvariantIsing.priorContact_raw_modulus line 20
  3. lemma OAI.InvariantIsing.continuous_finiteFieldPath line 60
  4. lemma OAI.InvariantIsing.continuous_finiteFieldVariance line 67
  5. lemma OAI.InvariantIsing.continuousOn_priorContactPressure line 81