theorem
IsCompact.exists_isMinOn_lowerSemicontinuousOn
{α : Type u_1}
{β : Type u_2}
[LinearOrder α]
[TopologicalSpace α]
[TopologicalSpace β]
[ClosedIicTopology α]
{s : Set β}
(hs : IsCompact s)
(ne_s : s.Nonempty)
{f : β → α}
(hf : LowerSemicontinuousOn f s)
:
∃ x ∈ s, IsMinOn f s x
theorem
LinearMap.quasilinearOn
{E : Type u_1}
{β : Type u_2}
{𝕜 : Type u_3}
[Semiring 𝕜]
[PartialOrder 𝕜]
[AddCommMonoid E]
[Module 𝕜 E]
[PartialOrder β]
[AddCommMonoid β]
[IsOrderedAddMonoid β]
[Module 𝕜 β]
[PosSMulMono 𝕜 β]
(f : E →ₗ[𝕜] β)
{s : Set E}
(hs : Convex 𝕜 s)
:
QuasilinearOn 𝕜 s ⇑f
theorem
LinearMap.quasiconvexOn
{E : Type u_1}
{β : Type u_2}
{𝕜 : Type u_3}
[Semiring 𝕜]
[PartialOrder 𝕜]
[AddCommMonoid E]
[Module 𝕜 E]
[PartialOrder β]
[AddCommMonoid β]
[IsOrderedAddMonoid β]
[Module 𝕜 β]
[PosSMulMono 𝕜 β]
(f : E →ₗ[𝕜] β)
{s : Set E}
(hs : Convex 𝕜 s)
:
QuasiconvexOn 𝕜 s ⇑f
theorem
LinearMap.quasiconcaveOn
{E : Type u_1}
{β : Type u_2}
{𝕜 : Type u_3}
[Semiring 𝕜]
[PartialOrder 𝕜]
[AddCommMonoid E]
[Module 𝕜 E]
[PartialOrder β]
[AddCommMonoid β]
[IsOrderedAddMonoid β]
[Module 𝕜 β]
[PosSMulMono 𝕜 β]
(f : E →ₗ[𝕜] β)
{s : Set E}
(hs : Convex 𝕜 s)
:
QuasiconcaveOn 𝕜 s ⇑f
theorem
continuous_stupid
{M : Type u_1}
[inst : NormedAddCommGroup M]
[inst_1 : Module ℝ M]
[inst_3 : ContinuousSMul ℝ M]
{N : Type u_2}
[inst_4 : NormedAddCommGroup N]
[inst_5 : Module ℝ N]
[FiniteDimensional ℝ M]
(f : N →L[ℝ] M →L[ℝ] ℝ)
:
Continuous fun (x : N × M) => (f x.1) x.2
theorem
minimax
{M : Type u_1}
[NormedAddCommGroup M]
[Module ℝ M]
[ContinuousAdd M]
[ContinuousSMul ℝ M]
[FiniteDimensional ℝ M]
{N : Type u_2}
[NormedAddCommGroup N]
[Module ℝ N]
[ContinuousAdd N]
[ContinuousSMul ℝ N]
(f : N →L[ℝ] M →L[ℝ] ℝ)
(S : Set M)
(T : Set N)
(hS₁ : IsCompact S)
(hT₁ : IsCompact T)
(hS₂ : Convex ℝ S)
(hT₂ : Convex ℝ T)
(hS₃ : S.Nonempty)
(hT₃ : T.Nonempty)
:
The minimax theorem, at the level of generality we need. For convex, compact, nonempty sets S
and Tin a real topological vector space M, and a bilinear function f on M, we can exchange
the order of minimizing and maximizing.
theorem
LinearMap.BilinForm.minimax
{M : Type u_1}
[NormedAddCommGroup M]
[Module ℝ M]
[ContinuousAdd M]
[ContinuousSMul ℝ M]
[FiniteDimensional ℝ M]
(f : LinearMap.BilinForm ℝ M)
(S T : Set M)
(hS₁ : IsCompact S)
(hT₁ : IsCompact T)
(hS₂ : Convex ℝ S)
(hT₂ : Convex ℝ T)
(hS₃ : S.Nonempty)
(hT₃ : T.Nonempty)
:
Von-Neumann's Minimax Theorem, specialized to bilinear forms.
theorem
LinearMap.BilinForm.minimax'
{M : Type u_1}
[NormedAddCommGroup M]
[Module ℝ M]
[ContinuousAdd M]
[ContinuousSMul ℝ M]
[FiniteDimensional ℝ M]
(f : LinearMap.BilinForm ℝ M)
(S T : Set M)
(hS₁ : IsCompact S)
(hT₁ : IsCompact T)
(hS₂ : Convex ℝ S)
(hT₂ : Convex ℝ T)
(hS₃ : S.Nonempty)
(hT₃ : T.Nonempty)
:
Convenience form of LinearMap.BilinForm.minimax with the order inf/sup arguments supplied to f flipped.