continuous_on.dif

Stream: Is there code for X?

[Shing Tak Lam]

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]

(docs#continuous_on.if for reference)

[Eric Wieser]

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

[Floris van Doorn]

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]

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]

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]

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]

the proof in both senses

[Shing Tak Lam]

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

[Shing Tak Lam]

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]

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

[Shing Tak Lam]

Alright, thanks!

[Floris van Doorn]

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.