constructive (computable) power rule

Stream: maths

[Congzhou Sha]

Hi all, from what I understand of the calculus section, the derivative of polynomials is defined completely formally, and is thus noncomputable. I've performed the proof explicitly for integer powers here: https://github.com/mikesha2/power_rule/tree/main

I'm totally new to Lean, so I'm unsure if this is something valuable and if there's interest in formalizing more tedious inequalities?

[Eric Wieser]

I think you're fighting against the tide here. Making polynomial derivatives computable seems pretty pointless as long as polynomial addition is non-computably!

[Eric Wieser]

Having said that, that looks like it was a great project to get familiar with lean, and it's very possible that some of your helper lemmas belong in mathlib (assuming they're not already there!)

[Eric Wieser]

Are you aware of docs#deriv_pow?

[Congzhou Sha]

Yes, I saw that, but again, it looks like it's a strictly formal proof, since it relies on docs#polynomial.derivative, in which the polynomial derivative is defined/assumed rather than proven, making it a tautology (in the mathematics sense, not the lean sense)

[Junyan Xu]

It uses docs#polynomial.derivative only because it uses the more general theorem docs#polynomial.has_strict_deriv_at that connects the derivative in the normed_field sense and the formal polynomial derviative.

[Eric Wieser]

I think a better model is to consider docs#polynomial.derivative as a name for an arbitrary polynomial that just so happens to be the derivative, just as defining def sqrt_four : ℕ := 2 happens to name a square root of 4. We're not proving a tautology when we show sqrt_four^2 = 4, we're simultaneously proving that we found the square root, 2, and that the name we chose for it was a sensible one.

[Eric Wieser]

What do you mean in your readme when you say "the proofs are noncomputable"?