I can't make sense of this error

Stream: new members

[Icaro Costa]

This is my code:

import analysis.calculus.deriv
import data.real.basic
import data.list.basic
import tactic
import algebra.big_operators.basic
import data.nat.interval

import algebra.group.defs

open_locale big_operators

open finset

/-Function definitions-/
variable (f : ℝ → ℝ)
variable (u : ℝ → ℝ)
variable (C : ℕ → ℝ)

noncomputable def D : (ℝ → ℝ) → (ℝ → ℝ)
  | a := deriv a

noncomputable def Dn : (ℕ) → (ℝ → ℝ) → (ℝ → ℝ)
  | 0 := id
  | 1 := D
  | (a+1) := D ∘ Dn a

noncomputable def h (n : ℕ)(x : ℝ) : ℝ := ∑ p in Icc 1 n, (C p) * (((Dn (n-p) (D u)) x)^p) * ((Dn p u) x)

noncomputable def Dnfu (n : ℕ) : ℝ → ℝ := (Dn n) (f ∘ u)

#check Dn 1 (f ∘ u)
#check Dnfu 1

The output of #check Dn 1 (f ∘ u) is Dn 1 (f ∘ u) : ℝ → ℝ, which is what I'm expecting. However, #check Dnfu 1 outputs Dnfu 1 : (ℝ → ℝ) → ℕ → ℝ → ℝ. Why is that?

[Yakov Pechersky]

It's because you have

variable (f : ℝ → ℝ)
variable (u : ℝ → ℝ)

so Dnfu (f : ℝ → ℝ) (u : ℝ → ℝ) (n : ℕ) : ℝ → ℝ := ...

[Sky Wilshaw]

Note that lean can interpret the symbol 1 as quite a lot of things, and in this case, it's interpreting it as a function ℝ → ℝ.

[Yakov Pechersky]

while neither f nor u are mentioned in the body of def Dn, so they are not inferred to be variables/arguments of that function.

[Icaro Costa]

Sky Wilshaw said:

Note that lean can interpret the symbol 1 as quite a lot of things, and in this case, it's interpreting it as a function ℝ → ℝ.

Wait, really? How do I just write "one"

[Sky Wilshaw]

As Yakov said, the first argument to Dnfuis actually f.

[Yakov Pechersky]

#check Dnfu f u 1

[Icaro Costa]

Oh, so it still expects f and u even though they aren't arguments of Dnfu?

[Yakov Pechersky]

Yakov Pechersky said:

It's because you have

variable (f : ℝ → ℝ)
variable (u : ℝ → ℝ)

so Dnfu (f : ℝ → ℝ) (u : ℝ → ℝ) (n : ℕ) : ℝ → ℝ := ...

because f and u are mentioned in the body of Dnfu. How could f and u not be arguments of Dnfu if they're mentioned in the body?

[Sky Wilshaw]

Actually, lean detects that they are arguments! The keyword variable makes f and u parameters to any function that uses them.

[Icaro Costa]

Sky Wilshaw said:

Actually, lean detects that they are arguments! The keyword variable makes f and u parameters to any function that uses them.

Oh, is there a way to make them just "arbitrary" functions? As some sort of constant

[Sky Wilshaw]

This is the correct way to do that.

[Sky Wilshaw]

A "constant in the environment" is exactly the same as a parameter to a function.

[Sky Wilshaw]

But when you used these functions in #check, lean didn't know if you really wanted to use the f from the environment or some other f.

[Icaro Costa]

Sky Wilshaw said:

But when you used these functions in #check, lean didn't know if you really wanted to use the f from the environment or some other f.

Ok, it's making sense now. How do I tell #check that I want to use the same f without having to pass it as a parameter?

[Sky Wilshaw]

I don't know of an easy way to do this. Most of the time, you won't be using #check, so this isn't usually a problem.

[Sky Wilshaw]

I mean, you'll only use #check while testing.

[Sky Wilshaw]

When you're writing theorems, you don't need to pass f explicitly.

[Icaro Costa]

Ok, I think I can live with that.

[Icaro Costa]

Thanks for the help, Sky and Yakov