OAI/Combinatorics/SquareDifference/UniformBase.lean
3 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.SquareDifference.positiveLaw_diagonal_pointwiseline 15 - lemma
OAI.SquareDifference.setFunctional_baseline 31 - lemma
OAI.SquareDifference.inverse_power_baseline 48