theorem iSup_iSup_eq_iSup {α : Type u_1} {ι : Type u_2} [CompleteLattice α] [SemilatticeSup ι] (f : ι → ι → α) (hf₁ : Monotone f) (hf₂ : ∀ (i : ι), Monotone (f i)) : ⨆ (i : ι), ⨆ (j : ι), f i j = ⨆ (i : ι), f i i

inductive Optimization : Type

• Angelic : Optimization
• Demonic : Optimization

def Optimization.Notation.term𝒜 : Lean.ParserDescr

Equations

• Optimization.Notation.term𝒜 = Lean.ParserDescr.node `Optimization.Notation.term𝒜 1024 (Lean.ParserDescr.symbol "𝒜")

def Optimization.Notation.term𝒟 : Lean.ParserDescr

Equations

• Optimization.Notation.term𝒟 = Lean.ParserDescr.node `Optimization.Notation.term𝒟 1024 (Lean.ParserDescr.symbol "𝒟")

@[reducible, inline]

abbrev Optimization.dual : Optimization → Optimization

Equations

• Optimization.Angelic.dual = Optimization.Demonic
• Optimization.Demonic.dual = Optimization.Angelic

@[simp]

theorem Optimization.𝓐_dual : Angelic.dual = Demonic

@[simp]

theorem Optimization.𝒟_dual : Demonic.dual = Angelic

def Optimization.opt {α : Type u_2} (O : Optimization) [Lattice α] (a b : α) : α

Equations

• Optimization.Angelic.opt a b = a ⊔ b
• Optimization.Demonic.opt a b = a ⊓ b

@[simp]

theorem Optimization.opt_apply {α : Type u_2} (O : Optimization) [Lattice α] {γ : Type u_3} {x : γ} (f g : γ → α) : O.opt f g x = O.opt (f x) (g x)

@[simp]

theorem Optimization.opt_OrderHom_apply {α : Type u_2} (O : Optimization) [Lattice α] {γ : Type u_3} {x : γ} [Preorder γ] (f g : γ →o α) : (O.opt f g) x = O.opt (f x) (g x)

theorem Optimization.opt_le {α : Type u_2} (O : Optimization) [Lattice α] {a b c d : α} (hac : a ≤ c) (hbd : b ≤ d) : O.opt a b ≤ O.opt c d

@[simp]

theorem Optimization.𝒜_opt {α : Type u_2} [Lattice α] {a b : α} : Angelic.opt a b = a ⊔ b

@[simp]

theorem Optimization.𝒟_opt {α : Type u_2} [Lattice α] {a b : α} : Demonic.opt a b = a ⊓ b

theorem Optimization.opt_ωScottContinuous {α : Type u_3} {β : Type u_4} [Order.Frame α] [Order.Frame β] (O : Optimization) {f g : α →o β} (hf : OmegaCompletePartialOrder.ωScottContinuous ⇑f) (hg : OmegaCompletePartialOrder.ωScottContinuous ⇑g) : OmegaCompletePartialOrder.ωScottContinuous (O.opt ⇑f ⇑g)

def Optimization.iOpt {ι : Type u_1} {α : Type u_2} (O : Optimization) [CompleteLattice α] : (ι → α) →o α

Equations

• Optimization.Angelic.iOpt = { toFun := fun (f : ι → α) => ⨆ (α : ι), f α, monotone' := ⋯ }
• Optimization.Demonic.iOpt = { toFun := fun (f : ι → α) => ⨅ (α : ι), f α, monotone' := ⋯ }

def Optimization.sOpt {ι : Type u_1} {α : Type u_2} (O : Optimization) [CompleteLattice α] (S : Set ι) : (ι → α) →o α

Equations

• Optimization.Angelic.sOpt S = { toFun := fun (f : ι → α) => ⨆ α_1 ∈ S, f α_1, monotone' := ⋯ }
• Optimization.Demonic.sOpt S = { toFun := fun (f : ι → α) => ⨅ α_1 ∈ S, f α_1, monotone' := ⋯ }

theorem Optimization.sOpt_eq_iOpt {ι : Type u_1} {α : Type u_2} (O : Optimization) [CompleteLattice α] (S : Set ι) (f : ι → α) : (O.sOpt S) f = O.iOpt fun (a : ↑S) => f ↑a

@[simp]

theorem Optimization.sOpt_singleton {ι : Type u_1} {α : Type u_2} (O : Optimization) [CompleteLattice α] {i : ι} {f : ι → α} : (O.sOpt {i}) f = f i

@[simp]

theorem Optimization.sOpt_pair {ι : Type u_1} {α : Type u_2} (O : Optimization) [CompleteLattice α] {a b : ι} {f : ι → α} : (O.sOpt {a, b}) f = O.opt (f a) (f b)

@[simp]

theorem Optimization.𝒜_iOpt {ι : Type u_1} {α : Type u_2} [CompleteLattice α] {f : ι → α} : Angelic.iOpt f = iSup f

@[simp]

theorem Optimization.𝒟_iOpt {ι : Type u_1} {α : Type u_2} [CompleteLattice α] {f : ι → α} : Demonic.iOpt f = iInf f

@[simp]

theorem Optimization.𝒜_sOpt {ι : Type u_1} {α : Type u_2} [CompleteLattice α] {S : Set ι} {f : ι → α} : (Angelic.sOpt S) f = ⨆ α_1 ∈ S, f α_1

@[simp]

theorem Optimization.𝒟_sOpt {ι : Type u_1} {α : Type u_2} [CompleteLattice α] {S : Set ι} {f : ι → α} : (Demonic.sOpt S) f = ⨅ α_1 ∈ S, f α_1

@[simp]

theorem Optimization.iOpt_apply {ι : Type u_1} {α : Type u_2} (O : Optimization) [CompleteLattice α] {β : Type u_3} {s : β} {f : ι → β → α} : O.iOpt f s = O.iOpt fun (x : ι) => f x s

@[simp]

theorem Optimization.iOpt_const {ι : Type u_1} {α : Type u_2} (O : Optimization) [CompleteLattice α] [Nonempty ι] {x : α} : (O.iOpt fun (x_1 : ι) => x) = x

theorem Optimization.ENNReal_add_iOpt {ι : Type u_1} (O : Optimization) {a : ENNReal} [Nonempty ι] {f : ι → ENNReal} : (O.iOpt fun (i : ι) => a + f i) = a + O.iOpt f

theorem Optimization.ENNReal_iOpt_add {ι : Type u_1} (O : Optimization) {a : ENNReal} [Nonempty ι] {f : ι → ENNReal} : (O.iOpt fun (i : ι) => f i + a) = O.iOpt f + a

theorem Optimization.ENNReal_mul_iOpt {ι : Type u_1} (O : Optimization) [Nonempty ι] {f : ι → ENNReal} {a : ENNReal} (ha : a ≠ ⊤) : (O.iOpt fun (i : ι) => a * f i) = a * O.iOpt f

theorem Optimization.ENNReal_iOpt_mul {ι : Type u_1} (O : Optimization) [Nonempty ι] {f : ι → ENNReal} {a : ENNReal} (ha : a ≠ ⊤) : (O.iOpt fun (i : ι) => f i * a) = O.iOpt f * a