## Stream: new members

### Topic: Prop equal and def equal

#### tsuki hao (Sep 01 2023 at 00:27):

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 (๐) (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 (Sep 01 2023 at 07:30):

    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 (Sep 01 2023 at 07:34):

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 (Sep 01 2023 at 08:43):

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 (Sep 01 2023 at 08:46):

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

Last updated: Dec 20 2023 at 11:08 UTC