OAI/Probability/InvariantIsing/Fields/FieldTangentOrder.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Evenness and radial antitonicity of a backward covariance derivative are preserved by each unchanged earlier Gaussian transition.

  1. lemma OAI.InvariantIsing.field_gaussianTiltAverage_even line 15
  2. lemma OAI.InvariantIsing.field_gaussianTiltAverage_even_monotone line 22
  3. lemma OAI.InvariantIsing.field_gaussianTiltAverage_even_antitone line 30
  4. lemma OAI.InvariantIsing.field_negative_square_average_shape line 51
  5. theorem OAI.InvariantIsing.FieldSmoothFamily.zero_slope_tangent_shape line 77