PGCL.ProbExp

source

def pGCL.ProbExp {𝒱 : Type u_2} (Γ : 𝒱 → Type u_1) :

Type (max 0 u_1 u_2)

Equations

pGCL.ProbExp Γ = { e : pGCL.State Γ → ENNReal // e ≤ 1 }

Instances For

source

instance pGCL.ProbExp.instFunLike {𝒱✝ : Type u_1} {Γ : 𝒱✝ → Type u_2} :

FunLike (ProbExp Γ) (State Γ) ENNReal

Equations

pGCL.ProbExp.instFunLike = { coe := Subtype.val, coe_injective' := ⋯ }

source

theorem pGCL.ProbExp.ext {𝒱✝ : Type u_1} {Γ : 𝒱✝ → Type u_2} {p q : ProbExp Γ} (h : ∀ (σ : State Γ), p σ = q σ) :

p = q

source

theorem pGCL.ProbExp.ext_iff {𝒱✝ : Type u_1} {Γ : 𝒱✝ → Type u_2} {p q : ProbExp Γ} :

p = q ↔ ∀ (σ : State Γ), p σ = q σ

source

@[simp]

theorem pGCL.ProbExp.coe_apply {𝒱✝ : Type u_1} {Γ : 𝒱✝ → Type u_2} {σ : State Γ} {f : State Γ → ENNReal} {h : f ≤ 1} :

⟨f, h⟩ σ = f σ

source

@[simp]

theorem pGCL.ProbExp.mk_val {𝒱✝ : Type u_1} {Γ : 𝒱✝ → Type u_2} {f : State Γ → ENNReal} {h : f ≤ 1} :

↑⟨f, h⟩ = f

source

@[simp]

theorem pGCL.ProbExp.mk_vcoe {𝒱✝ : Type u_1} {Γ : 𝒱✝ → Type u_2} {f : State Γ → ENNReal} {h : f ≤ 1} :

⇑⟨f, h⟩ = f

source

def pGCL.ProbExp.ofExp {𝒱✝ : Type u_1} {Γ : 𝒱✝ → Type u_2} (x : State Γ → ENNReal) :

ProbExp Γ

Equations

pGCL.ProbExp.ofExp x = ⟨x ⊓ 1, ⋯⟩

Instances For

source

@[simp]

theorem pGCL.ProbExp.ofExp_apply {𝒱✝ : Type u_1} {Γ : 𝒱✝ → Type u_2} {σ : State Γ} (x : State Γ → ENNReal) :

(ofExp x) σ = min (x σ) 1

source

@[simp]

def pGCL.ProbExp.ofExp_coe {𝒱✝ : Type u_1} {Γ : 𝒱✝ → Type u_2} (x : ProbExp Γ) :

ofExp ⇑x = x

Equations

⋯ = ⋯

Instances For

source

instance pGCL.ProbExp.instLE {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} :

LE (ProbExp Γ)

Equations

pGCL.ProbExp.instLE = { le := fun (a b : pGCL.ProbExp Γ) => ∀ (x : pGCL.State Γ), a x ≤ b x }

source

@[simp]

theorem pGCL.ProbExp.coe_le {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} {f g : State Γ → ENNReal} {hf : f ≤ 1} {hg : g ≤ 1} :

⟨f, hf⟩ ≤ ⟨g, hg⟩ ↔ f ≤ g

source

instance pGCL.ProbExp.instPartialOrder {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} :

PartialOrder (ProbExp Γ)

Equations

pGCL.ProbExp.instPartialOrder = { toLE := pGCL.ProbExp.instLE, lt := fun (a b : pGCL.ProbExp Γ) => a ≤ b ∧ ¬b ≤ a, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯, le_antisymm := ⋯ }

source

@[simp]

theorem pGCL.ProbExp.add_one_apply {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} (p : ProbExp Γ) (σ : State Γ) :

p σ + (1 - p σ) = 1

source

instance pGCL.ProbExp.instOfNat0 {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} :

OfNat (ProbExp Γ) 0

Equations

pGCL.ProbExp.instOfNat0 = { ofNat := ⟨fun (x : pGCL.State Γ) => 0, ⋯⟩ }

source

instance pGCL.ProbExp.instOfNat1 {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} :

OfNat (ProbExp Γ) 1

Equations

pGCL.ProbExp.instOfNat1 = { ofNat := ⟨fun (x : pGCL.State Γ) => 1, ⋯⟩ }

source

@[simp]

theorem pGCL.ProbExp.zero_apply {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} (σ : State Γ) :

(OfNat.ofNat 0) σ = 0

source

@[simp]

theorem pGCL.ProbExp.one_apply {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} (σ : State Γ) :

(OfNat.ofNat 1) σ = 1

source

@[simp]

theorem pGCL.ProbExp.le_one {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} (p : ProbExp Γ) :

p ≤ 1

source

@[simp]

theorem pGCL.ProbExp.zero_le {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} (p : ProbExp Γ) :

0 ≤ p

source

@[simp]

theorem pGCL.ProbExp.le_one_apply {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} (p : ProbExp Γ) (σ : State Γ) :

p σ ≤ 1

source

@[simp]

theorem pGCL.ProbExp.val_le_one {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} (p : ProbExp Γ) :

↑p ≤ 1

source

@[simp]

theorem pGCL.ProbExp.zero_le_apply {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} (p : ProbExp Γ) (σ : State Γ) :

0 ≤ p σ

source

@[simp]

theorem pGCL.ProbExp.zero_val_le {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} (p : ProbExp Γ) :

0 ≤ ↑p

source

@[simp]

theorem pGCL.ProbExp.lt_one_iff {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} (p : ProbExp Γ) (σ : State Γ) :

¬p σ = 1 ↔ p σ < 1

source

@[simp]

theorem pGCL.ProbExp.sub_one_le_one {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} (p : ProbExp Γ) (σ : State Γ) :

1 - p σ ≤ 1

source

@[simp]

theorem pGCL.ProbExp.ne_top {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} (p : ProbExp Γ) (σ : State Γ) :

p σ ≠ ⊤

source

@[simp]

theorem pGCL.ProbExp.top_ne {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} (p : ProbExp Γ) (σ : State Γ) :

⊤ ≠ p σ

source

@[simp]

theorem pGCL.ProbExp.not_zero_off {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} (p : ProbExp Γ) (σ : State Γ) :

¬p σ = 0 ↔ 0 < p σ

source

@[simp]

theorem pGCL.ProbExp.lt_one_iff' {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} (p : ProbExp Γ) (σ : State Γ) :

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

source

@[simp]

theorem pGCL.ProbExp.top_ne_one_sub {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} (p : ProbExp Γ) (σ : State Γ) :

¬⊤ = 1 - p σ

source

@[simp]

theorem pGCL.ProbExp.one_le_iff {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} (p : ProbExp Γ) (σ : State Γ) :

1 ≤ p σ ↔ p σ = 1

source

@[simp]

theorem pGCL.ProbExp.ite_eq_zero {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} (p : ProbExp Γ) (σ : State Γ) {x : ENNReal} :

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

source

@[simp]

theorem pGCL.ProbExp.ite_eq_one {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} (p : ProbExp Γ) (σ : State Γ) {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} {Γ : 𝒱 → Type u_2} (p : ProbExp Γ) (σ : State Γ) :

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

source

@[simp]

theorem pGCL.ProbExp.ite_eq_one' {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} (p : ProbExp Γ) (σ : State Γ) :

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

source

instance pGCL.ProbExp.instSubstitutionForallStateOfDecidableEq {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} [DecidableEq 𝒱] :

Substitution (ProbExp Γ) fun (x : 𝒱) => State Γ → Γ x

Equations

pGCL.ProbExp.instSubstitutionForallStateOfDecidableEq = { subst := fun (b : pGCL.ProbExp Γ) (x : (x : 𝒱) × (pGCL.State Γ → Γ x)) => ⟨fun (σ : pGCL.State Γ) => b (σ[x.fst ↦ x.snd σ]), ⋯⟩ }

source

@[simp]

theorem pGCL.ProbExp.subst_apply {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} (σ : State Γ) [DecidableEq 𝒱] {a : ProbExp Γ} {x : 𝒱} {A : State Γ → Γ x} :

(a[x ↦ A]) σ = a (σ[x ↦ A σ])

source

def pGCL.ProbExp.exp_coe {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} :

ProbExp Γ → State Γ → ENNReal

Equations

pGCL.ProbExp.exp_coe = Subtype.val

Instances For

source

instance pGCL.ProbExp.instCoeForallStateENNReal {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} :

Coe (ProbExp Γ) (State Γ → ENNReal)

Equations

pGCL.ProbExp.instCoeForallStateENNReal = { coe := pGCL.ProbExp.exp_coe }

source

@[simp]

theorem pGCL.ProbExp.exp_coe_apply {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} (p : ProbExp Γ) (σ : State Γ) :

↑p σ = p σ

source

@[simp]

theorem pGCL.ProbExp.coe_exp_coe {𝒱✝ : Type u_3} {Γ✝ : 𝒱✝ → Type u_4} {x : State Γ✝ → ENNReal} {hx : x ≤ 1} :

↑⟨x, hx⟩ = x

source

noncomputable instance pGCL.ProbExp.instHMulForallStateENNReal {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} :

HMul (ProbExp Γ) (State Γ → ENNReal) (State Γ → ENNReal)

Equations

pGCL.ProbExp.instHMulForallStateENNReal = { hMul := fun (p : pGCL.ProbExp Γ) (x : pGCL.State Γ → ENNReal) => ↑p * x }

source

noncomputable instance pGCL.ProbExp.instHMulForallStateENNReal_1 {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} :

HMul (State Γ → ENNReal) (ProbExp Γ) (State Γ → ENNReal)

Equations

pGCL.ProbExp.instHMulForallStateENNReal_1 = { hMul := fun (x : pGCL.State Γ → ENNReal) (p : pGCL.ProbExp Γ) => x * ↑p }

source

@[simp]

theorem pGCL.ProbExp.hMul_Exp_apply {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} (σ : State Γ) {p : ProbExp Γ} {x : State Γ → ENNReal} :

(⇑p * x) σ = p σ * x σ

source

@[simp]

theorem pGCL.ProbExp.Exp_hMul_apply {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} (σ : State Γ) {p : ProbExp Γ} {x : State Γ → ENNReal} :

(x * ⇑p) σ = x σ * p σ

source

noncomputable instance pGCL.ProbExp.instMul {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} :

Mul (ProbExp Γ)

Equations

pGCL.ProbExp.instMul = { mul := fun (a b : pGCL.ProbExp Γ) => ⟨fun (σ : pGCL.State Γ) => a σ * b σ, ⋯⟩ }

source

noncomputable instance pGCL.ProbExp.instAdd {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} :

Add (ProbExp Γ)

Equations

pGCL.ProbExp.instAdd = { add := fun (a b : pGCL.ProbExp Γ) => ⟨fun (σ : pGCL.State Γ) => min (a σ + b σ) 1, ⋯⟩ }

source

noncomputable instance pGCL.ProbExp.instSub {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} :

Sub (ProbExp Γ)

Equations

pGCL.ProbExp.instSub = { sub := fun (a b : pGCL.ProbExp Γ) => ⟨fun (σ : pGCL.State Γ) => a σ - b σ, ⋯⟩ }

source

@[simp]

theorem pGCL.ProbExp.add_apply {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} (σ : State Γ) {a b : ProbExp Γ} :

(a + b) σ = min (a σ + b σ) 1

source

@[simp]

theorem pGCL.ProbExp.mul_apply {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} (σ : State Γ) {a b : ProbExp Γ} :

(a * b) σ = a σ * b σ

source

@[simp]

theorem pGCL.ProbExp.sub_apply {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} (σ : State Γ) {a b : ProbExp Γ} :

(a - b) σ = a σ - b σ

source

@[simp]

theorem pGCL.ProbExp.add_subst {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} {a b : ProbExp Γ} [DecidableEq 𝒱] {x : 𝒱} {A : State Γ → Γ x} :

(a + b)[x ↦ A] = a[x ↦ A] + b[x ↦ A]

source

@[simp]

theorem pGCL.ProbExp.mul_subst {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} {a b : ProbExp Γ} [DecidableEq 𝒱] {x : 𝒱} {A : State Γ → Γ x} :

(a * b)[x ↦ A] = a[x ↦ A] * b[x ↦ A]

source

@[simp]

theorem pGCL.ProbExp.sub_subst {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} {a b : ProbExp Γ} [DecidableEq 𝒱] {x : 𝒱} {A : State Γ → Γ x} :

(a - b)[x ↦ A] = a[x ↦ A] - b[x ↦ A]

source

@[simp]

theorem pGCL.ProbExp.zero_subst {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} [DecidableEq 𝒱] {x : 𝒱} {A : State Γ → Γ x} :

0[x ↦ A] = 0

source

@[simp]

theorem pGCL.ProbExp.one_subst {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} [DecidableEq 𝒱] {x : 𝒱} {A : State Γ → Γ x} :

1[x ↦ A] = 1

source

noncomputable def pGCL.ProbExp.pick' {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} (p : ProbExp Γ) (x y : (State Γ → ENNReal) →o State Γ → ENNReal) :

(State Γ → ENNReal) →o State Γ → ENNReal

Equations

p.pick' x y = { toFun := fun (X : pGCL.State Γ → ENNReal) => ⇑p * x X + (1 - ⇑p) * y X, monotone' := ⋯ }

Instances For

source

@[simp]

theorem pGCL.ProbExp.pick'_apply {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} (p : ProbExp Γ) {x y : (State Γ → ENNReal) →o State Γ → ENNReal} {X : State Γ → ENNReal} :

(p.pick' x y) X = ⇑p * x X + (1 - ⇑p) * y X

source

@[simp]

theorem pGCL.ProbExp.pick'_apply2 {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} (p : ProbExp Γ) (σ : State Γ) {x y : (State Γ → ENNReal) →o State Γ → ENNReal} {X : State Γ → ENNReal} :

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

source

def OmegaCompletePartialOrder.ωScottContinuous.apply_iSup {α : Type u_3} {ι : Type u_4} [CompleteLattice α] [CompleteLattice ι] {f : ι →o α} (hf : ωScottContinuous ⇑f) (c : Chain ι) :

f (⨆ (i : ℕ), c i) = ⨆ (i : ℕ), f (c i)

Equations

⋯ = ⋯

Instances For

source

noncomputable def pGCL.ProbExp.inv {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} (n : State Γ → ENNReal) :

ProbExp Γ

The expression 1/n where is defined to be 1 if n ≤ 1.

Equations

pGCL.ProbExp.inv n = ⟨fun (σ : pGCL.State Γ) => if h : n σ ≤ 1 then 1 else (n σ)⁻¹, ⋯⟩

Instances For

source

@[simp]

theorem pGCL.ProbExp.inv_apply {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} (σ : State Γ) {n : State Γ → ENNReal} :

(inv n) σ = if n σ ≤ 1 then 1 else (n σ)⁻¹

source

instance pGCL.ProbExp.instBot {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} :

Bot (ProbExp Γ)

Equations

pGCL.ProbExp.instBot = { bot := 0 }

source

instance pGCL.ProbExp.instTop {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} :

Top (ProbExp Γ)

Equations

pGCL.ProbExp.instTop = { top := 1 }

source

@[simp]

theorem pGCL.ProbExp.bot_eq_0 {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} :

⊥ = 0

source

@[simp]

theorem pGCL.ProbExp.top_eq_1 {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} :

⊤ = 1

source

noncomputable instance pGCL.ProbExp.instCompleteLattice {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} :

CompleteLattice (ProbExp Γ)

Equations

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

source

@[simp]

theorem pGCL.ProbExp.sSup_apply {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} {x : State Γ} (S : Set (ProbExp Γ)) :

(sSup S) x = ⨆ s ∈ S, s x

source

@[simp]

theorem pGCL.ProbExp.sInf_apply {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} {x : State Γ} (S : Set (ProbExp Γ)) (hS : S.Nonempty) :

(sInf S) x = ⨅ s ∈ S, s x

source

@[simp]

theorem pGCL.ProbExp.iSup_apply {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} {ι : Sort u_3} {x : State Γ} (f : ι → ProbExp Γ) :

(⨆ (i : ι), f i) x = ⨆ (i : ι), (f i) x

source

@[simp]

theorem pGCL.ProbExp.iInf_apply {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} {ι : Sort u_3} {x : State Γ} [Nonempty ι] (f : ι → ProbExp Γ) :

(⨅ (i : ι), f i) x = ⨅ (i : ι), (f i) x

source

@[simp]

theorem pGCL.ProbExp.sup_apply {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} (σ : State Γ) {f g : ProbExp Γ} :

(f ⊔ g) σ = max (f σ) (g σ)

source

@[simp]

theorem pGCL.ProbExp.inf_apply {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} (σ : State Γ) {f g : ProbExp Γ} :

(f ⊓ g) σ = min (f σ) (g σ)

source

@[simp]

theorem pGCL.ProbExp.sup_coe_apply {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} (σ : State Γ) {f g : ProbExp Γ} :

↑(f ⊔ g) σ = max (f σ) (g σ)

source

@[simp]

theorem pGCL.ProbExp.inf_coe_apply {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} (σ : State Γ) {f g : ProbExp Γ} :

↑(f ⊓ g) σ = min (f σ) (g σ)

source

@[simp]

theorem pGCL.ProbExp.max_apply {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} (σ : State Γ) {f g : ProbExp Γ} :

(f ⊔ g) σ = max (f σ) (g σ)

source

@[simp]

theorem pGCL.ProbExp.min_apply {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} (σ : State Γ) {f g : ProbExp Γ} :

(f ⊓ g) σ = min (f σ) (g σ)

source

@[simp]

theorem pGCL.ProbExp.max_coe_apply {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} (σ : State Γ) {f g : ProbExp Γ} :

↑(f ⊔ g) σ = max (f σ) (g σ)

source

@[simp]

theorem pGCL.ProbExp.min_coe_apply {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} (σ : State Γ) {f g : ProbExp Γ} :

↑(f ⊓ g) σ = min (f σ) (g σ)

source

@[simp]

theorem pGCL.ProbExp.one_mul {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} (p : ProbExp Γ) :

1 * p = p

source

@[simp]

theorem pGCL.ProbExp.zero_mul {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} (p : ProbExp Γ) :

0 * p = 0

source

@[simp]

theorem pGCL.ProbExp.mul_one {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} (p : ProbExp Γ) :

p * 1 = p

source

@[simp]

theorem pGCL.ProbExp.mul_zero {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} (p : ProbExp Γ) :

p * 0 = 0

source

@[simp]

theorem pGCL.ProbExp.one_add {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} (p : ProbExp Γ) :

1 + p = 1

source

@[simp]

theorem pGCL.ProbExp.add_one {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} (p : ProbExp Γ) :

p + 1 = 1

source

@[simp]

theorem pGCL.ProbExp.zero_add {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} (p : ProbExp Γ) :

0 + p = p

source

@[simp]

theorem pGCL.ProbExp.add_zero {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} (p : ProbExp Γ) :

p + 0 = p

source

@[simp]

theorem pGCL.ProbExp.sub_one {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} (p : ProbExp Γ) :

p - 1 = 0

source

@[simp]

theorem pGCL.ProbExp.zero_sub {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} (p : ProbExp Γ) :

0 - p = 0

source

@[simp]

theorem pGCL.ProbExp.sub_zero {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} (p : ProbExp Γ) :

p - 0 = p

source

@[simp]

theorem pGCL.ProbExp.coe_one {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} :

↑1 = 1

source

@[simp]

theorem pGCL.ProbExp.coe_zero {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} :

↑0 = 0

source

theorem pGCL.ProbExp.mul_le_mul {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} (a b c d : ProbExp Γ) (hac : a ≤ c) (hbd : b ≤ d) :

a * b ≤ c * d

source

theorem pGCL.ProbExp.add_le_add {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} (a b c d : ProbExp Γ) (hac : a ≤ c) (hbd : b ≤ d) :

a + b ≤ c + d

source

theorem pGCL.ProbExp.sub_le_sub {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} (a b c d : ProbExp Γ) (hac : a ≤ c) (hdb : d ≤ b) :

a - b ≤ c - d

source

@[simp]

theorem pGCL.ProbExp.pick_le {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} (σ : State Γ) {l x r : ENNReal} {p : ProbExp Γ} (hl : l ≤ x) (hr : r ≤ x) :

p σ * l + (1 - p σ) * r ≤ x

source

@[simp]

theorem pGCL.ProbExp.coe_inv {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} {X : State Γ → ENNReal} :

↑(inv X) = X⁻¹ ⊓ 1

source

@[simp]

theorem pGCL.ProbExp.exp_coe_subst {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} [DecidableEq 𝒱] {X : ProbExp Γ} {x : 𝒱} {e : State Γ → Γ x} :

(↑X)[x ↦ e] = ↑(X[x ↦ e])

source

@[simp]

theorem pGCL.ProbExp.inv_subst {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} [DecidableEq 𝒱] {X : State Γ → ENNReal} {x : 𝒱} {e : State Γ → Γ x} :

(inv X)[x ↦ e] = inv (X[x ↦ e])

source

@[simp]

theorem pGCL.ProbExp.one_sub_one_sub_apply {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} (σ : State Γ) {X : ProbExp Γ} :

1 - (1 - X σ) = X σ

source

@[simp]

theorem pGCL.ProbExp.one_sub_one_sub {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} {X : ProbExp Γ} :

1 - (1 - X) = X

source

@[simp]

theorem pGCL.ProbExp.one_sub_le {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} {X : ProbExp Γ} :

1 - ↑X ≤ 1

source

noncomputable instance pGCL.ProbExp.instHImp {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} :

HImp (ProbExp Γ)

Equations

pGCL.ProbExp.instHImp = { himp := fun (a b : pGCL.ProbExp Γ) => ⟨fun (σ : pGCL.State Γ) => if a σ ≤ b σ then 1 else b σ, ⋯⟩ }

source

@[simp]

theorem pGCL.ProbExp.one_le {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} {p : ProbExp Γ} :

1 ≤ p ↔ p = 1

source

theorem pGCL.ProbExp.himp_mono {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} {l₁ l₂ r₁ r₂ : ProbExp Γ} (hl : l₂ ≤ l₁) (hr : r₁ ≤ r₂) :

l₁ ⇨ r₁ ≤ l₂ ⇨ r₂

source

@[simp]

theorem pGCL.ProbExp.himp_apply {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} (σ : State Γ) {l r : ProbExp Γ} :

(l ⇨ r) σ = if l σ ≤ r σ then 1 else r σ

source

noncomputable instance pGCL.ProbExp.instCompl {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} :

Compl (ProbExp Γ)

Equations

pGCL.ProbExp.instCompl = { compl := fun (x : pGCL.ProbExp Γ) => 1 - x }

source

noncomputable instance pGCL.ProbExp.instDistribLattice {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} :

DistribLattice (ProbExp Γ)

Equations

pGCL.ProbExp.instDistribLattice = { toLattice := CompleteLattice.toConditionallyCompleteLattice.toLattice, le_sup_inf := ⋯ }

source

theorem pGCL.ProbExp.compl_mono {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} {p r : ProbExp Γ} (h : r ≤ p) :

~ p ≤ ~ r

source

@[simp]

theorem pGCL.ProbExp.compl_compl {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} {p : ProbExp Γ} :

~ ~ p = p

source

theorem pGCL.ProbExp.gfp_eq_one_sub_lfp {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} {f : ProbExp Γ →o ProbExp Γ} :

OrderHom.gfp f = 1 - OrderHom.lfp { toFun := fun (x : ProbExp Γ) => 1 - f (1 - x), monotone' := ⋯ }

source

noncomputable instance pGCL.ProbExp.instComplOrderHom {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} :

Compl (ProbExp Γ →o ProbExp Γ)

Equations

pGCL.ProbExp.instComplOrderHom = { compl := fun (f : pGCL.ProbExp Γ →o pGCL.ProbExp Γ) => { toFun := fun (x : pGCL.ProbExp Γ) => ~ f (~ x), monotone' := ⋯ } }

source

@[simp]

theorem pGCL.ProbExp.orderHom_compl_compl {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} {f : ProbExp Γ →o ProbExp Γ} :

~ ~ f = f

source

theorem pGCL.ProbExp.gfp_eq_lfp_compl {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} {f : ProbExp Γ →o ProbExp Γ} :

OrderHom.gfp f = ~ OrderHom.lfp (~ f)

source

theorem pGCL.ProbExp.lfp_eq_gfp_compl {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} {f : ProbExp Γ →o ProbExp Γ} :

OrderHom.lfp f = ~ OrderHom.gfp (~ f)

source

noncomputable def pGCL.BExpr.probOf {𝒱✝ : Type u_1} {Γ : 𝒱✝ → Type u_2} (b : BExpr Γ) :

ProbExp Γ

Equations

p[b] = ⟨i[b], ⋯⟩

Instances For

source

def pGCL.BExpr.«termP[_]» :

Lean.ParserDescr

Equations

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

Instances For

source

@[simp]

theorem pGCL.BExpr.probOf_apply {𝒱✝ : Type u_1} {Γ : 𝒱✝ → Type u_2} {σ : State Γ} (b : BExpr Γ) :

p[b] σ = ↑i[b σ]