OAI/Probability/InvariantIsing/Fields/FieldFiniteCoordinates.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The finite covariance-coordinate differential used in the joint height Hessian. The final coordinate is the scalar spatial field.

  1. abbrev OAI.InvariantIsing.FieldCovariate line 14
  2. def OAI.InvariantIsing.fieldFiniteLinear line 16
  3. lemma OAI.InvariantIsing.fieldFiniteLinear_apply line 21
  4. lemma OAI.InvariantIsing.norm_fieldFiniteLinear_le line 25
  5. lemma OAI.InvariantIsing.measurable_fieldFiniteLinear line 45
  6. lemma OAI.InvariantIsing.integral_fieldFiniteLinear line 53