OAI/Probability/InvariantIsing/Haar/CompactNegativeMinimum.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A compact parabolic minimum test restricted to negative minima.

  1. lemma OAI.InvariantIsing.compact_nonneg_of_negative_min_derivative line 11