Newton Picard

Stream: maths

[Jeremy Avigad]

@Patrick Massot @Jan-David Salchow I moved this from the out_param again thread. Newton-Picard looks great! It would be nice to have it in mathlib.

I agree with Patrick that before moving it to mathlib, we should think about whether the basic notions look the way we want them to. For example, pos_real belongs in real with nnreal and ennreal, and should probably be named preal, to match pnat(in the data folder). For another thing, I wonder whether it will later cause problems to have moreover be a token.

I don't have any recommendation as to how to use deriv as a function or partial function. I tend to be conservative and wait until I have an application before adding something to the library. So, for example, my tendency would be to keep using has_fderiv and has_deriv until there is a good reason not to (for example, because they don't work well with calculations). And then that application will help us figure out what we want.

I do have some ideas as to how to make calculations with partial functions more palatable, and I am hoping to experiment with that soon.

Jan-David, is there a specific reason that Newton-Picard requires defining the space of differentiable maps? Or were you just experimenting with the definition?

[Patrick Massot]

I think what Jan-David wrote uses only the derivative of f at 0. The right-inverse assumptions are morally about the second derivative of f at zero, but the second derivative actually doesn't appear. This is a really technical stuff, relevant in situations where we actually don't want to try to handle more derivative. Jeremy, in the situation Jan-David has in mind, the equation f = 0 is a non-linear Cauchy-Riemann equation, on spaces of maps between manifolds, with some Sobolev regularity. This explain while this theorem looks a bit strange

[Patrick Massot]

But I can totally understand why he introduced differentiable maps. This is really the first move you want after defining has_deriv

[Jan-David Salchow]

I mainly introduce differentiable maps in this way, because it worked nicely for the operator norm

[Patrick Massot]

I think the mean value inequality is a much better test for this. Here we really need a differentiable function. It would also need some stuff specific to dimension 1 (the mean value theorem).

[Patrick Massot]

I don't understand the comment about the operator norm

[Jan-David Salchow]

Well, the last thing I did with lean was putting the structure of a normed linear space on the set of bounded linear operators between normed spaces

[Patrick Massot]

Yes, we know this

[Jan-David Salchow]

Since copy and paste of that definition almost worked, I used it as a domain for the differential

[Jan-David Salchow]

That's definitely more than necessary

[Jan-David Salchow]

But handy if you want the differential at zero