Probability Lemmas About Monad Operations

This file contains lemmas about evalDist applied to monadic operations like pure and bind.

theorem probFailure_bind_congr {ι : Type v} {spec : OracleSpec ι} {α β γ : Type u} [spec.FiniteRange] (oa : OracleComp spec α) {ob : α → OracleComp spec β} {oc : α → OracleComp spec γ} (h : ∀ x ∈ oa.support, [⊥|ob x] = [⊥|oc x]) : [⊥|oa >>= ob] = [⊥|oa >>= oc]

theorem probFailure_bind_congr' {ι : Type v} {spec : OracleSpec ι} {α β γ : Type u} [spec.FiniteRange] (oa : OracleComp spec α) {ob : α → OracleComp spec β} {oc : α → OracleComp spec γ} (h : ∀ (x : α), [⊥|ob x] = [⊥|oc x]) : [⊥|oa >>= ob] = [⊥|oa >>= oc]

theorem probOutput_bind_congr {ι : Type v} {spec : OracleSpec ι} {α β : Type u} [spec.FiniteRange] {oa : OracleComp spec α} {ob₁ ob₂ : α → OracleComp spec β} {y : β} (h : ∀ x ∈ oa.support, [=y|ob₁ x] = [=y|ob₂ x]) : [=y|oa >>= ob₁] = [=y|oa >>= ob₂]

theorem probOutput_bind_congr' {ι : Type v} {spec : OracleSpec ι} {α β : Type u} [spec.FiniteRange] (oa : OracleComp spec α) {ob₁ ob₂ : α → OracleComp spec β} (y : β) (h : ∀ (x : α), [=y|ob₁ x] = [=y|ob₂ x]) : [=y|oa >>= ob₁] = [=y|oa >>= ob₂]

theorem probOutput_bind_mono {ι : Type v} {spec : OracleSpec ι} {α β γ : Type u} [spec.FiniteRange] {oa : OracleComp spec α} {ob : α → OracleComp spec β} {oc : α → OracleComp spec γ} {y : β} {z : γ} (h : ∀ x ∈ oa.support, [=y|ob x] ≤ [=z|oc x]) : [=y|oa >>= ob] ≤ [=z|oa >>= oc]

theorem probOutput_bind_congr_div_const {ι : Type v} {spec : OracleSpec ι} {α β : Type u} [spec.FiniteRange] {oa : OracleComp spec α} {ob₁ ob₂ : α → OracleComp spec β} {y : β} {r : ENNReal} (h : ∀ x ∈ oa.support, [=y|ob₁ x] = [=y|ob₂ x] / r) : [=y|oa >>= ob₁] = [=y|oa >>= ob₂] / r

theorem probOutput_bind_congr_eq_add {ι : Type v} {spec : OracleSpec ι} {α β : Type u} [spec.FiniteRange] {γ₁ γ₂ : Type u} {oa : OracleComp spec α} {ob : α → OracleComp spec β} {oc₁ : α → OracleComp spec γ₁} {oc₂ : α → OracleComp spec γ₂} {y : β} {z₁ : γ₁} {z₂ : γ₂} (h : ∀ x ∈ oa.support, [=y|ob x] = [=z₁|oc₁ x] + [=z₂|oc₂ x]) : [=y|oa >>= ob] = [=z₁|oa >>= oc₁] + [=z₂|oa >>= oc₂]

theorem probOutput_bind_congr_le_add {ι : Type v} {spec : OracleSpec ι} {α β : Type u} [spec.FiniteRange] {γ₁ γ₂ : Type u} {oa : OracleComp spec α} {ob : α → OracleComp spec β} {oc₁ : α → OracleComp spec γ₁} {oc₂ : α → OracleComp spec γ₂} {y : β} {z₁ : γ₁} {z₂ : γ₂} (h : ∀ x ∈ oa.support, [=y|ob x] ≤ [=z₁|oc₁ x] + [=z₂|oc₂ x]) : [=y|oa >>= ob] ≤ [=z₁|oa >>= oc₁] + [=z₂|oa >>= oc₂]

theorem probOutput_bind_congr_add_le {ι : Type v} {spec : OracleSpec ι} {α β : Type u} [spec.FiniteRange] {γ₁ γ₂ : Type u} {oa : OracleComp spec α} {ob : α → OracleComp spec β} {oc₁ : α → OracleComp spec γ₁} {oc₂ : α → OracleComp spec γ₂} {y : β} {z₁ : γ₁} {z₂ : γ₂} (h : ∀ x ∈ oa.support, [=z₁|oc₁ x] + [=z₂|oc₂ x] ≤ [=y|ob x]) : [=z₁|oa >>= oc₁] + [=z₂|oa >>= oc₂] ≤ [=y|oa >>= ob]

theorem probOutput_bind_congr_le_sub {ι : Type v} {spec : OracleSpec ι} {α β : Type u} [spec.FiniteRange] {γ₁ γ₂ : Type u} {oa : OracleComp spec α} {ob : α → OracleComp spec β} {oc₁ : α → OracleComp spec γ₁} {oc₂ : α → OracleComp spec γ₂} {y : β} {z₁ : γ₁} {z₂ : γ₂} (h : ∀ x ∈ oa.support, [=y|ob x] ≤ [=z₁|oc₁ x] - [=z₂|oc₂ x]) : [=y|oa >>= ob] ≤ [=z₁|oa >>= oc₁] - [=z₂|oa >>= oc₂]

theorem probOutput_bind_congr_sub_le {ι : Type v} {spec : OracleSpec ι} {α β : Type u} [spec.FiniteRange] {γ₁ γ₂ : Type u} {oa : OracleComp spec α} {ob : α → OracleComp spec β} {oc₁ : α → OracleComp spec γ₁} {oc₂ : α → OracleComp spec γ₂} {y : β} {z₁ : γ₁} {z₂ : γ₂} (h : ∀ x ∈ oa.support, [=z₁|oc₁ x] - [=z₂|oc₂ x] ≤ [=y|ob x]) : [=z₁|oa >>= oc₁] - [=z₂|oa >>= oc₂] ≤ [=y|oa >>= ob]