Uniform oracle semantics agreement #
A finite uniform oracle's measure-valued and probability-mass-valued answer interpretations assign the same measure to each response type. The agreement certificate lets a direct measure fold retain the discrete probability bridges.
@[instance_reducible, instance 50]
noncomputable instance
OracleSpec.instIsUniformMeasureSpecOfIsUniformSpec
{ι : Type u}
{spec : OracleSpec ι}
[(t : ι) → MeasurableSpace (spec.Range t)]
[∀ (t : ι), DiscreteMeasurableSpace (spec.Range t)]
[spec.IsUniformSpec]
:
spec.IsUniformMeasureSpec
The uniform measure interpretation induced by an existing uniform oracle specification.
instance
OracleSpec.IsUniformMeasureSpec.instCompatible
{ι : Type u}
{spec : OracleSpec ι}
[(t : ι) → MeasurableSpace (spec.Range t)]
[∀ (t : ι), DiscreteMeasurableSpace (spec.Range t)]
[spec.IsUniformSpec]
[spec.IsUniformMeasureSpec]
:
Uniform measure and mass-function interpretations agree on every oracle answer type.