coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Series / Real Analysis in Coq?

From: Siddharth Bhat <siddu.druid AT gmail.com>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: [Coq-Club] Series / Real Analysis in Coq?
Date: Fri, 12 Jan 2018 11:36:37 +0000
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=siddu.druid AT gmail.com; spf=Pass smtp.mailfrom=siddu.druid AT gmail.com; spf=None smtp.helo=postmaster AT mail-qt0-f177.google.com
Ironport-phdr: 9a23:Z4JmVR0YOfibnPwusmDT+DRfVm0co7zxezQtwd8Zse0UIvad9pjvdHbS+e9qxAeQG9mDsrQc06L/iOPJYSQ4+5GPsXQPItRndiQuroEopTEmG9OPEkbhLfTnPGQQFcVGU0J5rTngaRAGUMnxaEfPrXKs8DUcBgvwNRZvJuTyB4Xek9m72/q99pHPfglEniaxba9vJxiqsAvdsdUbj5F/Iagr0BvJpXVIe+VSxWx2IF+Yggjx6MSt8pN96ipco/0u+dJOXqX8ZKQ4UKdXDC86PGAv5c3krgfMQA2S7XYBSGoWkx5IAw/Y7BHmW5r6ryX3uvZh1CScIMb7S60/Vza/4KdxUBLnhycJOTA6/m/KlMJ/kLlWrwi9qxFl2YPYfJ2ZOfh4c6jAfd0aX21BXsNJWiJcA4OzcpYAD+obMuZCs4n9p0YFoAa+BQa2GOPk1zhFhmT33aInzushDBvK0xE6H9ITsXTbsc74NKgXUe+vzanIyS/PYO9R2Tf48YXFdA0qr/KUXb9ob8bd1U0iGxnGg1iQs4DpIS6Z2+UXv2SG7edtV+SigHM9pQ5ruDig3MIsh5HJho0LzlDE8j10wIMvKt25TE53eMekEIdMuy2DOYt6X8EvTmNytCY1zb0GvpG7fCwUx5g92xHfbPmHf5CJ4hLlSumRPS91iGx5dL+7nRq/8kitxvfiWsWp0VtGtDdJn9vOu3wV0hzc8MmHSv9z/ke73jaP0hje6vpFIU8piKXbNoQtzaMqlpoOsETMAzT7mErzjKCMd0Uk/vKk5PjgYrXjvpOcLZN7ihniMqQyncyyGfg3Mg8XX2SC5eu80KDj8lbiTbVRjvw2l7HZv4rAKcQaoK65GQ5V3Zw55xaxFTf1mOgfyDMMK0sAcxaahaDoPUvPKbb2F73311+riXJgw+3MFrznGJTEaHbZxuTPZ7F4vnVdxAYzxMpD59p+CrgdaKboW0P9qZrUFAI4PyS7xu/mDJN20YZICjHHObOQLK6H6QzA3ekoOeTZPNZE6ga4EOAs4rvVtVF8nFYceaez2p5OMSK3G/1nJwOSZn++245dQ1dPhRI3SanRsHPHSSRaPi/gUKc15zV9A4WjX9+aG9KdxYeZ1SL+JaV4I2BLDlfWTyXtfoSAHu4QMGece5A+1DMDUrelRskq0hT87AI=

Hello all,

I'm taking a signals and systems course this semester, so I was interesting in formalizing results on LTI systems in Coq. I've mostly dabbled with it in terms of software foundations, never on the math side.

So, is there a formalization of real analysis ideas, such as sequences, series, etc? What about linear algebra?

I tried searching "mathematical components", but it's a little too large to check out :)

Cheers,

Siddharth

Sending this from my phone, please excuse any typos!

[Coq-Club] Series / Real Analysis in Coq?, Siddharth Bhat, 01/12/2018
- Re: [Coq-Club] Series / Real Analysis in Coq?, Bas Spitters, 01/12/2018