OAI/Probability/InvariantIsing/Fields/FieldSmoothFamily.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

The scalar field family carrying exactly the derivatives needed for finite covariance-coordinate differentiation. No bound on the value is required: bounded spatial derivative supplies its Gaussian moments.

  1. structure OAI.InvariantIsing.FieldSmoothFamily line 15
  2. lemma OAI.InvariantIsing.FieldSmoothFamily.kx_nonneg line 38
  3. lemma OAI.InvariantIsing.FieldSmoothFamily.growth line 40
  4. def OAI.InvariantIsing.FieldSmoothFamily.value line 43
  5. def OAI.InvariantIsing.FieldSmoothFamily.mean line 46
  6. def OAI.InvariantIsing.FieldSmoothFamily.curvature line 50
  7. def OAI.InvariantIsing.FieldSmoothFamily.tangent line 56
  8. lemma OAI.InvariantIsing.FieldSmoothFamily.measurable_value line 62
  9. lemma OAI.InvariantIsing.FieldSmoothFamily.measurable_mean line 65
  10. lemma OAI.InvariantIsing.FieldSmoothFamily.measurable_curvature line 69
  11. lemma OAI.InvariantIsing.FieldSmoothFamily.measurable_tangent line 76
  12. lemma OAI.InvariantIsing.FieldSmoothFamily.bound_mean line 83
  13. lemma OAI.InvariantIsing.FieldSmoothFamily.bound_curvature line 87
  14. lemma OAI.InvariantIsing.FieldSmoothFamily.bound_tangent line 111
  15. lemma OAI.InvariantIsing.FieldSmoothFamily.spatial_value line 127
  16. lemma OAI.InvariantIsing.FieldSmoothFamily.spatial_mean line 133
  17. def OAI.InvariantIsing.FieldSmoothFamily.transform line 144