Constraints on lambda function

Stream: Is there code for X?

[Max Bobbin]

Is there a way to constrain a variable in a lambda expression. For instance, if I am working with λ x, 1/x and the proof requires that x≠ 0, is there a way to constrain that variable inside the lambda expression, since x doesn't exist inside the local proof? The problem arises when applying a tactic and the expression changes to a form like: (λ x, 1/x) y where lean introduces a new variable, y, but I have no way of also forcing y≠ 0

[Mario Carneiro]

why do you need that assumption in the expression?

[Mario Carneiro]

#mwe

[Mario Carneiro]

there are a few possible techniques but the simplest is to not do that

[Max Bobbin]

Because as I'm going in the proof, I end up with a goal y≠ 0, but I can't prove such a thing since that variable doesn't exist. An example would be showing

example

:deriv (λ x : ℝ, 1/x) = λ x, -1/x^2:=

Such a proof would require x≠ 0
and I can't write it as

example
{y : ℝ}
(hy : y ≠ 0)
:deriv (λ x : ℝ, 1/x) y=  -1/y^2:=

because I also want to show

example
{y : ℝ}
(hy : y ≠ 0)
:deriv^[2] (λ x : ℝ, 1/x) y=  2/y^3:=

which requires the first example when simplified

[Yaël Dillies]

Doesn't that just mean you forgot an assumption originally/your original goal is false?

[Max Bobbin]

I don't think so. take for instance showing

example
{y : ℝ}
(hy : y ≠ 0)
:deriv^[2] (λ x : ℝ, 2/x^2) y=  12/y^4:=

When simplified, the goal becomes deriv (deriv (λ (x : ℝ), 2 / x ^ 2)) y = 12 / y ^ 4

Yet to prove the inside derivative part, would require x≠ 0 by using the deriv.div theorem. However, since x only exists in the lambda function, you can't write such a thing as a premise

[Max Bobbin]

So when you try to prove that inside part,

example
: deriv (λ (x : ℝ), 2 / x ^ 2) = λ x, -4/x^3:=

You can use funext to get a form of deriv (λ (x : ℝ), 2 / x ^ 2) x = (-4) / x ^ 3 with a new variable x, but no way of also constraining x≠ 0

[Kyle Miller]

You might be looking for docs#set.eq_on, which is the relation that two functions are equal on a particular set

[Mario Carneiro]

That's because trying to prove that theorem by rewriting deriv (λ (x : ℝ), 2 / x ^ 2) to λ x : ℝ, -4/x^3 is a wrong move, it's not true

[Yaël Dillies]

This is where your mistake lies. You cannot apply funext because both functions are only equal away from 0.

[Mario Carneiro]

(actually, it might be true because of fortuitous use of 1/0 = 0)

[Max Bobbin]

Ah, I see, let me try that

[Max Bobbin]

I think I see, since funext is for everywhere, but I need to only look at the set of all numbers exlcuding zero

[Vincent Beffara]

You might also be looking for docs#filter.eventually_eq.deriv or something similar, to work locally

[Yaël Dillies]

Mario Carneiro said:

(actually, it might be true because of fortuitous use of 1/0 = 0)

I was expecting docs#deriv_inv to be that unconditional result, but it's not...

[Anatole Dedecker]

Wait it is right ?

[Yaël Dillies]

I think so, yeah, because either c x ≠ 0 in which it holds just as in real maths, or c x = 0 in which case λ x, (c x)⁻¹ is not differentiable so deriv (λ x, (c x)⁻¹) x = 0 = (c x)⁻¹.

[Vincent Beffara]

Wait, if c x is 1 / x (and hence 0 at 0), then λ x, (c x)⁻¹ is id and is differentiable at 0 IIUC?

[Mario Carneiro]

I don't think that function c x is differentiable at 0

[Mario Carneiro]

this being a precondition of the theorem

[Vincent Beffara]

Sure it does not has_deriv_at zero, but that means that deriv c 0 = 0 as a garbage value and my remark was just about the equality deriv (λ x, (c x)⁻¹) x = 0 = -(c x ^ 2)⁻¹ * deriv c x being possibly true unconditionally, not about docs#deriv_inv'' itself