Zulip Chat Archive

While trying to do some analysis I realized that piecewise functions are quite important. For example, you might have a function defined on R \ {0}, which is continuous at 0 with limit y. You then need to define a function g as f(x) when x != 0 and y when x = 0 to be able to prove continuous_at g 0 or continuous g.
An explicit example of this kind of situation would be the following:

import analysis.complex.basic
import data.complex.exponential
universes u v w
noncomputable theory

def f : ℝ -> ℝ := λ x, ((has_inv.inv x) * real.sin x)
def g : ℝ -> ℝ := set.piecewise {0} 1 f

lemma cont : continuous g :=
  begin
    rw metric.continuous_iff,
    unfold dist,
    unfold g,
    unfold f,
    unfold set.piecewise,
    sorry,
  end

⊢ ∀ (b ε : ℝ), ε > 0 → (∃ (δ : ℝ) (H : δ > 0),
∀ (a : ℝ), abs (a - b) < δ → abs (ite (a ∈ {0}) (1 a) (a⁻¹ * real.sin a)
                                 - ite (b ∈ {0}) (1 b) (b⁻¹ * real.sin b)) < ε)

When resolving this kind of situation I can end up with a goal that insolves several ite with possibly each different functions and propositions of the form "variable" \in "set". I'm not looking for a way to solve this explicit problem above, but how to efficiently deal with many ite in this kind of situation.
I have found the theorems ite_eq_iff and ite_apply, which would allow me to deal with the situations above, but in more complicated situations they feel a bit inefficient and complicated to apply.
Could it be possible to have a method which allows you to split an expression involving n ite with n different variables directly into 2^n cases?

Mario Carneiro (Oct 24 2020 at 10:28):

that would be split_ifs

Mario Carneiro (Oct 24 2020 at 10:28):

but I think you should not do this kind of big case split unless you have to

Mario Carneiro (Oct 24 2020 at 10:30):

In this case, what you want is a theorem that says that a set.piecewise is continuous if the two branches agree on the frontier of the if-predicate; this is called the pasting lemma and I'm pretty sure mathlib has it already

Mario Carneiro (Oct 24 2020 at 10:30):

docs#continuous_if

Mario Carneiro (Oct 24 2020 at 10:37):

actually I think you need docs#continuous_if' since the original function is not continuous on the whole domain

Golol (Oct 24 2020 at 10:45):

Thanks, split_ifs is exactly what I was looking for! The theorems continuous_if and continuous_if' are great too but damn, these names do make them hard to find if you're looking for something with "ite" or "piecewise" in the name.

Mario Carneiro (Oct 24 2020 at 10:49):

it's usually referred to as if, except in a few (very popular) lemmas in core

Mario Carneiro (Oct 24 2020 at 10:50):

part of the reason for the ugly ite name is that if is a keyword

Golol (Oct 24 2020 at 10:55):

Oh I see, the "if" in "continuous_if" refers to the presence of "ite", not "-> continuous ...".

Mario Carneiro (Oct 24 2020 at 11:03):

no, that's always of

Mario Carneiro (Oct 24 2020 at 11:04):

or occasionally imp in logic files

Heather Macbeth (Oct 24 2020 at 15:05):

I think what's missing here is a punctured-neighbourhood lemma for continuity: a function is continuous if and only if for all $c$ , as $x$ tends to $c$ but without being equal to $c$ , $f(x)$ tends to $f(c)$ . I'm not sure whether we have this! @Anatole Dedecker or @Patrick Massot might know. It should be formulated using docs#nhds_within. Then you will only have two cases.