Prop equal and def equal

Stream: new members

[tsuki hao]

import Mathlib.Tactic
import Mathlib.Analysis.Convex.Function
import Mathlib.Data.Real.EReal
import Mathlib.Topology.Basic
import Mathlib.Topology.Sequences
import Mathlib.Order.Filter.Basic
import Mathlib.Order.LiminfLimsup
import Mathlib.Data.Set.Basic
import Mathlib.Logic.Basic
import Mathlib.Order.Basic
import Mathlib.Topology.Sets.Closeds
import Mathlib.Topology.Bases
import Mathlib.Init.Set
import Mathlib.Data.Set.Basic

open EReal Function Topology Filter Set TopologicalSpace


variable {𝕜 E α β ι : Type _}

variable [OrderedSemiring 𝕜]

variable [AddCommMonoid E]

variable (𝕜) (s : Set E) (f : E → EReal)[SMul 𝕜 E]

def properfun : Prop :=
  (∃ x ∈ s, f x < ⊤) ∧ (∀ x ∈ s, f x > ⊥)

def dom : Set E :=
  {x | f x < ⊤} ∩ s

def sublevel (r : EReal) : Set E :=
  { x ∈ s | f x ≤ r }

def uplevel (r : EReal) : Set E :=
  { x ∈ s | f x > r }

def epigraph : Set <| E × EReal :=
  {p : E × EReal | p.1 ∈ s ∧ f p.1 ≤ p.2}
-- {p : E × β | p.1 ∈ s ∧ f p.1 ≤ p.2}

variable [TopologicalSpace 𝕜] [PseudoMetricSpace E] [TopologicalSpace EReal]

variable [SequentialSpace E] [SequentialSpace EReal] [SequentialSpace <| E × EReal]

variable [OrderTopology EReal]

variable [FirstCountableTopology E] [FirstCountableTopology EReal]


def closedfunc : Prop :=
  IsClosed <| epigraph s f

def lo_semicontinuous : Prop :=
  ∀ x ∈ s, f x ≤ (liminf f <| 𝓝[s] x)

section IsClosed

variable (s : Closeds E) (f : E → EReal) [SMul 𝕜 E] [SMul 𝕜 EReal]


theorem aux12 (hf : ∀ (r : EReal), IsClosed <| sublevel s f r) : lo_semicontinuous s f := by
  by_contra h
  unfold lo_semicontinuous at h
  push_neg at h
  rcases h with ⟨x, ⟨_, hx⟩⟩
  rcases exists_between hx with ⟨t, ⟨ltt, tlt⟩⟩
  have : x ∈ sublevel s f t := by
    apply (isClosed_iff_frequently.mp (hf t) x)
    have h1 : ∃ᶠ (y : E) in 𝓝[s] x, f y < t := frequently_lt_of_liminf_lt (by isBoundedDefault) ltt
    have h1' : ∃ᶠ (y : E) in 𝓝[s] x, f y ≤ t := by
      apply frequently_iff.mpr
      intro _ hu
      rcases ((frequently_iff.mp h1) hu) with ⟨x, xu, fx⟩
      exact Exists.intro x { left := xu, right := LT.lt.le fx }
    have : ∃ᶠ (y : E) in 𝓝 x, f y ≤ t ∧ y ∈ s := frequently_nhdsWithin_iff.mp h1'
    apply frequently_iff.mpr
    intro _ hu
    rcases ((frequently_iff.mp this) hu) with ⟨x, xu, fx, xs⟩
    exact Exists.intro x { left := xu, right := { left := xs, right := fx } }
  apply not_le_of_gt tlt (mem_setOf.mp this).2

theorem aux23 (hf : lo_semicontinuous s f) : closedfunc s f := by
  apply IsSeqClosed.isClosed
  intro f' ⟨x', y'⟩ hxy cxy
  rw [Prod.tendsto_iff] at cxy
  let x : ℕ -> E := fun (n : ℕ) => (f' n).1
  have hx : ∀ (n : ℕ), x n ∈ ↑ s := fun n =>  (hxy n).1
  have h1 : x' ∈ s :=
    SetLike.mem_coe.mp ((isSeqClosed_iff_isClosed.mpr <| Closeds.closed s) hx cxy.1)
  have cx : Tendsto x atTop (𝓝[s] x') :=
    tendsto_nhdsWithin_iff.mpr ⟨cxy.1, eventually_of_forall hx⟩
  let y : ℕ -> EReal := fun (n : ℕ) => (f' n).2
  have xley : ∀ (n : ℕ), (f ∘ x) n ≤ y n :=
    fun n => Trans.trans (Trans.trans (Eq.refl ((f ∘ x) n)) (hxy n).2) (Eq.refl (f' n).2)
  have h2 : f x' ≤ y' := by
    calc
      f x' ≤ liminf f (𝓝[s] x') := hf x' h1
      _ = sSup {a | ∀ᶠ (n : E) in 𝓝[s] x', a ≤ f n} := by rw[liminf_eq]
      _ ≤ sSup {a | ∀ᶠ (n : ℕ) in atTop, a ≤ (f ∘ x) n} :=
        sSup_le_sSup
        fun _ fa => mem_setOf.mpr ((eventually_iff_seq_eventually.mp <| mem_setOf.mp fa) x cx)
      _ = liminf (f ∘ x) atTop := by rw[← liminf_eq]
      _ ≤ liminf y atTop := liminf_le_liminf (eventually_of_forall xley)
      _ = y' := (cxy.2).liminf_eq
  exact ⟨h1, h2⟩

theorem aux31 (hf : closedfunc s f) : ∀ (r : EReal), IsClosed <| sublevel s f r := by
  intro r
  rw [← isSeqClosed_iff_isClosed]
  intro x x' xns cx
  exact IsClosed.isSeqClosed hf (fun n => xns n) (Tendsto.prod_mk_nhds cx tendsto_const_nhds)

theorem aux31' (s : Set E) (f : E → EReal) (hf : closedfunc s f) : ∀ (r : EReal), IsClosed <| sublevel s f r := by
  intro r
  rw [← isSeqClosed_iff_isClosed]
  intro x x' xns cx
  exact IsClosed.isSeqClosed hf (fun n => xns n) (Tendsto.prod_mk_nhds cx tendsto_const_nhds)

theorem eq12 :  (∀ (r : EReal), IsClosed <| sublevel s f r) ↔ lo_semicontinuous s f :=
  ⟨fun a => aux12 s f a, fun a => aux31 s f (aux23 s f a)⟩

theorem eq23 : lo_semicontinuous s f ↔ closedfunc s f :=
  ⟨fun a => aux23 s f a, fun a => aux12 s f (aux31 s f a)⟩

theorem eq31 : closedfunc s f ↔ (∀ (r : EReal), IsClosed <| sublevel s f r):=
  ⟨fun a => aux31 s f a , fun a => aux23 s f (aux12 s f a)⟩

end IsClosed


theorem closed_of_continuous (hs : IsClosed s) (hf : Continuous f) : closedfunc s f := by
  apply IsSeqClosed.isClosed
  intro xt prod h cxt
  rcases (Prod.tendsto_iff xt prod).mp cxt with ⟨cx, ct⟩
  have cfx : Tendsto f (𝓝 prod.1) (𝓝 (f prod.1)) := Continuous.continuousAt hf
  constructor
  · exact (IsClosed.isSeqClosed hs) (fun n => (h n).1) cx
  · exact le_of_tendsto_of_tendsto' (Tendsto.comp cfx cx) ct (fun n => (h n).2)


#check @le_of_tendsto_of_tendsto'


theorem aux (hf :  ∀ (r : EReal), IsClosed <| sublevel s f r) : closedfunc s f := by
  sorry

theorem sup_closed2 (f1 f2: E → EReal){hf1 : closedfunc s f1} {hf2 : closedfunc s f2} : closedfunc s (sSup {f1, f2}) := by
  have h : ∀ (r : EReal), IsClosed <| sublevel s (sSup {f1, f2}) r := by
    have h1 : ∀ (r : EReal),  IsClosed <| sublevel s f1 r := by
      exact fun r => aux31' s f1 hf1 r
    have h2 : ∀ (r : EReal),  IsClosed <| sublevel s f2 r := by
      exact fun r => aux31' s f2 hf2 r
    have h3 : ∀ (r : EReal), sublevel s (sSup {f1, f2}) r = {x ∈ s | sSup {f1, f2} x ≤ r }:= by
      exact fun r => rfl
    have h4 : ∀ (r : EReal), {x ∈ s | sSup {f1, f2} x ≤ r } = {x ∈ s | f1 x ≤ r} ∩ {x ∈ s | f2 x ≤ r} := by
      intro r
      have l1 : ∀ x ∈ {x ∈ s | sSup {f1, f2} x ≤ r }, x ∈ {x | sSup {f1, f2} x ≤ r} := by
        exact fun x a => mem_of_mem_inter_right a
      have c1 : ∀ x ∈ {x ∈ s | sSup {f1, f2} x ≤ r }, sSup {f1, f2} x ≤ r := by
        exact fun x a => l1 x a
      have c2 : ∀ x ∈ {x ∈ s | sSup {f1, f2} x ≤ r }, x ∈ {x ∈ s | f1 x ≤ r} ∩ {x ∈ s | f2 x ≤ r}:= by
        have m1 : ∀ x ∈ s, f1 x ≤ r ∧ f2 x ≤ r → x ∈ {x ∈ s | f1 x ≤ r} ∩ {x ∈ s | f2 x ≤ r} := by
          intro x a1 a2
          rcases a2 with ⟨a3, a4⟩
          constructor
          · exact mem_sep a1 a3
          · exact mem_sep a1 a4
      have c3 : ∀ x ∈ {x ∈ s | f1 x ≤ r} ∩ {x ∈ s | f2 x ≤ r}, x ∈ {x ∈ s | sSup {f1, f2} x ≤ r } := by
        sorry
      exact Subset.antisymm c2 c3

    have h5 : ∀ (r : EReal), sublevel s (sSup {f1, f2}) r = {x ∈ s | f1 x ≤ r} ∩ {x ∈ s | f2 x ≤ r} := by
      exact fun r => h4 r
    have h6 : ∀ (r : EReal), IsClosed <| {x ∈ s | f1 x ≤ r} ∩ {x ∈ s | f2 x ≤ r} := by
      exact fun r => IsClosed.inter (h1 r) (h2 r)
    have h7 : ∀ (r : EReal), IsClosed <| sublevel s (sSup {f1, f2}) r := by
      sorry
    exact fun r => h7 r
  exact aux s (sSup {f1, f2}) h

Does anyone know how to write the last sorry? It should be launched directly with h5 and h6, but h5 is Prop Equal not Def Equal, maybe it cannot be directly replaced for this reason? Does anyone know what to do?

[Kevin Buzzard]

    have h7 : ∀ (r : EReal), IsClosed <| sublevel s (sSup {f1, f2}) r := by
      convert h6
      apply h5

By the way, you don't need all those imports:

import Mathlib.Tactic
import Mathlib.Data.Real.EReal
import Mathlib.Topology.Sets.Closeds

will do.

[Kevin Buzzard]

And also, stuff like [TopologicalSpace EReal] is I suspect not correct: this means "put an arbitrary topology on EReal", not "put the obvious topology on EReal". I might be wrong about this though, I don't know much about EReal (I did write the definition, but I didn't think at all about topology at the time)

[Kevin Buzzard]

Yeah you should be importing Mathlib.Topology.Instances.EReal and you should delete all variables putting instances on EReal; you can put structure on abstract types using variables (eg variable [AddCommMonoid E] is fine) but you can't put structure on a concrete type like EReal in this way (it will overwrite the correct structure if you do)

[Kevin Buzzard]

Similarly you shouldn't have two SMul \k E variables -- this will put two different actions of \k on E.