OAI/Probability/InvariantIsing/Fields/FieldSpatialParameterOrder.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The spatial consequence of the backward covariance derivative. Radial antitonicity of that derivative gives ordering of the physical conditional means, and hence ordering of all earlier squared means.

  1. theorem OAI.InvariantIsing.field_spatial_derivative_order line 17
  2. theorem OAI.InvariantIsing.FieldSmoothFamily.physical_mean_antitone_parameter line 28
  3. theorem OAI.InvariantIsing.FieldSmoothFamily.earlier_squares_antitone_parameter line 37