NormedAddCommGroup for real intervals

Stream: new members

[Martin C. Martin]

The Differentiable part fails with failed to synthesize instance NormedAddCommGroup ↑zero_to_three. Do I need to provide the proof of NormedAddCommGroup myself, or does it exist in Mathlib somewhere? Seems like it should exist, but I can't figure out what else to include.

import Mathlib.Data.Set.Intervals.Basic
import Mathlib.Data.Real.Basic
import Mathlib.Analysis.Calculus.FDeriv.Basic

def zero_to_three := Set.Ioo (0 : ℝ) (3 : ℝ)

noncomputable section

variable (f : zero_to_three → ℝ)
variable [Differentiable ℝ f]

end -- noncomputable

[Martin C. Martin]

If an instance exists, such as NormedAddCommGroup ℝ, how do I find it using VS Code?

[Eric Rodriguez]

does it work with abbrev zero_to_three...? The def makes zero_to_three obscure to Lean - by default, it won't look through a def.

[Martin C. Martin]

Thanks Eric, I didn't know about Lean not looking through def or abbrev. Alas, switching to abbrev didn't help.

[Eric Wieser]

Do I need to provide the proof of NormedAddCommGroup myself

This can't possibly work, because [0, 3] is not an additive group

[Martin C. Martin]

Good point. :) Why does Differentiable need it to be one?

[Eric Rodriguez]

docs#Differentiable is in the end defined as (some quantifiers over) docs#HasFDerivAtFilter, which needs the domain to have a well-defined addition and subtraction. I guess you're expecting differentiability at the end-points to be one sided, right?

[Eric Wieser]

I would guess that docs#MDifferentiable can be made to work here, but that's above my paygrade

[Martin C. Martin]

@Eric Rodriguez it's actually the open interval (0, 3) so we don't have to worry about end points. Still not a group though.

[Martin C. Martin]

My next attempt is to define the function on all of ℝ, but only declare it differentiable on the open interval. However, that fails with "invalid binder annotation, type is not a class instance
DifferentiableOn ℝ f zero_to_three"

What am I doing wrong here?

variable (f : ℝ → ℝ)
variable [DifferentiableOn ℝ f zero_to_three]

[Eric Rodriguez]

The error suggests that you can't use [] binders, but instead () or {} binders; [] would mean it's an instance, which can be searched for automatically by the system; however, this isn't turned on for DifferentiableOn

[Martin C. Martin]

Thanks. Why is it not turned on? Because of the last Set argument?

[Jireh Loreaux]

docs#Differentiable is not a class either. Why would you want it to be one?

[Martin C. Martin]

Jireh Loreaux said:

docs#Differentiable is not a class either. Why would you want it to be one?

The same reason the algebraic types are. Sometimes, you need the fact that a function is differentiable, and rather than trying to remember the name of the theorem, it would be nice if Lean could look it up itself.

But I guess many functions are not differentiable everywhere, and anyway sometimes you need the actual derivative, so deriv is the main way of using derivatives in Lean?

[Yakov Pechersky]

Typeclass synthesis is not meant to be a global proof generator.

[Yakov Pechersky]

We have tactics that are specialized for solving goals of a particular shape.

[Jireh Loreaux]

In addition, the typeclass system is already taxed, so creating undue burden is not desirable.

[Jireh Loreaux]

And (I think) even basic lemmas about differentiability would fail to be implemented as instances because Lean wouldn't be able to determine the order in which to synthesize.