Zulip Chat Archive

Stream: maths

Topic: define a function by cases


view this post on Zulip 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 χ[0,1]\chi_{[0,1]} which is 1 on [0,1][0,1] and 0 elsewhere?

view this post on Zulip 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

view this post on Zulip Joseph Corneli (Apr 11 2019 at 11:45):

thanks

view this post on Zulip Joseph Corneli (Apr 11 2019 at 11:49):

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

view this post on Zulip Joseph Corneli (Apr 11 2019 at 11:50):

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

view this post on Zulip 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)

view this post on Zulip Chris Hughes (Apr 11 2019 at 11:53):

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

view this post on Zulip Joseph Corneli (Apr 11 2019 at 11:56):

Nice, it works now.

view this post on Zulip Joseph Corneli (Apr 11 2019 at 11:57):

Thanks Chris.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Joseph Corneli (Apr 11 2019 at 12:19):

Aha, "function extensionality" is great

view this post on Zulip Joseph Corneli (Apr 11 2019 at 12:20):

Denied by Haskellists IIUC

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Reid Barton (Apr 11 2019 at 18:06):

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

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Joseph Corneli (Apr 11 2019 at 18:09):

@Scott Olson :grinning_face_with_smiling_eyes:

view this post on Zulip Reid Barton (Apr 11 2019 at 18:11):

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

view this post on Zulip Reid Barton (Apr 11 2019 at 18:11):

although I think it's also not that hard

view this post on Zulip 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