Zulip Chat Archive

Stream: Is there code for X?

Topic: Linear map is continuous if it's continuous at zero


Bhavik Mehta (Apr 15 2021 at 16:49):

Here's my goal:

import data.real.basic
import topology.algebra.ordered
import topology.instances.real
import analysis.normed_space.operator_norm

noncomputable theory

lemma continuous_linear_map_of_continuous_at_zero {E F : Type*} [normed_group E] [normed_space  E]
  [normed_group F] [normed_space  F] (f : E →ₗ[] F) (hf : continuous_at f (0:E)):
  continuous f :=
begin

end

The closest things I can see in mathlib are to strengthen docs#multilinear_map.exists_bound_of_continuous (its proof only actually uses continuity at zero anyway) and then use docs#linear_map.continuous_of_bound but is there a more direct way?

Patrick Massot (Apr 15 2021 at 16:56):

open filter
open_locale topological_space

lemma continuous_linear_map_of_continuous_at_zero {E F : Type*} [normed_group E] [normed_space  E]
  [normed_group F] [normed_space  F] (f : E →ₗ[] F) (hf : continuous_at f (0:E)):
  continuous f :=
begin
  have : tendsto f (𝓝 0) (𝓝 0), by simpa using hf.tendsto,
  exact (uniform_continuous_of_tendsto_zero this).continuous,
end

Bhavik Mehta (Apr 15 2021 at 16:56):

Amazing, thank you Patrick!

Bhavik Mehta (Apr 15 2021 at 16:56):

Here was the attempt I'd just finished up, yours is much nicer :)

lemma continuous_linear_map_of_continuous_at_zero {E F : Type*} [normed_group E] [normed_space  E]
  [normed_group F] [normed_space  F] (f : E →ₗ[] F) (hf : continuous_at f (0:E)):
  continuous f :=
begin
  rw continuous_iff_continuous_at,
  intros x,
  change filter.tendsto _ _ _,
  change filter.tendsto _ _ _ at hf,
  rw normed_group.tendsto_nhds_nhds at  hf,
  intros ε ,
  obtain δ, hδ₁, hδ₂ := hf ε ,
  refine δ, hδ₁, λ x' hx', by simpa using hδ₂ (x' - x) (by simpa using hx')⟩,
end

Patrick Massot (Apr 15 2021 at 16:56):

I don't know why this isn't in mathlib.

Patrick Massot (Apr 15 2021 at 16:57):

maybe it is somewhere

Patrick Massot (Apr 15 2021 at 16:59):

Regarding your proof: the main hint is this lemma has nothing to do with norms.

Patrick Massot (Apr 15 2021 at 16:59):

lemma continuous_group_hom_of_continuous_at_zero {E F : Type*}
  [add_comm_group E] [add_comm_group F] [uniform_space E] [uniform_add_group E]
  [uniform_space F] [uniform_add_group F]  (f : E →+ F) (hf : continuous_at f (0:E)) :
  continuous f :=
begin
  have : tendsto f (𝓝 0) (𝓝 0), by simpa using hf.tendsto,
  exact (uniform_continuous_of_tendsto_zero this).continuous,
end

Patrick Massot (Apr 15 2021 at 16:59):

(also nothing to do with scalar multiplication)


Last updated: Dec 20 2023 at 11:08 UTC