## Stream: Is there code for X?

### Topic: continuous_on.dif

#### Shing Tak Lam (Apr 14 2021 at 18:02):

Right now, I'm trying to prove that this triangular function $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


#### Eric Wieser (Apr 14 2021 at 19:49):

(docs#continuous_on.if for reference)

#### Eric Wieser (Apr 14 2021 at 19:58):

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

#### 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.

#### 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


#### 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?

#### 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.

#### Mario Carneiro (Apr 14 2021 at 20:21):

the proof in both senses

#### 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 frontiers 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
end


#### 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!

#### 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

Alright, thanks!

#### 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