PGCL.Exp

source

def pGCL.States (ϖ : Type u_2) :

Type u_2

Equations

pGCL.States ϖ = (ϖ → ENNReal)

Instances For

source

instance pGCL.instNonemptyStates {ϖ : Type u_1} :

Nonempty (States ϖ)

source

@[reducible, inline]

abbrev pGCL.Exp (ϖ : Type u_2) :

Type u_2

Equations

pGCL.Exp ϖ = (pGCL.States ϖ → ENNReal)

Instances For

source

@[reducible, inline]

abbrev pGCL.BExpr (ϖ : Type u_2) :

Type u_2

Equations

pGCL.BExpr ϖ = (pGCL.States ϖ → Bool)

Instances For

source

def pGCL.ProbExp (ϖ : Type u_2) :

Type u_2

Equations

pGCL.ProbExp ϖ = { e : pGCL.Exp ϖ // e ≤ 1 }

Instances For

source

def pGCL.States.subst {ϖ : Type u_1} [DecidableEq ϖ] (σ : States ϖ) (x : ϖ) (v : ENNReal) :

States ϖ

Equations

(σ[x ↦ v]) α = if x = α then v else σ α

Instances For

source

def pGCL.«term_[_↦_]» :

Lean.TrailingParserDescr

Equations

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

Instances For

source

def pGCL.Exp.subst {ϖ : Type u_1} [DecidableEq ϖ] (e : Exp ϖ) (x : ϖ) (A : Exp ϖ) :

Exp ϖ

Equations

e.subst x A σ = e (σ[x ↦ A σ])

Instances For

source

@[simp]

theorem pGCL.Exp.subst_lift {ϖ : Type u_1} {x : ϖ} {A : Exp ϖ} {σ : States ϖ} [DecidableEq ϖ] (e : Exp ϖ) :

e.subst x A σ = e (σ[x ↦ A σ])

source

def pGCL.BExpr.not {ϖ : Type u_1} (b : BExpr ϖ) :

BExpr ϖ

Equations

b.not x✝ = !b x✝

Instances For

source

def pGCL.BExpr.probOf {ϖ : Type u_1} (b : BExpr ϖ) :

Exp ϖ

Equations

b.probOf x✝ = if b x✝ = true then 1 else 0

Instances For

source

@[simp]

theorem pGCL.BExpr.true_probOf {ϖ : Type u_1} {b : BExpr ϖ} {σ : States ϖ} (h : b σ = true) :

b.probOf σ = 1

source

@[simp]

theorem pGCL.BExpr.false_probOf {ϖ : Type u_1} {b : BExpr ϖ} {σ : States ϖ} (h : b σ = false) :

b.probOf σ = 0

source

@[simp]

theorem pGCL.BExpr.true_not_probOf {ϖ : Type u_1} {b : BExpr ϖ} {σ : States ϖ} (h : b σ = true) :

b.not.probOf σ = 0

source

@[simp]

theorem pGCL.BExpr.false_not_probOf {ϖ : Type u_1} {b : BExpr ϖ} {σ : States ϖ} (h : b σ = false) :

b.not.probOf σ = 1

source

@[simp]

theorem pGCL.ProbExp.add_one {ϖ : Type u_1} (p : ProbExp ϖ) (σ : States ϖ) :

↑p σ + (1 - ↑p σ) = 1

source

@[simp]

theorem pGCL.ProbExp.le_one {ϖ : Type u_1} (p : ProbExp ϖ) (σ : States ϖ) :

↑p σ ≤ 1

source

@[simp]

theorem pGCL.ProbExp.lt_one_iff {ϖ : Type u_1} (p : ProbExp ϖ) (σ : States ϖ) :

¬↑p σ = 1 ↔ ↑p σ < 1

source

@[simp]

theorem pGCL.ProbExp.sub_one_le_one {ϖ : Type u_1} (p : ProbExp ϖ) (σ : States ϖ) :

1 - ↑p σ ≤ 1

source

@[simp]

theorem pGCL.ProbExp.ne_top {ϖ : Type u_1} (p : ProbExp ϖ) (σ : States ϖ) :

↑p σ ≠ ⊤

source

@[simp]

theorem pGCL.ProbExp.top_ne {ϖ : Type u_1} (p : ProbExp ϖ) (σ : States ϖ) :

⊤ ≠ ↑p σ

source

@[simp]

theorem pGCL.ProbExp.not_zero_off {ϖ : Type u_1} (p : ProbExp ϖ) (σ : States ϖ) :

¬↑p σ = 0 ↔ 0 < ↑p σ

source

@[simp]

theorem pGCL.ProbExp.lt_one_iff' {ϖ : Type u_1} (p : ProbExp ϖ) (σ : States ϖ) :

1 - ↑p σ < 1 ↔ ¬↑p σ = 0

source

@[simp]

theorem pGCL.ProbExp.top_ne_one_sub {ϖ : Type u_1} (p : ProbExp ϖ) (σ : States ϖ) :

¬⊤ = 1 - ↑p σ

source

@[simp]

theorem pGCL.ProbExp.one_le_iff {ϖ : Type u_1} (p : ProbExp ϖ) (σ : States ϖ) :

1 ≤ ↑p σ ↔ ↑p σ = 1

source

@[simp]

theorem pGCL.ProbExp.ite_eq_zero {ϖ : Type u_1} (p : ProbExp ϖ) (σ : States ϖ) {x : ENNReal} :

(if 0 < ↑p σ then ↑p σ * x else 0) = ↑p σ * x

source

@[simp]

theorem pGCL.ProbExp.ite_eq_one {ϖ : Type u_1} (p : ProbExp ϖ) (σ : States ϖ) {x : ENNReal} :

(if ↑p σ < 1 then (1 - ↑p σ) * x else 0) = (1 - ↑p σ) * x

source

@[simp]

theorem pGCL.ProbExp.ite_eq_zero' {ϖ : Type u_1} (p : ProbExp ϖ) (σ : States ϖ) :

(if 0 < ↑p σ then ↑p σ else 0) = ↑p σ

source

@[simp]

theorem pGCL.ProbExp.ite_eq_one' {ϖ : Type u_1} (p : ProbExp ϖ) (σ : States ϖ) :

(if ↑p σ < 1 then 1 - ↑p σ else 0) = 1 - ↑p σ

source

noncomputable def pGCL.ProbExp.pick {ϖ : Type u_1} (p : ProbExp ϖ) (x y : Exp ϖ) :

Exp ϖ

Equations

p.pick x y = ↑p * x + (1 - ↑p) * y

Instances For

source

@[simp]

theorem pGCL.ProbExp.pick_le {ϖ : Type u_1} (p : ProbExp ϖ) {x z y w : Exp ϖ} (h₁ : x ≤ z) (h₂ : y ≤ w) :

p.pick x y ≤ p.pick z w

source

@[simp]

theorem pGCL.ProbExp.pick_le' {ϖ : Type u_1} (p : ProbExp ϖ) (σ : States ϖ) {x z y w : Exp ϖ} (h₁ : x ≤ z) (h₂ : y ≤ w) :

p.pick x y σ ≤ p.pick z w σ

source

@[simp]

theorem pGCL.ProbExp.pick_same {ϖ : Type u_1} (p : ProbExp ϖ) {x : Exp ϖ} :

p.pick x x = x

source

@[simp]

theorem pGCL.ProbExp.pick_of {ϖ : Type u_1} (p : ProbExp ϖ) (σ : States ϖ) {x y : Exp ϖ} :

↑p σ * x σ + (1 - ↑p σ) * y σ = p.pick x y σ