complex vs real limit

Stream: Is there code for X?

[Yaël Dillies]

Where does this lemma belong? Do we already have it? Or maybe it is highly generalisable in ways I'm unaware of?

lemma filter.complex_tendsto_iff_real_tendsto {α : Type*} (l : filter α) (u : α → ℝ) (x : ℝ) :
  tendsto (coe ∘ u) l (𝓝 (x : ℂ)) ↔ tendsto u l (𝓝 x) :=
⟨(complex.continuous_re.tendsto x).comp, (complex.continuous_of_real.tendsto x).comp⟩

[Anatole Dedecker]

I think this should be a special case of docs#inducing.tendsto_nhds_iff, but I can't find the fact that coe : ℝ → ℂ is an inducing (it's even an embedding actually)

[Yaël Dillies]

Oooh, could we cook that up then?

[Anatole Dedecker]

You should be able to get it from docs#complex.isometry_of_real, docs#isometry.closed_embedding and then docs#closed_embedding.to_embedding and docs#embedding.to_inducing

[Anatole Dedecker]

(Sorry I don't have access to Lean right now so I can't give you the complete proof)

[Adam Topaz]

import analysis.complex.basic

noncomputable theory

open filter
open_locale topological_space

lemma filter.complex_tendsto_iff_real_tendsto {α : Type*} (l : filter α) (u : α → ℝ) (x : ℝ) :
  tendsto (coe ∘ u) l (𝓝 (x : ℂ)) ↔ tendsto u l (𝓝 x) :=
complex.isometry_of_real.closed_embedding.to_embedding.tendsto_nhds_iff.symm

[Adam Topaz]

Just following what Anatole already said.

[Adam Topaz]

Perhaps we should have complex.closed_embedding_of_real, complex.embedding_of_real, complex.inducing_of_real, etc.

[Yaël Dillies]

Oh wow! You gotta love dot notation.

[Yaël Dillies]

I am not knowledgeable enough to decide, but yeah we needed complex_tendsto_iff_real_tendsto. What should I do then? PR that lemma?

[Adam Topaz]

My inclination is to define the topological things I mentioned above, and use complex.inducing_of_real.tendsto_nhds_iff, but maybe another maintainer who is more involved with the analysis folder can chime in. @Heather Macbeth ?

[Anatole Dedecker]

I agree with Adam, I think the best is to add the topological statements like complex.inducing_of_real and then you can just use complex.inducing_of_real.tendsto_nhds_iff directly

[Heather Macbeth]

I think stop at embedding, since we have docs#embedding.tendsto_nhds_iff.

[Adam Topaz]

We could also add closed_embedding.tendsto_nhds_iff and isometry.tendsto_nhds_iff.

[Yaël Dillies]

I think that's cleaner and less complex-specific.

[Yaël Dillies]

By the way, why is isometry a predicate while inducing, embedding, closed_embedding, open_embedding, uniform_inducing, uniform_embedding are all structures?

[Heather Macbeth]

There's both, see docs#isometric for the bundled version.

[Yaël Dillies]

Ah! Okay

[Heather Macbeth]

Or maybe I'm misunderstanding your question? Actually I don't understand why docs#inducing is

structure inducing [tα : topological_space α] [tβ : topological_space β] (f : α → β) : Prop :=
(induced : tα = tβ.induced f)

rather than

def inducing [tα : topological_space α] [tβ : topological_space β] (f : α → β) : Prop :=
tα = tβ.induced f

[Adam Topaz]

I think it's so that you use dot notation

[Yaël Dillies]

But you can use dot notation with predicates.

[Yaël Dillies]

Maybe it's to then extend it by embedding?

[Yaël Dillies]

Then you have several Prop fields

[Adam Topaz]

Can you really use dot notation with predicates? I'm thinking e.g. of docs#inducing.continuous_iff

[Heather Macbeth]

@Adam Topaz Eg, docs#isometry.dist_eq

[Adam Topaz]

Cool! TIL

[Heather Macbeth]

There's a lot of it in topology, perhaps. docs#is_open.inter

[Adam Topaz]

Oh right. I guess I knew about the is_open stuff.