Zulip Chat Archive

Stream: maths

Topic: continuous function to pi type


view this post on Zulip Johan Commelin (May 23 2018 at 09:58):

I have no clue how to prove this:

lemma continuous.pi_mk {X I : Type*} {Y : I  Type*}
[topological_space X] [Πi, topological_space (Y i)] (f : Πi, X  (Y i)) (H : Πi, continuous (f i))
: continuous (λ x i, f i x) := sorry

view this post on Zulip Kevin Buzzard (May 23 2018 at 09:59):

Can you prove it in maths?

view this post on Zulip Kevin Buzzard (May 23 2018 at 09:59):

:-)

view this post on Zulip Kevin Buzzard (May 23 2018 at 09:59):

i.e. "is it true"

view this post on Zulip Johan Commelin (May 23 2018 at 09:59):

Unless I made a stupid mistake: yes

view this post on Zulip Mario Carneiro (May 23 2018 at 10:00):

how is the pi topology defined?

view this post on Zulip Johan Commelin (May 23 2018 at 10:00):

It just says that Pi is some sort of categorical product on steroids

view this post on Zulip Kevin Buzzard (May 23 2018 at 10:00):

what Mario said

view this post on Zulip Johan Commelin (May 23 2018 at 10:00):

If I have continuous maps to all the factors, I get a continuous map to the Pi

view this post on Zulip Kevin Buzzard (May 23 2018 at 10:00):

(in Lean)

view this post on Zulip Johan Commelin (May 23 2018 at 10:00):

instance Pi.topological_space {β : α  Type v} [t₂ : Πa, topological_space (β a)]
 : topological_space (Πa, β a) :=
a, topological_space.induced (λf, f a) (t₂ a)

view this post on Zulip Mario Carneiro (May 23 2018 at 10:01):

so look for theorems about continuity on induced

view this post on Zulip Johan Commelin (May 23 2018 at 10:01):

There are loads of those... but how do I deal with the ⨆a, that is in front?

view this post on Zulip Mario Carneiro (May 23 2018 at 10:01):

look for continuity on a Sup

view this post on Zulip Johan Commelin (May 23 2018 at 10:02):

there is only continuity for sup, not Sup

view this post on Zulip Mario Carneiro (May 23 2018 at 10:03):

I think it's called that... serach for the bigcup

view this post on Zulip Johan Commelin (May 23 2018 at 10:03):

I'm already down 5 rabbit holes, I really hope I don't need to go down this one as well...

view this post on Zulip Johan Commelin (May 23 2018 at 10:03):

Search for gives No results in continuity.lean

view this post on Zulip Mario Carneiro (May 23 2018 at 10:04):

hm, looks like it is missing from the list at continuity.lean

view this post on Zulip Johan Commelin (May 23 2018 at 10:05):

Right, there is constructors for products of two topological spaces, and continous maps towards them, etc... but for Pi types this seems missing. And I don't know exactly how to prove this stuff...

view this post on Zulip Johan Commelin (May 23 2018 at 10:06):

/me doesn't know anything about Sup and friends

view this post on Zulip Mario Carneiro (May 23 2018 at 10:06):

okay, so use the existing theorems as guides and write your own version for continuity on supr

view this post on Zulip Johan Commelin (May 23 2018 at 10:06):

\me goes down rabbit hole # 6

view this post on Zulip Mario Carneiro (May 23 2018 at 10:06):

(or I can, if this is going too far afield)

view this post on Zulip Mario Carneiro (May 23 2018 at 10:06):

I'm just showing you what I would do

view this post on Zulip Johan Commelin (May 23 2018 at 10:07):

Well, I'm trying to prove that the face map between two standard simplices is continuous...

view this post on Zulip Johan Commelin (May 23 2018 at 10:08):

@Mario Carneiro At the moment, I don't even know how to write the statement for Sup

view this post on Zulip Mario Carneiro (May 23 2018 at 10:20):

here you go:

lemma continuous_Sup_dom {t₁ : set (tspace α)} {t₂ : tspace β}
  {t : tspace α} (h₁ : t ∈ t₁) : cont t t₂ f → cont (Sup t₁) t₂ f :=
continuous_le_dom (le_Sup h₁)

lemma continuous_Sup_rng {t₁ : tspace α} {t₂ : set (tspace β)}
  (h : ∀t∈t₂, cont t₁ t f) : cont t₁ (Sup t₂) f :=
continuous_Inf_rng
  (λ t ht, show t ≤ coinduced f t₁, from h t ht)
  continuous_coinduced_rng

lemma continuous_supr_dom {t₁ : ι → tspace α} {t₂ : tspace β}
  {i : ι} : cont (t₁ i) t₂ f → cont (supr t₁) t₂ f :=
continuous_Sup_dom ⟨i, rfl⟩

lemma continuous_supr_rng {t₁ : tspace α} {t₂ : ι → tspace β}
  (h : ∀i, cont t₁ (t₂ i) f) : cont t₁ (supr t₂) f :=
continuous_Sup_rng $ assume t ⟨i, (t_eq : t = t₂ i)⟩, t_eq.symm ▸ h i

view this post on Zulip Mario Carneiro (May 23 2018 at 10:20):

I just copied the Inf stuff and dualized everything

view this post on Zulip Johan Commelin (May 23 2018 at 10:29):

Ok, thanks!

view this post on Zulip Johan Commelin (May 23 2018 at 10:29):

Let me see if I can continue with rabbit hole # 5 (-;

view this post on Zulip Johan Commelin (May 23 2018 at 10:53):

Hurray!

lemma continuous.pi_mk {X I : Type*} {Y : I  Type*}
[t₁ : topological_space X] [t₂ : Πi, topological_space (Y i)] (f : Πi, X  (Y i)) (H : Πi, continuous (f i))
: continuous (λ x i, f i x) :=
begin
let YY := (Πi, Y i),
apply continuous_Sup_rng,
intros t ht,
cases ht with i hi,
simp at *,
rw hi,
apply continuous_induced_rng,
unfold function.comp,
exact H i,
end

view this post on Zulip Johan Commelin (May 23 2018 at 11:23):

Ok, so now I'm stuck with this MWE:

lemma continuous_sums {n : } : continuous (λ x : ((fin n)  ), univ.sum x) := sorry

view this post on Zulip Johan Commelin (May 23 2018 at 11:24):

Whatever I try, I'm pulled hard into all sorts of foldr stuff. And I'm completely out of my comfort zone.

view this post on Zulip Mario Carneiro (May 23 2018 at 11:24):

that's not a trivial theorem

view this post on Zulip Johan Commelin (May 23 2018 at 11:25):

I would like to mumble some think like... well, addition is continuous... if you repeatedly add, you get continuity by induction

view this post on Zulip Johan Commelin (May 23 2018 at 11:25):

Can I foldr the continuity proof off add?

view this post on Zulip Mario Carneiro (May 23 2018 at 11:25):

I guess you can prove it by induction on n, you will need to show that fin (succ n) -> R is homeomorphic to R x (fin n -> R)

view this post on Zulip Johan Commelin (May 23 2018 at 11:27):

To link back to the discussion with Kevin, from about an hour ago... do you think this could be made into a trivial theorem?

view this post on Zulip Mario Carneiro (May 23 2018 at 11:27):

no

view this post on Zulip Mario Carneiro (May 23 2018 at 11:28):

okay, maybe that's too strong, you might be able to prove it by induction on the set instead

view this post on Zulip Johan Commelin (May 23 2018 at 11:29):

that sounds closer to what I wanted to mumble

view this post on Zulip Mario Carneiro (May 23 2018 at 11:29):

in that case you want to use finset.induction_on

view this post on Zulip Mario Carneiro (May 23 2018 at 11:30):

and the IH says that a sum of continuous functions over set s is continuous

view this post on Zulip Johan Commelin (May 23 2018 at 11:33):

Ok, I'm going to try this. Thanks!

view this post on Zulip Patrick Massot (May 23 2018 at 12:43):

Johan, you may already know, but just in case: there very easy clean up steps you can run on such proofs. YY is never used. unfold is actually much less useful that one thinks in the beginning, so I always try to remove all unfold once a proof work. And then we always try to get rid of simp in the middle of proofs. The result is:

lemma continuous.pi_mk {X I : Type*} {Y : I  Type*}
[t₁ : topological_space X] [t₂ : Πi, topological_space (Y i)] (f : Πi, X  (Y i)) (H : Πi, continuous (f i))
: continuous (λ x i, f i x) :=
begin
    apply continuous_Sup_rng,
    intros t ht,
    cases ht with i hi,
    rw hi,
    apply continuous_induced_rng,
    exact H i,
end

view this post on Zulip Patrick Massot (May 23 2018 at 12:44):

Out of curiosity, I also tried to build a term proof, but haven't succeeded because of the mysterious rewrite in the middle (which rewrites implicit arguments, which has the weird effect of not changing the visible goal)

view this post on Zulip Patrick Massot (May 23 2018 at 12:45):

I can't get more obfuscated than:

lemma continuous.pi_mk {X I : Type*} {Y : I  Type*}
[t₁ : topological_space X] [t₂ : Πi, topological_space (Y i)] (f : Πi, X  (Y i)) (H : Πi, continuous (f i))
: continuous (λ x i, f i x) :=
continuous_Sup_rng $ λ t ht, match ht with i, hi := by rw hi ; apply continuous_induced_rng ; exact (H i) end

view this post on Zulip Johannes Hölzl (May 23 2018 at 12:49):

For the sum proof: its easiest to generalize for finset, and then go from list to multiset to finset. I will add this to mathlib:

lemma continuous_supr_rng
  {ι : Sort*} {α : Type*} {β : Type*} {t₁ : topological_space α} {t₂ : ι  topological_space β}
  {f : α  β}
  (h : i, @continuous _ _ t₁ (t₂ i) f) :
  @continuous _ _ t₁ (lattice.supr t₂) f :=
continuous_iff_le_coinduced.2 $ lattice.supr_le $ assume i, continuous_iff_le_coinduced.1 (h i)

lemma continuous.pi_mk
  {X I : Type*} {Y : I  Type*} [t₁ : topological_space X] [t₂ : Πi, topological_space (Y i)]
  (f : Πi, X  (Y i)) (H : Πi, continuous (f i)) :
  continuous (λ x i, f i x) :=
continuous_supr_rng $ assume i, continuous_induced_rng $ H i

lemma continuous_list_sum {α : Type*} {β : Type*} {γ : Type*}
  [topological_space α] [topological_space β] [add_comm_monoid β] [topological_add_monoid β]
  {f : γ  α  β} :
  l:list γ, (cl, continuous (f c))  continuous (λa, (l.map (λc, f c a)).sum)
| []       _ := by simp [continuous_const]
| (f :: l) h :=
  begin
    simp,
    exact continuous_add
      (h f (list.mem_cons_self _ _))
      (continuous_list_sum l (assume c hc, h c (list.mem_cons_of_mem _ hc)))
  end

lemma continuous_multiset_sum {α : Type*} {β : Type*} {γ : Type*}
  [topological_space α] [topological_space β] [add_comm_monoid β] [topological_add_monoid β]
  {f : γ  α  β} (s : multiset γ) :
  (cs, continuous (f c))  continuous (λa, (s.map (λc, f c a)).sum) :=
quot.induction_on s $ by simp; exact continuous_list_sum

lemma continuous_finset_sum {α : Type*} {β : Type*} {γ : Type*}
  [topological_space α] [topological_space β] [add_comm_monoid β] [topological_add_monoid β]
  (f : γ  α  β) (s : finset γ) :
  (cs, continuous (f c))  continuous (λa, s.sum (λc, f c a)) :=
continuous_multiset_sum _

view this post on Zulip Johan Commelin (May 23 2018 at 12:50):

@Patrick Massot Yes, you are completely right. But it seems the work is now already done (-;

view this post on Zulip Mario Carneiro (May 23 2018 at 12:57):

you can see how Johannes built the term proof for pi_mk; the key is to use continuous_supr_rng not continuous_Sup_rng because the definition uses supr (the indexed supremum) not Sup (the set supremum). In fact supr is defined in terms of Sup, but if you apply the wrong theorem it unfolds this definition and things get harder.

view this post on Zulip Johan Commelin (May 23 2018 at 13:06):

Yes, I will take a closer look. I think I can learn a lot from how Johannes improved my kludge

view this post on Zulip Patrick Massot (May 23 2018 at 13:13):

Sure. But this is too efficient in a sense. My message was focused on easy local clean up, that you can actually do without any understanding of the proof. Of course this is only the first step. Really efficient proofs like Johannes' require actual thinking

view this post on Zulip Mario Carneiro (May 23 2018 at 13:15):

you can also look at my term proof of continuous_supr_rng, which uses the \t for rewriting

view this post on Zulip Patrick Massot (May 23 2018 at 13:17):

I'm a bit frustrated by this \t thing. I know it's somehow the term version of rw and I see it everywhere in mathlib, but I was almost never able to use it

view this post on Zulip Mario Carneiro (May 23 2018 at 13:17):

I admit it was a bit delicate for me at first

view this post on Zulip Mario Carneiro (May 23 2018 at 13:18):

it is so much weaker than the lean 2 version, it fails whenever the expected type or the thing to rewrite with has metavariables

view this post on Zulip Johan Commelin (May 23 2018 at 13:19):

Anyway, I just proved that the face map between standard simplices is continuous!

view this post on Zulip Johan Commelin (May 23 2018 at 13:19):

The proof is not cleaned up. But it works (-;

view this post on Zulip Mario Carneiro (May 23 2018 at 13:20):

but it's often just the thing when you want to rewrite with an equality in the context

view this post on Zulip Patrick Massot (May 23 2018 at 13:23):

What about my attempt? Can you use \t there? (without switching to continuous_supr_rng)

view this post on Zulip Mario Carneiro (May 23 2018 at 13:24):

yes, the proof should be almost identical to the one I pointed at

view this post on Zulip Johan Commelin (May 23 2018 at 13:25):

Ok, like I said, the proofs are still ugly. But here goes nothing: https://github.com/jcommelin/mathlib/commit/fec9db2028bea163352f574055dad44029d04788

view this post on Zulip Mario Carneiro (May 23 2018 at 13:25):

lemma continuous.pi_mk
  {X I : Type*} {Y : I → Type*} [t₁ : topological_space X] [t₂ : Πi, topological_space (Y i)]
  (f : Πi, X → (Y i)) (H : Πi, continuous (f i)) :
  continuous (λ x i, f i x) :=
continuous_Sup_rng $ assume t ⟨i, e⟩, e.symm ▸ continuous_induced_rng (H i)

view this post on Zulip Patrick Massot (May 23 2018 at 15:06):

Hum, I think I stupidly missed the eq.symm when I tried

view this post on Zulip Johannes Hölzl (May 23 2018 at 15:31):

@Johan Commelin I forgot that there is already tendsto_sum, so you could also derive continuous_finset_sum from this.
Anyway, this all is now in mathlib.

view this post on Zulip Johan Commelin (May 23 2018 at 16:54):

Thanks a lot! I will merge into my fork. Once I clean my stuff up, I think I will make a PR


Last updated: May 18 2021 at 08:14 UTC