WeightedNetKAT.Instances.Arctic

source

def Arctic :

Type

Equations

Arctic = WithBot ℕ∞

Instances For

source

@[implicit_reducible]

instance instDecidableEqArctic :

DecidableEq Arctic

Equations

instDecidableEqArctic = instDecidableEqArctic._aux_1

source

def Arctic.arc (n : WithBot ℕ∞) :

Arctic

Equations

Arctic.arc n = n

Instances For

source

def Arctic.unarc (a : Arctic) :

WithBot ℕ∞

Equations

a.unarc = a

Instances For

source

@[simp]

theorem Arctic.arc_unarc {a : Arctic} :

arc a.unarc = a

source

@[simp]

theorem Arctic.unarc_arc {a : WithBot ℕ∞} :

(arc a).unarc = a

source

theorem Arctic.eq_of_unarc {a b : Arctic} (h : a.unarc = b.unarc) :

a = b

source

theorem Arctic.eq_of_arc {a b : WithBot ℕ∞} (h : arc a = arc b) :

a = b

source

def Arctic.max' :

Arctic → Arctic → Arctic

Equations

Arctic.max' (some a) (some b) = if a ≤ b then Arctic.arc ↑b else Arctic.arc ↑a
x✝.max' (some b) = Arctic.arc ↑b
Arctic.max' (some b) x✝ = Arctic.arc ↑b
Arctic.max' none none = Arctic.arc ⊥

Instances For

source

def Arctic.min' :

Arctic → Arctic → Arctic

Equations

Arctic.min' (some a) (some b) = if a ≤ b then Arctic.arc ↑a else Arctic.arc ↑b
Arctic.min' none x✝ = Arctic.arc ⊥
x✝.min' none = Arctic.arc ⊥

Instances For

source

@[simp]

theorem Arctic.max'_eq_unarc_sup {a b : Arctic} :

a.max' b = max a.unarc b.unarc

source

@[simp]

theorem Arctic.min'_eq_unarc_inf {a b : Arctic} :

a.min' b = min a.unarc b.unarc

source

@[implicit_reducible]

instance Arctic.instPartialOrder :

PartialOrder Arctic

Equations

One or more equations did not get rendered due to their size.

source

@[simp]

theorem Arctic.le_def {x y : Arctic} :

x ≤ y ↔ x.unarc ≤ y.unarc

source

@[simp]

theorem Arctic.arctic_lt_iff {x y : Arctic} :

x < y ↔ x.unarc ≤ y.unarc ∧ ¬y.unarc ≤ x.unarc

source

theorem Arctic.arc_le {x y : WithBot ℕ∞} :

arc x ≤ arc y ↔ x ≤ y

source

theorem Arctic.unarc_le {x y : Arctic} :

x.unarc ≤ y.unarc ↔ x ≤ y

source

theorem Arctic.arc_lt {x y : WithBot ℕ∞} :

arc x < arc y ↔ x < y

source

theorem Arctic.unarc_lt {x y : Arctic} :

x.unarc < y.unarc ↔ x < y

source

theorem Arctic.unarc_le_of {x y : Arctic} (h : x ≤ y) :

x.unarc ≤ y.unarc

source

@[implicit_reducible]

instance Arctic.instTop :

Top Arctic

Equations

Arctic.instTop = { top := Arctic.instTop._aux_1 }

source

@[implicit_reducible]

instance Arctic.instBot :

Bot Arctic

Equations

Arctic.instBot = { bot := Arctic.instBot._aux_1 }

source

@[implicit_reducible]

instance Arctic.instOrderTop :

OrderTop Arctic

Equations

Arctic.instOrderTop = { toTop := Arctic.instTop, le_top := Arctic.instOrderTop._proof_1 }

source

@[implicit_reducible]

instance Arctic.instOrderBot :

OrderBot Arctic

Equations

Arctic.instOrderBot = { toBot := Arctic.instBot, bot_le := Arctic.instOrderBot._proof_1 }

source

@[implicit_reducible]

instance Arctic.instSemilatticeSup :

SemilatticeSup Arctic

Equations

Arctic.instSemilatticeSup = { toPartialOrder := Arctic.instPartialOrder, sup := Arctic.max', le_sup_left := ⋯, le_sup_right := ⋯, sup_le := Arctic.instSemilatticeSup._proof_3 }

source

@[implicit_reducible]

instance Arctic.instSemilatticeInf :

SemilatticeInf Arctic

Equations

Arctic.instSemilatticeInf = { toPartialOrder := Arctic.instPartialOrder, inf := Arctic.min', inf_le_left := ⋯, inf_le_right := ⋯, le_inf := Arctic.instSemilatticeInf._proof_3 }

source

@[implicit_reducible]

instance Arctic.instLattice :

Lattice Arctic

Equations

Arctic.instLattice = { toSemilatticeSup := Arctic.instSemilatticeSup, inf := SemilatticeInf.inf, inf_le_left := ⋯, inf_le_right := ⋯, le_inf := ⋯ }

source

@[implicit_reducible]

noncomputable instance Arctic.instCompleteLattice :

CompleteLattice Arctic

Equations

One or more equations did not get rendered due to their size.

source

@[implicit_reducible]

instance Arctic.instZero :

Zero Arctic

Equations

Arctic.instZero = { zero := Arctic.arc ⊥ }

source

@[implicit_reducible]

instance Arctic.instOne :

One Arctic

Equations

Arctic.instOne = { one := Arctic.arc 0 }

source

@[implicit_reducible]

instance Arctic.instAdd :

Add Arctic

Equations

Arctic.instAdd = { add := fun (a b : Arctic) => max a b }

source

@[implicit_reducible]

instance Arctic.instMul :

Mul Arctic

Equations

Arctic.instMul = { mul := fun (a b : Arctic) => Arctic.arc (a.unarc + b.unarc) }

source

@[simp]

theorem Arctic.zero_eq_arc_bot :

0 = arc ⊥

source

@[simp]

theorem Arctic.one_eq_arc_0 :

1 = arc 0

source

@[simp]

theorem Arctic.add_eq_sup {a b : Arctic} :

a + b = max a b

source

@[simp]

theorem Arctic.mul_eq_add {a b : Arctic} :

a * b = arc (a.unarc + b.unarc)

source

@[simp]

theorem Arctic.unarc_sup {a b : Arctic} :

(max a b).unarc = max a.unarc b.unarc

source

@[simp]

theorem Arctic.unarc_inf {a b : Arctic} :

(min a b).unarc = min a.unarc b.unarc

source

@[simp]

theorem Arctic.arc_sup {a b : WithBot ℕ∞} :

arc (max a b) = max (arc a) (arc b)

source

@[simp]

theorem Arctic.arc_inf {a b : WithBot ℕ∞} :

arc (min a b) = min (arc a) (arc b)

source

@[simp]

theorem Arctic.unarc_bot :

⊥.unarc = ⊥

source

@[simp]

theorem Arctic.unarc_top :

⊤.unarc = ⊤

source

@[implicit_reducible]

instance Arctic.instSemiring :

Semiring Arctic

Equations

One or more equations did not get rendered due to their size.

source

instance Arctic.instIsPositiveOrderedAddMonoid :

IsPositiveOrderedAddMonoid Arctic

source

instance Arctic.instMulLeftMono :

MulLeftMono Arctic

source

instance Arctic.instMulRightMono :

MulRightMono Arctic

source

instance Arctic.instAddLeftMonoWithBotENat :

AddLeftMono (WithBot ℕ∞)

source

instance Arctic.instAddRightMonoWithBotENat :

AddRightMono (WithBot ℕ∞)

source

@[simp]

theorem Arctic.le_iff_le' :

LE.le = LE.le

source

@[simp]

theorem Arctic.lt_iff_lt' :

LT.lt = LT.lt

source

@[simp]

theorem Arctic.iSup_eq_iSup' {α : Sort u_1} :

iSup = iSup

source

@[simp]

theorem Arctic.unarc_iSup {α : Sort u_1} {f : α → Arctic} :

(⨆ (i : α), f i).unarc = ⨆ (i : α), (f i).unarc

source

@[simp]

theorem Arctic.arc_iSup {α : Sort u_1} {f : α → WithBot ℕ∞} :

arc (⨆ (i : α), f i) = ⨆ (i : α), arc (f i)

source

instance Arctic.instOmegaContinuousNonUnitalSemiring :

OmegaContinuousNonUnitalSemiring Arctic

source

@[implicit_reducible]

instance Arctic.instKStar :

KStar Arctic

Equations

Arctic.instKStar = { kstar := fun (x : Arctic) => if x ≤ Arctic.arc 0 then Arctic.arc 0 else Arctic.arc ⊤ }

source

@[simp]

theorem Arctic.le_zero_arc {x : Arctic} :

x ≤ arc 0 ↔ x = arc ⊥ ∨ x = arc 0

source

@[implicit_reducible]

noncomputable instance Arctic.instCompleteLinearOrder :

CompleteLinearOrder Arctic

Equations

One or more equations did not get rendered due to their size.

source

@[simp]

theorem Arctic.finset_sum_eq_iSup {ι : Type u_1} [DecidableEq ι] {S : Finset ι} (f : ι → Arctic) :

∑ i ∈ S, f i = ⨆ i ∈ S, f i

source

@[simp]

theorem Arctic.pow_eq_mul {n : ℕ} {a : Arctic} :

a ^ n = arc (↑n * a.unarc)

source

theorem Arctic.add_top {x : WithBot ℕ∞} (hx : x ≠ ⊥) :

⊤ + x = ⊤

source

theorem Arctic.top_add {x : WithBot ℕ∞} (hx : x ≠ ⊥) :

x + ⊤ = ⊤

source

theorem Arctic.help_me {a b : Arctic} (ha₁ : a ≠ ⊥) (ha₂ : a ≠ ⊤) (hb₁ : b ≠ ⊥) (hb₂ : b ≠ ⊤) (h : Option.get (Option.get a.unarc ⋯) ⋯ < Option.get (Option.get b.unarc ⋯) ⋯) :

a < b

source

@[simp]

theorem Arctic.unarc_get {x : Arctic} (h : Option.isSome x.unarc = true) :

Option.get x.unarc h = Option.get x h

source

instance Arctic.instMulLeftMonoWithBotENat :

MulLeftMono (WithBot ℕ∞)

source

instance Arctic.instLawfulKStar :

LawfulKStar Arctic

source

@[implicit_reducible]

instance Arctic.instRepr :

Repr Arctic

Equations

One or more equations did not get rendered due to their size.