Zulip Chat Archive

Stream: Is there code for X?

Topic: continuous_on.dif


view this post on Zulip Shing Tak Lam (Apr 14 2021 at 18:02):

Right now, I'm trying to prove that this triangular function f:[0,1][0,1]f : [0, 1] \to [0, 1] is continuous, but I'm struggling to find any lemmas which will help. I did find continuous_on.if, but in my example it's a dite and not an ite, so it doesn't work. Does anyone have any suggestions on how to prove this? Or what continuous_on.dif would look like?

import topology.unit_interval

open_locale unit_interval

noncomputable theory

lemma two_mul_mem_I {t : } (ht0 : 0  t) (ht : t  1/2) : 2 * t  I := by linarith, by linarith

lemma two_sub_two_mul_mem_I {t : } (ht : (1/2 : )  t) (ht' : t  1) : 2 - 2 * t  I :=
by nlinarith, by nlinarith

def f : I  I := λ x,
  if h : x.1  1/2 then
    2 * x, two_mul_mem_I x.2.1 h
  else
    2 - 2 * x, two_sub_two_mul_mem_I (not_le.1 h).le x.2.2

example : continuous f :=
begin
  unfold f,
  rw [continuous_iff_continuous_on_univ],
  sorry
end

view this post on Zulip Eric Wieser (Apr 14 2021 at 19:49):

(docs#continuous_on.if for reference)

view this post on Zulip Eric Wieser (Apr 14 2021 at 19:58):

For your example, can't you solve it by moving the dite inside the angle brackets?

view this post on Zulip Floris van Doorn (Apr 14 2021 at 20:02):

Here is a generalization, but maybe not the most general form.

import topology.continuous_on

open set

variables {α β : Type*} [topological_space α] [topological_space β]
  {p : α  Prop} [Π (a : α), decidable (p a)] {s : set α} {f g : α  β}
  {t : set β}

theorem continuous_on.dif_subtype (hp :  (a : α), a  s  frontier {a : α | p a}  f a = g a)
  (hf : continuous_on f (s  closure {a : α | p a}))
  (hg : continuous_on g (s  closure {a : α | ¬p a}))
  (h2f : maps_to f {x | p x} t) (h2g : maps_to g {x | ¬ p x} t) :
  continuous_on (λ x, if h : p x then (⟨f x, h2f h : t) else g x, h2g h⟩) s :=
sorry

It's about using dite for functions that map into a subtype.

view this post on Zulip Floris van Doorn (Apr 14 2021 at 20:13):

Now with proof:

import topology.continuous_on

open set

variables {α β : Type*} [topological_space α] [topological_space β]
  {p : α  Prop} [Π (a : α), decidable (p a)] {s : set α} {f g : α  β}
  {t : set β}

theorem continuous_on.dif_subtype (hp :  (a : α), a  s  frontier {a : α | p a}  f a = g a)
  (hf : continuous_on f (s  closure {a : α | p a}))
  (hg : continuous_on g (s  closure {a : α | ¬p a}))
  (h2f : maps_to f {x | p x} t) (h2g : maps_to g {x | ¬ p x} t) :
  continuous_on (λ x, if h : p x then (⟨f x, h2f h : t) else g x, h2g h⟩) s :=
begin
  rw [embedding_subtype_coe.continuous_on_iff],
  convert continuous_on.if hp hf hg,
  ext x, split_ifs; simp [h]
end

view this post on Zulip Eric Wieser (Apr 14 2021 at 20:17):

Do we have a lemma that says if h : p x then (⟨f x, h2f h⟩ : t) else ⟨g x, h2g h⟩ = ⟨if p x then f x else g x, _⟩ for an appropriately valued underscore?

view this post on Zulip Floris van Doorn (Apr 14 2021 at 20:19):

library_search couldn't easily find it (though I didn't let it terminate), so I'm not sure. The proof is just split_ifs; simp [h] though.

view this post on Zulip Mario Carneiro (Apr 14 2021 at 20:21):

the proof in both senses

view this post on Zulip Shing Tak Lam (Apr 15 2021 at 04:37):

Eric Wieser said:

For your example, can't you solve it by moving the dite inside the angle brackets?

Oops, I've definitely #xy -ed myself here. That example didn't need a dif, but I think for my use case I will need a dif. The general statement I'm trying to prove is this, which I don't think you can write without a dite?

import topology.unit_interval
open_locale unit_interval

example {X Y : Type} [topological_space X] [topological_space Y] (F G : X × I  Y)
  (hF : continuous F) (hG : continuous G)
-- hFG here is enough to show they agree on the appropriate `frontier`s with a bunch of other lemmas I have.
(hFG :  x, F (x, 1/2, sorry⟩) = G (x, 1/2, sorry⟩)) :
  continuous
    (λ (x : X × I),
       dite (x.snd.val  1 / 2)
         (λ (h : x.snd.val  1 / 2), F (x.fst, 2 * x.snd.val, sorry⟩))
         (λ (h : ¬x.snd.val  1 / 2), G (x.fst, 2 * x.snd.val - 1, sorry⟩))) :=
begin
  admit,
end

view this post on Zulip Shing Tak Lam (Apr 15 2021 at 05:24):

Floris van Doorn said:

Now with proof:

import topology.continuous_on

open set

variables {α β : Type*} [topological_space α] [topological_space β]
  {p : α  Prop} [Π (a : α), decidable (p a)] {s : set α} {f g : α  β}
  {t : set β}

theorem continuous_on.dif_subtype (hp :  (a : α), a  s  frontier {a : α | p a}  f a = g a)
  (hf : continuous_on f (s  closure {a : α | p a}))
  (hg : continuous_on g (s  closure {a : α | ¬p a}))
  (h2f : maps_to f {x | p x} t) (h2g : maps_to g {x | ¬ p x} t) :
  continuous_on (λ x, if h : p x then (⟨f x, h2f h : t) else g x, h2g h⟩) s :=
begin
  rw [embedding_subtype_coe.continuous_on_iff],
  convert continuous_on.if hp hf hg,
  ext x, split_ifs; simp [h]
end

Unfortunately I've realised I've #xy -ed myself when making the example, so this can't be used as-is for my issue. But this is useful for some other things I'm doing. Thanks a lot!

view this post on Zulip Eric Wieser (Apr 15 2021 at 06:06):

Even with that example, the proof approach is probably to push the dite inside until it reaches the prop terms

view this post on Zulip Shing Tak Lam (Apr 15 2021 at 06:59):

Alright, thanks!

view this post on Zulip Floris van Doorn (Apr 15 2021 at 21:18):

Would a lemma like this be helpful?

import topology.continuous_on
open_locale topological_space
open set filter

variables {α β : Type*} [topological_space α] [topological_space β]
  {p : α  Prop} [Π (a : α), decidable (p a)]

theorem continuous.dif
  {f : {x // p x}  β} {g : {x // ¬ p x}  β}
  (hp :  (a  frontier {a : α | p a}) (b : β),
    tendsto f ((𝓝 a).comap coe) (𝓝 b)  tendsto g ((𝓝 a).comap coe) (𝓝 b))
  (hf : continuous f) (hg : continuous g) :
  continuous (λ x, if h : p x then f x, h else g x, h⟩) :=
sorry

I'm not sure if this is the best way of saying that f and g agree on the frontier (I believe the hypothesis does state that, but I'm also not 100% sure about that).

Is it at all possible to reorganize your formalization so that F and G are defined on all X × \R. Sometimes making a function total makes your life easier. You can still conder them as functions on X × I, stating that they're only continuous on X × I instead of everywhere.


Last updated: May 07 2021 at 21:10 UTC