Declare a continuous function space

Stream: new members

[Robert hackman]

Hi,
I would like to define a continuous function space. In lean3 that worked with def C := map_continuous (Icc 0 1) ℝ how does work in lean4? I've been looking through mathlib4 but couldn't find an equivalent. Maybe I'm just missing the correct import path.
regards

[Eric Wieser]

Are you sure that worked in lean 3?

[Eric Wieser]

I think you have the name backwards

[Eric Wieser]

#lookup3 continuous_map is how to find the Lean 4 version of things

[Robert hackman]

yeah I'm uncertain if map_continuous is even a thing in lean3, it's from an old code base. Let's rephrase the question: How do I define a continuous function space as "described" above?

[Robert hackman]

Eric Wieser said:

#lookup3 continuous_map is how to find the Lean 4 version of things

uh didn't know that thx

[Eric Wieser]

Did that work for you?

[Robert hackman]

nope, didn't find any equivalent. Could very well be that it was some internal definition...

[Anatole Dedecker]

Is docs#ContinuousMap what you want?

[Robert hackman]

uff that was so obvious(to find in the docs). thx though!

[Eric Wieser]

I'm surprised that my line of code above did not lead to exactly that

[Damiano Testa]

Eric, indeed:

import Mathlib.Tactic

#lookup3 continuous_map  -- ContinuousMap

[Robert hackman]

Eric Wieser said:

I'm surprised that my line of code above did not lead to exactly that

my fault sry

[Robert hackman]

So I'm still fighting with the next line (lol):

Mve:

import Mathlib.MeasureTheory.Integral.SetIntegral
import Mathlib.Data.Set.Intervals.Basic

open Function
open MeasureTheory

-- Define the space of continuous functions on [0, 1]
def C := ContinuousMap (Set.Icc 0 1) ℝ

-- Define the L1 norm on C([0, 1])
def L1_norm (f : C) : ℝ := ∫ x in (Set.Icc 0 1), |f.toFun x| dx

Where the last line throws: failed to synthesize instance MeasureSpace ↑(Set.Icc 0 1) and function expected at |ContinuousMap.toFun f x| term has type ℝ but I think the latter is a symptom of the first error.
I kind of understand why it throws the error, I know that the MeasureSpace ↑(Set.Icc 0 1)relates to the set defined used in the C def but I really don't know why it cannot synth. the instance. regards

[Patrick Massot]

I guess all your sets are in natural numbers since you never put any type information about 0 and 1.

[Patrick Massot]

and dx is not part of the integral notation.

[Patrick Massot]

But I guess this won't be enough since x won't have the correct type in your integral.

[Eric Wieser]

I would recommend replacing def C := with abbrev C :=, as the former makes lean forget a lot of things about continuous maps

[Eric Wieser]

Notably your can then drop the toFun

[Robert hackman]

import Mathlib.MeasureTheory.Integral.SetIntegral
import Mathlib.Data.Set.Intervals.Basic

open Function
open MeasureTheory

def I01 := (Set.Icc (0: ℝ) (1: ℝ))

abbrev C := ContinuousMap I01 ℝ

noncomputable
def L1_norm (f : C) : ℝ := ∫ x in I01, |f x|

ok thank you, the above is the current state so that's already a lot better but as @Patrick Massot already said, x has the wrong type because it's of type ℝ. One solution is to change I01 to ℝ but then I've got a different definition (I think). Because what I want is the L1 Norm over all fn C[0 1] and not ℝ. Another possible solution I thought of was changing the I01(for the L1_norm only) to a Set of Sets or smth like that

[Eric Wieser]

You should use abbrev for I01 too

[Eric Wieser]

Using def for types is usually a bad choice

[Eric Wieser]

Does removing the in I01 work?

[Wen Yang]

@Robert hackman It is more convenient to work on types than subtypes in Lean. If you decide to handle functions defined on Icc, you could try using the Function.toval' I defined in this PR: https://github.com/leanprover-community/mathlib4/pull/7449

[Eric Wieser]

I don't think I agree with that: sticking with subtypes is often just fine.

[Wen Yang]

By the way, unitInterval has been defined in mathlib4

[Eric Wieser]

docs#unitInterval

[Eric Wieser]

Note it is an abbrev as I suggest above; this means Lean doesn't care whether you write Icc 0 1 or unitInterval, it knows to treat them as the same

[Robert hackman]

ok so just removed in I01from the Integral and that makes it work, I guess it just infers what to use a function input. Thanks!

[Robert hackman]

Wen Yang said:

Robert hackman It is more convenient to work on types than subtypes in Lean. If you decide to handle functions defined on Icc, you could try using the Function.toval' I defined in this PR: https://github.com/leanprover-community/mathlib4/pull/7449

what would toVal do, it's not in the docs?

[Eric Wieser]

Removing in I01 is the same as replacing it with : I01

[Eric Wieser]

But indeed, Lean infers the latter automatically

[Wen Yang]

Robert hackman said:

what would toVal do, it's not in the docs?

It could help you to extend the function from unitInterval to R. But it has not been accepted to merge into master branch yet, so it is not in the docs.

[Robert hackman]

Eric Wieser said:

Removing in I01 is the same as replacing it with : I01

ah I tried just removing the in but that didn't work, I'm not yet used to the syntax

[Kevin Buzzard]

@Robert hackman in Lean's type theory it's often convenient to have functions which are defined on all of a type rather than just a subset of it. This is why, for example, division by zero is defined and produces a "junk value" (but nonetheless a value, namely 1/0=0). So one approach for studying functions on $[0,1]$ is to study functions on all of $\R$ and then just ignore their values outside $[0,1]$, like how we use division (a mathematician never divides by 0). The advantage of this is that if you have $x,y\in\R$ then things like $(x+y)/2$ make sense and linarith will work with goals. If you have x y : unitInterval then (x + y) / 2 will probably not typecheck and linarith will probably not prove that if $x\leq y$ and $y\leq x$ then $x=y$ (if indeed that question even typechecks): you would have to move to the reals and then move back. However there is a disadvantage too, namely that if you have two functions $\R\to\R$ which agree on $[0,1]$ but disagree somewhere else then Lean will not think that they are equal, even though they're equal on your domain of interest, so you might end up having to quotient out by an equivalence relation, which adds an extra layer of noise (rather like how using the subtype adds an extra layer of noise). So whether you use functions defined on the type $\R$ or the subtype $[0,1]$ is a design decision which needs some thought.

[Robert hackman]

Ah very interesting, very engineering like design thing to think about... I'm also a fan of having everything explicit, so having junk types or keeping generality with explicit exceptions instead of making the type "implicitly coerce" to one attribute.

[Eric Wieser]

You can always write the coercions explicitly