Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] New in the AFP: Wooley's Discrete Inequality

Email Gateway (Oct 17 2024 at 13:20):

From: Lawrence Paulson <lp15@cam.ac.uk>
I'm happy to announce a new contribution, by Angeliki Koutsoukou-Argyraki: Wooley's Discrete Inequality.

This is a formalisation of the proof of an inequality by Trevor D. Wooley... based on the note An Elementary Discrete Inequality: https://www.math.purdue.edu/~twooley/publ/20230410discineq.pdf

Her entry is online at https://www.isa-afp.org/entries/Wooley_Elementary_Discrete_Inequality.html

Larry Paulson

Last updated: Jan 04 2025 at 20:18 UTC