theorem
ciSup_ciInf_le_ciInf_ciSup
{ι : Type u_1}
{α : Type u_2}
[ConditionallyCompleteLattice α]
{ι' : Type u_3}
[Nonempty ι]
(f : ι → ι' → α)
(Ha : ∀ (j : ι'), BddAbove (Set.range fun (x : ι) => f x j))
(Hb : ∀ (i : ι), BddBelow (Set.range (f i)))
:
The max-min theorem. A version of iSup_iInf_le_iInf_iSup for conditionally complete lattices.
theorem
QuasiconvexOn.subset
{𝕜 : Type u_1}
{E : Type u_2}
{β : Type u_3}
[Semiring 𝕜]
[PartialOrder 𝕜]
[AddCommMonoid E]
[LE β]
[SMul 𝕜 E]
{s : Set E}
{f : E → β}
(h : QuasiconvexOn 𝕜 s f)
{t : Set E}
(hts : t ⊆ s)
(ht : Convex 𝕜 t)
:
QuasiconvexOn 𝕜 t f
theorem
QuasiconvexOn.mem_segment_le_max
{𝕜 : Type u_1}
{E : Type u_2}
{β : Type u_3}
[Semiring 𝕜]
[PartialOrder 𝕜]
[AddCommMonoid E]
[SemilatticeSup β]
[SMul 𝕜 E]
{s : Set E}
{f : E → β}
(h : QuasiconvexOn 𝕜 s f)
{x y z : E}
(hx : x ∈ s)
(hy : y ∈ s)
(hz : z ∈ segment 𝕜 x y)
:
theorem
QuasiconcaveOn.min_le_mem_segment
{𝕜 : Type u_1}
{E : Type u_2}
{β : Type u_3}
[Semiring 𝕜]
[PartialOrder 𝕜]
[AddCommMonoid E]
[SemilatticeInf β]
[SMul 𝕜 E]
{s : Set E}
{f : E → β}
(h : QuasiconcaveOn 𝕜 s f)
{x y z : E}
(hx : x ∈ s)
(hy : y ∈ s)
(hz : z ∈ segment 𝕜 x y)
:
theorem
LowerSemicontinuousOn.bddBelow
{α : Type u_1}
[TopologicalSpace α]
{S : Set α}
{g : α → ℝ}
(hg : LowerSemicontinuousOn g S)
(hS : IsCompact S)
:
theorem
LowerSemicontinuousOn.max
{α : Type u_1}
[TopologicalSpace α]
{S : Set α}
{f g : α → ℝ}
(hf : LowerSemicontinuousOn f S)
(hg : LowerSemicontinuousOn g S)
:
LowerSemicontinuousOn (fun (x : α) => Max.max (f x) (g x)) S
theorem
lowerSemicontinuousOn_iff_isClosed_preimage
{α : Type u_1}
[TopologicalSpace α]
{s : Set α}
{γ : Type u_3}
[LinearOrder γ]
{f : α → γ}
[IsClosed s]
:
theorem
segment.isConnected
{E : Type u_1}
[AddCommGroup E]
[Module ℝ E]
[TopologicalSpace E]
[ContinuousAdd E]
[ContinuousSMul ℝ E]
(a b : E)
:
IsConnected (segment ℝ a b)
theorem
BddAbove.range_inf_of_image2
{M : Type u_4}
{N : Type u_5}
{α : Type u_6}
{f : M → N → α}
[ConditionallyCompleteLinearOrder α]
{S : Set M}
{T : Set N}
(h_bddA : BddAbove (Set.image2 f S T))
(h_bddB : BddBelow (Set.image2 f S T))
:
theorem
BddBelow.range_sup_of_image2
{M : Type u_4}
{N : Type u_5}
{α : Type u_6}
{f : M → N → α}
[ConditionallyCompleteLinearOrder α]
{S : Set M}
{T : Set N}
(h_bddA : BddAbove (Set.image2 f S T))
(h_bddB : BddBelow (Set.image2 f S T))
:
theorem
LowerSemicontinuousOn.dite_top
{α : Type u_4}
{β : Type u_5}
[TopologicalSpace α]
[Preorder β]
[OrderTop β]
{s : Set α}
(p : α → Prop)
[DecidablePred p]
{f : (a : α) → p a → β}
(hf : LowerSemicontinuousOn (fun (x : Subtype p) => f ↑x ⋯) {x : Subtype p | ↑x ∈ s})
(h_relatively_closed : ∃ (U : Set α), IsClosed U ∧ s ∩ U = s ∩ setOf p)
:
LowerSemicontinuousOn (fun (x : α) => dite (p x) (f x) fun (x : ¬p x) => ⊤) s
theorem
LowerSemicontinuousOn.comp_continuousOn
{α : Type u_4}
{β : Type u_5}
{γ : Type u_6}
[TopologicalSpace α]
[TopologicalSpace β]
[Preorder γ]
{f : α → β}
{s : Set α}
{g : β → γ}
{t : Set β}
(hg : LowerSemicontinuousOn g t)
(hf : ContinuousOn f s)
(h : Set.MapsTo f s t)
:
LowerSemicontinuousOn (g ∘ f) s
theorem
UpperSemicontinuousOn.comp_continuousOn
{α : Type u_4}
{β : Type u_5}
{γ : Type u_6}
[TopologicalSpace α]
[TopologicalSpace β]
[Preorder γ]
{f : α → β}
{s : Set α}
{g : β → γ}
{t : Set β}
(hg : UpperSemicontinuousOn g t)
(hf : ContinuousOn f s)
(h : Set.MapsTo f s t)
:
UpperSemicontinuousOn (g ∘ f) s
theorem
LowerSemicontinuousOn.ite_top
{α : Type u_4}
{β : Type u_5}
[TopologicalSpace α]
[Preorder β]
[OrderTop β]
{s : Set α}
(p : α → Prop)
[DecidablePred p]
{f : α → β}
(hf : LowerSemicontinuousOn f (s ∩ setOf p))
(h_relatively_closed : ∃ (U : Set α), IsClosed U ∧ s ∩ U = s ∩ setOf p)
:
LowerSemicontinuousOn (fun (x : α) => if p x then f x else ⊤) s
theorem
LeftOrdContinuous.comp_lowerSemicontinuousOn_strong_assumptions
{α : Type u_4}
{γ : Type u_5}
{δ : Type u_6}
[TopologicalSpace α]
[LinearOrder γ]
[LinearOrder δ]
[TopologicalSpace δ]
[OrderTopology δ]
[TopologicalSpace γ]
[OrderTopology γ]
[DenselyOrdered γ]
[DenselyOrdered δ]
{s : Set α}
{g : γ → δ}
{f : α → γ}
(hg : LeftOrdContinuous g)
(hf : LowerSemicontinuousOn f s)
(hg2 : Monotone g)
:
LowerSemicontinuousOn (g ∘ f) s
theorem
UpperSemicontinuousOn.frequently_lt_of_tendsto
{α : Type u_4}
{β : Type u_5}
{γ : Type u_6}
[TopologicalSpace β]
[Preorder γ]
{f : β → γ}
{T : Set β}
(hf : UpperSemicontinuousOn f T)
{c : γ}
{zs : α → β}
{z : β}
{l : Filter α}
[l.NeBot]
(hzs : Filter.Tendsto zs l (nhds z))
(hx₂ : f z < c)
(hzI : ∀ (a : α), zs a ∈ T)
(hzT : z ∈ T)
:
Following https://projecteuclid.org/journals/kodai-mathematical-journal/volume-11/issue-1/Elementary-proof-for-Sions-minimax-theorem/10.2996/kmj/1138038812.full, with some corrections. There are two errors in Lemma 2 and the main theorem: an incorrect step that
(∀ x, a < f x) → (a < ⨅ x, f x). This is repaired by taking an extra exists_between to get a < b < ⨅ ..., concluding that
(∀ x, b < f x) → (b ≤ ⨅ x, f x) and so (a < ⨅ x, f x).
theorem
sion_minimax
{M : Type u_4}
[NormedAddCommGroup M]
{N : Type u_5}
{f : M → N → ℝ}
{S : Set M}
{T : Set N}
(hfc₂ : ∀ y ∈ T, LowerSemicontinuousOn (fun (x : M) => f x y) S)
(hS₁ : IsCompact S)
(hS₃ : S.Nonempty)
(hT₃ : T.Nonempty)
[Module ℝ M]
[ContinuousSMul ℝ M]
[AddCommGroup N]
[TopologicalSpace N]
[SequentialSpace N]
[T2Space N]
[ContinuousAdd N]
[Module ℝ N]
[ContinuousSMul ℝ N]
(hfc₁ : ∀ x ∈ S, UpperSemicontinuousOn (f x) T)
(hfq₂ : ∀ y ∈ T, QuasiconvexOn ℝ S fun (x : M) => f x y)
(hfq₁ : ∀ x ∈ S, QuasiconcaveOn ℝ T (f x))
(hT₂ : Convex ℝ T)
(hS₂ : Convex ℝ S)
(h_bddA : BddAbove (Set.image2 f S T))
(h_bddB : BddBelow (Set.image2 f S T))
:
Sion's Minimax theorem. Because of ciSup and ciInf junk values when f isn't
bounded, we need to assume that it's bounded above and below.