## Stream: maths

### Topic: define a function by cases

#### Joseph Corneli (Apr 11 2019 at 11:39):

I know about function.restrict, which allows me to take a function and look at it over a subtype, but what about going the other way, and building up a function from components? E.g., suppose I want to define $\chi_{[0,1]}$ which is 1 on $[0,1]$ and 0 elsewhere?

#### Chris Hughes (Apr 11 2019 at 11:42):

import data.real.basic data.set.intervals

def f (x : ℝ) : ℝ :=
if x ∈ set.Icc (0 : ℝ) 1 then 1 else 0


thanks

#### Joseph Corneli (Apr 11 2019 at 11:49):

I wonder why I did not retain this information after reading TIPL.

#### Joseph Corneli (Apr 11 2019 at 11:50):

Probably it was a case of too much new stuff all at once.

#### Joseph Corneli (Apr 11 2019 at 11:52):

Actually, Lean complains about the code above:

failed to synthesize type class instance for
x : ℝ
⊢ decidable (x ∈ set.Icc 0 1)


#### Chris Hughes (Apr 11 2019 at 11:53):

Put this at the start of your file.
local attribute [instance] classical.prop_decidable

#### Joseph Corneli (Apr 11 2019 at 11:56):

Nice, it works now.

Thanks Chris.

#### Joseph Corneli (Apr 11 2019 at 12:12):

Maybe you can guess what my next question is. I'm stuck again.

import data.real.basic data.set.intervals topology.basic analysis.exponential
local attribute [instance] classical.prop_decidable

noncomputable def unit_indicator (x : ℝ) : ℝ := if x ∈ set.Icc (0 : ℝ) 1 then 1 else 0

noncomputable def on_unit := function.restrict unit_indicator (set.Icc (0 : ℝ) 1)

lemma on_unit_cont : continuous on_unit :=
begin
unfold on_unit function.restrict unit_indicator,
-- ...
end


#### Chris Hughes (Apr 11 2019 at 12:17):

lemma on_unit_eq_one : on_unit = (λ x, 1) := funext (λ x, if_pos x.property)

lemma on_unit_cont : continuous on_unit :=
begin
rw on_unit_eq_one,
exact continuous_const,
-- ...
end


#### Joseph Corneli (Apr 11 2019 at 12:19):

Aha, "function extensionality" is great

#### Joseph Corneli (Apr 11 2019 at 15:54):

Here's another related question. Why can't I unfold fake_abs here?

import data.real.basic data.set.intervals topology.basic analysis.exponential
local attribute [instance] classical.prop_decidable

open real

noncomputable def fake_abs (x : ℝ) : ℝ := if x ≤ 0 then -x else x

lemma fake_abs_is_abs : fake_abs = (λ x, abs x)  :=
begin
unfold fake_abs,
sorry,
end


I get

simplify tactic failed to simplify
state:
⊢ fake_abs = λ (x : ℝ), abs x


#### Chris Hughes (Apr 11 2019 at 15:58):

unfold does simp using the equation lemmas. Try looking at the output of this

noncomputable def fake_abs (x : ℝ) : ℝ := if x ≤ 0 then -x else x

noncomputable def fake_abs' : ℝ → ℝ := λ x, if x ≤ 0 then -x else x

#print fake_abs.equations._eqn_1

#print fake_abs'.equations._eqn_1


unfold fake_abs' will have the behaviour you want, due to the different equation lemma.

#### Kevin Buzzard (Apr 11 2019 at 16:14):

This also makes progress:

import data.real.basic data.set.intervals topology.basic analysis.exponential
local attribute [instance] classical.prop_decidable

open real

noncomputable def fake_abs (x : ℝ) : ℝ := if x ≤ 0 then -x else x

lemma fake_abs_is_abs : fake_abs = (λ x, abs x)  :=
begin
ext,
unfold fake_abs,
sorry
end


Note: #print prefix fake_abs.equations prints the equation lemmas for your fake_abs.

#### Kevin Buzzard (Apr 11 2019 at 16:15):

The way you set it up, unfold can only make progress when faced with something of the form fake_abs x (and not just fakeabs); this is what the functional extensionality tactic gives you.

#### Joseph Corneli (Apr 11 2019 at 17:58):

I could prove that fake_abs is equal to abs, but I've gotten stuck with the continuity part of the exercise.

import data.real.basic data.set.intervals topology.basic analysis.exponential tactic.fin_cases
local attribute [instance] classical.prop_decidable

open real

-- Use the version that will unfold properly
noncomputable def fake_abs : ℝ → ℝ := λ x, if x < 0 then -x else x

lemma fake_abs_is_abs : fake_abs = (λ x, abs x)  :=
begin
unfold fake_abs abs,
funext,
by_cases x < 0,
simp [if_pos h],
have he : -x > 0, from neg_pos_of_neg h,
have hl : -x > x, from lt_trans h he,
have hm : max x (-x) = -x, from max_eq_right_of_lt hl,
exact hm.symm,
simp [if_neg h],
have he : 0 ≤ x, from begin simp at h, exact h, end,
have hl : -x ≤ 0, from neg_nonpos_of_nonneg he,
have hll : -x ≤ x, from le_trans hl he,
have hm : max x (-x) = x, from max_eq_left hll,
exact hm.symm,
end

lemma continuous_fake_abs : continuous fake_abs := begin
unfold fake_abs,
-- ⊢ continuous (λ (x : ℝ), ite (x < 0) (-x) x)
end


#### Joseph Corneli (Apr 11 2019 at 18:04):

I guess I could break this down into two lemmas, each similar to on_unit_eq_one from before.

#### Reid Barton (Apr 11 2019 at 18:06):

You could try apply continuous_if--now you'll have several more things to prove

#### Scott Olson (Apr 11 2019 at 18:07):

I'm assuming it's against the spirit of the exercise to rw fake_abs_is_abs, apply continuous_abs?

#### Joseph Corneli (Apr 11 2019 at 18:07):

Right, and here I was thinking that continuous_if would be too much magic because the boundary would be in general too complicated.

#### Joseph Corneli (Apr 11 2019 at 18:09):

@Scott Olson :grinning_face_with_smiling_eyes:

#### Reid Barton (Apr 11 2019 at 18:11):

Identifying the boundary is the main work that you will have to do

#### Reid Barton (Apr 11 2019 at 18:11):

although I think it's also not that hard

#### Joseph Corneli (Apr 11 2019 at 18:14):

It should be interesting... a bit of topology sneaks in after all. Time for dinner here; thanks for the help.

Last updated: May 10 2021 at 06:13 UTC