Measure reasoning from structural support

Continuations that denote the same measure on all syntactically reachable outputs may be interchanged. The proof inducts on the free program, so no probability/support bridge or positivity assumption on query answers is necessary.

If every query answer has positive singleton mass, a second induction identifies structural support with positive output mass. Native uniform oracle specifications satisfy that condition, so their events of probability one, zero, or positive probability are exactly the events holding on all, none, or some structurally reachable outputs; wrapped optional computations are observed through their present values.

theorem OracleComp.evalDist_bind_congr_of_support {ι : Type u} {α β : Type} {spec : OracleSpec ι} [(t : ι) → MeasurableSpace (spec.Range t)] [∀ (t : ι), DiscreteMeasurableSpace (spec.Range t)] [MeasurableSpace β] [EvalDistSemantics (OracleComp spec)] [LawfulEvalDistSemantics (OracleComp spec)] (mx : OracleComp spec α) (f g : α → OracleComp spec β) (h : ∀ a ∈ support mx, 𝒟[f a] = 𝒟[g a]) : 𝒟[mx >>= f] = 𝒟[mx >>= g]

Equal continuation measures on structural support give equal composed measures.

theorem OracleComp.evalDist_bind_bind_swap {ι : Type u} {α β γ : Type} {spec : OracleSpec ι} [(t : ι) → MeasurableSpace (spec.Range t)] [∀ (t : ι), DiscreteMeasurableSpace (spec.Range t)] [∀ (t : ι), Countable (spec.Range t)] [spec.IsMeasureSpec] [MeasurableSpace γ] (mx : OracleComp spec α) (my : OracleComp spec β) (f : α → β → OracleComp spec γ) : 𝒟[do let a ← mx let b ← my f a b] = 𝒟[do let b ← my let a ← mx f a b]

Independent oracle computations commute before any measurably observed continuation. Only the actual query answers must be countable; the two unobserved output types require neither countability nor measurable-space instances.

theorem OracleComp.lintegral_evalDist_bind_mono_of_support {ι : Type u} {α β γ : Type} {spec : OracleSpec ι} [(t : ι) → MeasurableSpace (spec.Range t)] [∀ (t : ι), DiscreteMeasurableSpace (spec.Range t)] [spec.IsMeasureSpec] [MeasurableSpace β] [MeasurableSpace γ] (mx : OracleComp spec α) (f : α → OracleComp spec β) (g : α → OracleComp spec γ) {v : β → ENNReal} {w : γ → ENNReal} (hv : Measurable v) (hw : Measurable w) (hfg : ∀ a ∈ support mx, ∫⁻ (y : β), v y ∂𝒟[f a] ≤ ∫⁻ (z : γ), w z ∂𝒟[g a]) : ∫⁻ (y : β), v y ∂𝒟[mx >>= f] ≤ ∫⁻ (z : γ), w z ∂𝒟[mx >>= g]

Compare measurable valuations of continuation outputs on structural support. The common computation's unobserved intermediate result needs no measurable-space instance.

theorem OracleComp.evalDist_bind_apply_mono_of_support {ι : Type u} {α β : Type} {spec : OracleSpec ι} [(t : ι) → MeasurableSpace (spec.Range t)] [∀ (t : ι), DiscreteMeasurableSpace (spec.Range t)] [spec.IsMeasureSpec] [MeasurableSpace β] (mx : OracleComp spec α) (f g : α → OracleComp spec β) {event : Set β} (hevent : MeasurableSet event) (hfg : ∀ a ∈ support mx, 𝒟[f a] event ≤ 𝒟[g a] event) : 𝒟[mx >>= f] event ≤ 𝒟[mx >>= g] event

Compare event masses after a common oracle computation when the continuation bound only needs to hold on structurally reachable outputs. This is the operational specialization of evalDist_bind_apply_mono: structural reachability supplies its almost-everywhere premise.

theorem OracleComp.evalDist_bind_apply_le_add_of_support {ι : Type u} {α β : Type} {spec : OracleSpec ι} [(t : ι) → MeasurableSpace (spec.Range t)] [∀ (t : ι), DiscreteMeasurableSpace (spec.Range t)] [spec.IsMeasureSpec] [MeasurableSpace β] (mx : OracleComp spec α) (f g h : α → OracleComp spec β) {event : Set β} (hevent : MeasurableSet event) (hfg : ∀ a ∈ support mx, 𝒟[f a] event ≤ 𝒟[g a] event + 𝒟[h a] event) : 𝒟[mx >>= f] event ≤ 𝒟[mx >>= g] event + 𝒟[mx >>= h] event

Additive continuation bounds on reachable outputs lift through a common oracle computation. No measurable space is required on the hidden common result type.

theorem OracleComp.le_evalDist_bind_apply_of_support {ι : Type u} {α β : Type} {spec : OracleSpec ι} [(t : ι) → MeasurableSpace (spec.Range t)] [∀ (t : ι), DiscreteMeasurableSpace (spec.Range t)] [spec.IsMeasureSpec] [MeasurableSpace β] (mx : OracleComp spec α) (f : α → OracleComp spec β) {event : Set β} (hevent : MeasurableSet event) {r : ENNReal} (h : ∀ a ∈ support mx, r ≤ 𝒟[f a] event) : r ≤ 𝒟[mx >>= f] event

A uniform lower bound on reachable continuation events bounds their composed event. The common computation need not carry a measurable-space instance on its output type.

theorem OracleComp.evalDist_bind_apply_eq_one_of_ae {ι : Type u} {α β : Type v} {spec : OracleSpec ι} [(t : ι) → MeasurableSpace (spec.Range t)] [∀ (t : ι), DiscreteMeasurableSpace (spec.Range t)] [spec.IsMeasureSpec] [MeasurableSpace α] [DiscreteMeasurableSpace α] [MeasurableSpace β] (mx : OracleComp spec α) (f : α → OracleComp spec β) {event : Set β} (hevent : MeasurableSet event) (h : ∀ᵐ (a : α) ∂𝒟[mx], 𝒟[f a] event = 1) : 𝒟[mx >>= f] event = 1

Almost-sure probability-one continuation events remain probability one after sequencing a lossless oracle computation.

theorem OracleComp.prEvent_congr_of_support {ι : Type u} {α : Type} {spec : OracleSpec ι} [(t : ι) → MeasurableSpace (spec.Range t)] [∀ (t : ι), DiscreteMeasurableSpace (spec.Range t)] [spec.IsMeasureSpec] (mx : OracleComp spec α) (p q : α → Prop) (h : ∀ a ∈ support mx, p a ↔ q a) : 𝒟[do let a ← mx pure (p a)] {True} = 𝒟[do let a ← mx pure (q a)] {True}

Events agreeing on every possible output have equal successful probability.

theorem OracleComp.prEvent_mono_of_support {ι : Type u} {α : Type} {spec : OracleSpec ι} [(t : ι) → MeasurableSpace (spec.Range t)] [∀ (t : ι), DiscreteMeasurableSpace (spec.Range t)] [spec.IsMeasureSpec] (mx : OracleComp spec α) {p q : α → Prop} (h : ∀ a ∈ support mx, p a → q a) : 𝒟[do let a ← mx pure (p a)] {True} ≤ 𝒟[do let a ← mx pure (q a)] {True}

Implication on structurally reachable outputs bounds native event probability.

theorem OracleComp.mem_support_iff_evalDist_singleton_pos_of_fullSupport {ι : Type u} {spec : OracleSpec ι} [(t : ι) → MeasurableSpace (spec.Range t)] [∀ (t : ι), DiscreteMeasurableSpace (spec.Range t)] [spec.IsMeasureSpec] (hfull : ∀ (t : ι) (u : spec.Range t), 0 < (OracleSpec.IsMeasureSpec.toMeasure t) {u}) {α : Type v} [MeasurableSpace α] [MeasurableSingletonClass α] (mx : OracleComp spec α) (x : α) : x ∈ support mx ↔ 0 < 𝒟[mx] {x}

Structural support is positive singleton mass when every oracle response has positive singleton mass. The full-support hypothesis belongs to the chosen measure interpretation; finiteness alone does not determine it.

theorem OracleComp.evalDist_apply_setOf_eq_one_iff_forall_mem_support_of_fullSupport {ι : Type u} {α : Type v} {spec : OracleSpec ι} [(t : ι) → MeasurableSpace (spec.Range t)] [∀ (t : ι), DiscreteMeasurableSpace (spec.Range t)] [spec.IsMeasureSpec] (hfull : ∀ (t : ι) (u : spec.Range t), 0 < (OracleSpec.IsMeasureSpec.toMeasure t) {u}) [MeasurableSpace α] [DiscreteMeasurableSpace α] (mx : OracleComp spec α) (p : α → Prop) : 𝒟[mx] {x : α | p x} = 1 ↔ ∀ x ∈ support mx, p x

An event has probability one exactly when it contains every structurally reachable output, provided every oracle response has positive singleton mass.

theorem OracleComp.mem_support_iff_evalDist_singleton_pos {ι : Type u} {spec : OracleSpec ι} [(t : ι) → MeasurableSpace (spec.Range t)] [∀ (t : ι), DiscreteMeasurableSpace (spec.Range t)] [spec.IsUniformMeasureSpec] {α : Type v} [MeasurableSpace α] [MeasurableSingletonClass α] (mx : OracleComp spec α) (x : α) : x ∈ support mx ↔ 0 < 𝒟[mx] {x}

Under native uniform oracle semantics, structural reachability is positive singleton mass.

theorem OracleComp.evalDist_apply_setOf_eq_one_iff_forall_mem_support {ι : Type u} {α : Type v} {spec : OracleSpec ι} [(t : ι) → MeasurableSpace (spec.Range t)] [∀ (t : ι), DiscreteMeasurableSpace (spec.Range t)] [spec.IsUniformMeasureSpec] [MeasurableSpace α] [DiscreteMeasurableSpace α] (mx : OracleComp spec α) (p : α → Prop) : 𝒟[mx] {x : α | p x} = 1 ↔ ∀ x ∈ support mx, p x

Under native uniform oracle semantics, an event has probability one exactly when it contains every structurally reachable output.

Events in Pr{} form

theorem OracleComp.prEvent_true_eq_one {ι : Type u} {spec : OracleSpec ι} [(t : ι) → MeasurableSpace (spec.Range t)] [∀ (t : ι), DiscreteMeasurableSpace (spec.Range t)] [spec.IsMeasureSpec] {α : Type} (mx : OracleComp spec α) : 𝒟[do let _ ← mx pure True] {True} = 1

Oracle computations with a measure interpretation are lossless.

theorem OracleComp.prEvent_eq_one_of_forall_mem_support {ι : Type u} {spec : OracleSpec ι} [(t : ι) → MeasurableSpace (spec.Range t)] [∀ (t : ι), DiscreteMeasurableSpace (spec.Range t)] [spec.IsMeasureSpec] {α : Type} (mx : OracleComp spec α) (p : α → Prop) (h : ∀ x ∈ support mx, p x) : 𝒟[do let x ← mx pure (p x)] {True} = 1

An event containing every structurally reachable output has probability one.

theorem OracleComp.prEvent_eq_zero_of_forall_mem_support {ι : Type u} {spec : OracleSpec ι} [(t : ι) → MeasurableSpace (spec.Range t)] [∀ (t : ι), DiscreteMeasurableSpace (spec.Range t)] [spec.IsMeasureSpec] {α : Type} (mx : OracleComp spec α) (p : α → Prop) (h : ∀ x ∈ support mx, ¬p x) : 𝒟[do let x ← mx pure (p x)] {True} = 0

An event avoiding every structurally reachable output has probability zero.

theorem OracleComp.prEvent_eq_one_iff {ι : Type u} {spec : OracleSpec ι} [(t : ι) → MeasurableSpace (spec.Range t)] [∀ (t : ι), DiscreteMeasurableSpace (spec.Range t)] [spec.IsUniformMeasureSpec] {α : Type} (mx : OracleComp spec α) (p : α → Prop) : 𝒟[do let x ← mx pure (p x)] {True} = 1 ↔ ∀ x ∈ support mx, p x

Under native uniform oracle semantics, an event has probability one exactly when it holds on every structurally reachable output.

theorem OracleComp.prEvent_eq_zero_iff {ι : Type u} {spec : OracleSpec ι} [(t : ι) → MeasurableSpace (spec.Range t)] [∀ (t : ι), DiscreteMeasurableSpace (spec.Range t)] [spec.IsUniformMeasureSpec] {α : Type} (mx : OracleComp spec α) (p : α → Prop) : 𝒟[do let x ← mx pure (p x)] {True} = 0 ↔ ∀ x ∈ support mx, ¬p x

Under native uniform oracle semantics, an event has probability zero exactly when it fails on every structurally reachable output.

theorem OracleComp.prEvent_pos_iff {ι : Type u} {spec : OracleSpec ι} [(t : ι) → MeasurableSpace (spec.Range t)] [∀ (t : ι), DiscreteMeasurableSpace (spec.Range t)] [spec.IsUniformMeasureSpec] {α : Type} (mx : OracleComp spec α) (p : α → Prop) : 0 < 𝒟[do let x ← mx pure (p x)] {True} ↔ ∃ x ∈ support mx, p x

Under native uniform oracle semantics, an event has positive probability exactly when some structurally reachable output satisfies it.

theorem OracleComp.OptionT.prEvent_mk_eq_one_iff {ι : Type u} {spec : OracleSpec ι} [(t : ι) → MeasurableSpace (spec.Range t)] [∀ (t : ι), DiscreteMeasurableSpace (spec.Range t)] [spec.IsUniformMeasureSpec] {α : Type} (mx : OracleComp spec (Option α)) (p : α → Prop) : 𝒟[do let x ← OptionT.mk mx pure (p x)] {True} = 1 ↔ ∀ o ∈ support mx, ∃ (x : α), o = some x ∧ p x

A wrapped optional oracle computation has a probability-one event exactly when every structurally reachable output is a present value satisfying the event.

theorem OracleComp.OptionT.prEvent_mk_eq_zero_iff {ι : Type u} {spec : OracleSpec ι} [(t : ι) → MeasurableSpace (spec.Range t)] [∀ (t : ι), DiscreteMeasurableSpace (spec.Range t)] [spec.IsUniformMeasureSpec] {α : Type} (mx : OracleComp spec (Option α)) (p : α → Prop) : 𝒟[do let x ← OptionT.mk mx pure (p x)] {True} = 0 ↔ ∀ (x : α), some x ∈ support mx → ¬p x

A wrapped optional oracle computation has a probability-zero event exactly when no structurally reachable present value satisfies the event.

theorem OracleComp.OptionT.prEvent_mk_pos_iff {ι : Type u} {spec : OracleSpec ι} [(t : ι) → MeasurableSpace (spec.Range t)] [∀ (t : ι), DiscreteMeasurableSpace (spec.Range t)] [spec.IsUniformMeasureSpec] {α : Type} (mx : OracleComp spec (Option α)) (p : α → Prop) : 0 < 𝒟[do let x ← OptionT.mk mx pure (p x)] {True} ↔ ∃ (x : α), some x ∈ support mx ∧ p x

A wrapped optional oracle computation has a positive-probability event exactly when some structurally reachable present value satisfies the event.

theorem OracleComp.OptionT.isProbabilityMeasure_mk_iff {ι : Type u} {spec : OracleSpec ι} [(t : ι) → MeasurableSpace (spec.Range t)] [∀ (t : ι), DiscreteMeasurableSpace (spec.Range t)] [spec.IsUniformMeasureSpec] {α : Type} (mx : OracleComp spec (Option α)) [MeasurableSpace α] [DiscreteMeasurableSpace α] : MeasureTheory.IsProbabilityMeasure 𝒟[OptionT.mk mx] ↔ none ∉ support mx

A wrapped optional oracle computation is lossless exactly when none is unreachable.