Characterizations of semi-continuity.

nhds_set_semicontinuity.lean

import topology.semicontinuous

open_locale topological_space filter
open topological_space set filter

variables {α β : Type*} [topological_space α] (f : α → β) (x : α)

section

variables [linear_order α] [t : order_topology α]
include t

lemma is_topological_basis_Iio_Ioi_Ioo :
  is_topological_basis $ {univ} ∪ range Ioi ∪ range Iio ∪ range (λ a : α × α, Ioo a.1 a.2) :=
begin
  convert topological_space.is_topological_basis_of_subbasis t.topology_eq_generate_intervals,
  ext1 s, split,
  { rintro ((((rfl : _ = _) | ⟨a, rfl⟩) | ⟨b, rfl⟩) | ⟨⟨a, b⟩, rfl⟩),
    { exact ⟨_, ⟨finite_empty, empty_subset _⟩, sInter_empty⟩ },
    { exact ⟨_, ⟨finite_singleton _, singleton_subset_iff.2 ⟨a, or.inl rfl⟩⟩, sInter_singleton _⟩ },
    { exact ⟨_, ⟨finite_singleton _, singleton_subset_iff.2 ⟨b, or.inr rfl⟩⟩, sInter_singleton _⟩ },
    { refine ⟨_, ⟨(finite_singleton _).insert _, insert_subset.2
        ⟨⟨a, or.inl rfl⟩, singleton_subset_iff.2 ⟨b, or.inr rfl⟩⟩⟩, _⟩,
      rw [sInter_pair, Ioi_inter_Iio] } },
  rintro ⟨s, ⟨hf, hs⟩, rfl⟩,
  refine hf.induction_on' _ (λ s₁ S hs₁s hSs hs₁S, _),
  { rw sInter_empty, exact or.inl (or.inl $ or.inl rfl) },
  rw sInter_insert,
  set s₂ := ⋂₀ S, clear_value s₂,
  obtain ⟨a, rfl|rfl⟩ := hs hs₁s;
  rintro ((((rfl : _ = _)|⟨a₂, rfl⟩)|⟨b₂, rfl⟩)|⟨⟨a₂, b₂⟩, rfl⟩),
  { rw inter_univ, exact or.inl (or.inl $ or.inr ⟨_, rfl⟩) },
  { rw Ioi_inter_Ioi, exact or.inl (or.inl $ or.inr ⟨_, rfl⟩) },
  { exact or.inr ⟨⟨_, _⟩, rfl⟩ },
  { dsimp only, rw [← Ioi_inter_Iio, ← inter_assoc, Ioi_inter_Ioi, Ioi_inter_Iio],
    exact or.inr ⟨⟨_, _⟩, rfl⟩ },
  { rw inter_univ, exact or.inl (or.inr ⟨_, rfl⟩) },
  { rw Iio_inter_Ioi, exact or.inr ⟨⟨_, _⟩, rfl⟩ },
  { rw Iio_inter_Iio, exact or.inl (or.inr ⟨_, rfl⟩) },
  { dsimp only, rw [← Iio_inter_Ioi, ← inter_assoc, Iio_inter_Iio, Iio_inter_Ioi],
    exact or.inr ⟨⟨_, _⟩, rfl⟩ },
end

lemma nhds_set_Ici : 𝓝ˢ (Ici x) = ⨅ y < x, 𝓟 (Ioi y) :=
begin
  apply le_antisymm,
  { refine le_infi₂ (λ y hy, le_principal_iff.2 _),
    exact is_open_Ioi.mem_nhds_set.2 (λ z hz, hy.trans_le hz) },
  intros s hs,
  obtain ⟨U, ho, hxU, hUs⟩ := mem_nhds_set_iff_exists.1 hs,
  obtain ⟨_, (((rfl : _ = _) | ⟨y, rfl⟩) | ⟨y, rfl⟩) | ⟨⟨y, z⟩, rfl⟩, hx, hU⟩ :=
    is_topological_basis_Iio_Ioi_Ioo.is_open_iff.1 ho x (hxU le_rfl);
  let := hU.trans hUs,
  { rw univ_subset_iff.1 this, exact univ_mem },
  { refine mem_infi_of_mem y (mem_infi_of_mem hx $ mem_principal.2 this) },
  { convert univ_mem, rw ← univ_subset_iff,
    intros z hz, obtain hxz | hxz := le_total x z,
    exacts [hUs (hxU hxz), this (hxz.trans_lt hx)] },
  { refine mem_infi_of_mem y (mem_infi_of_mem hx.1 $ mem_principal.2 _),
    intros w hw, obtain hwz | hwz := lt_or_le w z,
    exacts [this ⟨hw, hwz⟩, hUs (hxU $ hx.2.le.trans hwz)] },
end

end

section

variables (α)

def lower_semicontinuous_topology [preorder α] [t : topological_space α] : Prop :=
t = generate_from (range Ioi)
/- https://ncatlab.org/nlab/show/semicontinuous+topology .
  When the order is linear, happen to agree with the lower topology
    (https://github.com/leanprover-community/mathlib/pull/17037) as well,
  but not the same as https://en.wikipedia.org/wiki/Lower_limit_topology -/

variable {α}
lemma is_topological_basis_Ioi [linear_order α]
  (h : lower_semicontinuous_topology α) :
  is_topological_basis $ {univ} ∪ range (Ioi : α → set α) :=
begin
  convert topological_space.is_topological_basis_of_subbasis h,
  ext1 s, split,
  { rintro ((rfl : _ = _) | ⟨a, rfl⟩),
    { exact ⟨_, ⟨finite_empty, empty_subset _⟩, sInter_empty⟩ },
    { exact ⟨_, ⟨finite_singleton _, singleton_subset_iff.2 ⟨a, rfl⟩⟩, sInter_singleton _⟩ } },
  rintro ⟨s, ⟨hf, hs⟩, rfl⟩,
  refine hf.induction_on' _ (λ s₁ S hs₁s hSs hs₁S, _),
  { rw sInter_empty, exact or.inl rfl },
  rw sInter_insert,
  set s₂ := ⋂₀ S, clear_value s₂,
  obtain ⟨a, rfl⟩ := hs hs₁s,
  rintro ((rfl : _ = _)|⟨b, rfl⟩),
  { rw inter_univ, exact or.inr ⟨_, rfl⟩ },
  { rw Ioi_inter_Ioi, exact or.inr ⟨_, rfl⟩ },
end

end

variables {f x}

lemma lower_semicontinuous_at_iff [preorder β] :
  lower_semicontinuous_at f x ↔ tendsto f (𝓝 x) (⨅ y < f x, 𝓟 (Ioi y)) :=
by simp_rw [lower_semicontinuous_at, tendsto, le_infi₂_iff, le_principal_iff]; refl

variables [linear_order β] [topological_space β]

lemma lower_semicontinuous_at_iff' [order_topology β] :
  lower_semicontinuous_at f x ↔ filter.tendsto f (𝓝 x) (𝓝ˢ (Ici $ f x)) :=
by rw [lower_semicontinuous_at_iff, nhds_set_Ici]

lemma lower_semicontinuous_at_iff'' (ht : lower_semicontinuous_topology β) :
  lower_semicontinuous_at f x ↔ continuous_at f x :=
begin
  rw [lower_semicontinuous_at, continuous_at_def], split; intro h,
  { simp_rw (is_topological_basis_Ioi ht).mem_nhds_iff,
    rintro s ⟨t, (rfl : _ = _)|⟨a, rfl⟩, hxt, hts⟩,
    { rw [univ_subset_iff.1 hts, preimage_univ], exact univ_mem },
    { exact mem_of_superset (h a hxt) (preimage_mono hts) } },
  { exact λ y hy, h (Ioi y) ((is_topological_basis_Ioi ht).mem_nhds (or.inr ⟨y, rfl⟩) hy) },
end

lemma lower_semicontinuous_iff (ht : lower_semicontinuous_topology β) :
  lower_semicontinuous f ↔ continuous f :=
by simp_rw [lower_semicontinuous, continuous_iff_continuous_at, lower_semicontinuous_at_iff'' ht]