Measure-valued oracle specifications

An oracle specification assigns a probability measure to each query's response type. A uniform specification identifies each chosen response measure with the uniform measure on its response type; this is a proposition about the chosen measures, and finiteness and inhabitedness of the response types follow from it rather than being carried as data. These certificates are explicit: finiteness alone does not select a probabilistic interpretation.

@[instance_reducible]

instance OracleSpec.addRangeMeasurableSpace {ι : Type u} {spec : OracleSpec ι} {ι' : Type u_1} (spec' : OracleSpec ι') [(t : ι) → MeasurableSpace (spec.Range t)] [(t : ι') → MeasurableSpace (spec'.Range t)] (t : (spec + spec').Domain) : MeasurableSpace ((spec + spec').Range t)

Combined signatures retain each summand's chosen answer measurable space.

instance OracleSpec.addRangeDiscreteMeasurableSpace {ι : Type u} {spec : OracleSpec ι} {ι' : Type u_1} (spec' : OracleSpec ι') [(t : ι) → MeasurableSpace (spec.Range t)] [(t : ι') → MeasurableSpace (spec'.Range t)] [∀ (t : ι), DiscreteMeasurableSpace (spec.Range t)] [∀ (t : ι'), DiscreteMeasurableSpace (spec'.Range t)] (t : (spec + spec').Domain) : DiscreteMeasurableSpace ((spec + spec').Range t)

Discrete answer spaces are preserved by combining signatures.

@[reducible, inline]

abbrev OracleSpec.IsMeasureSpec {ι : Type u} (spec : OracleSpec ι) [(t : ι) → MeasurableSpace (spec.Range t)] : Type (max v u)

A measure-valued response distribution for each query in an oracle specification.

@[reducible, inline]

abbrev OracleSpec.IsMeasureSpec.toMeasure {ι : Type u} {spec : OracleSpec ι} [(t : ι) → MeasurableSpace (spec.Range t)] [spec.IsMeasureSpec] (t : spec.Domain) : MeasureTheory.Measure (spec.Range t)

The probability measure assigned to the response of query t.

instance OracleSpec.IsMeasureSpec.isProbabilityMeasure_toMeasure {ι : Type u} {spec : OracleSpec ι} [(t : ι) → MeasurableSpace (spec.Range t)] [spec.IsMeasureSpec] (t : spec.Domain) : MeasureTheory.IsProbabilityMeasure (toMeasure t)

Each response measure is a probability measure. This restates the polynomial-functor instance at the oracle API, whose response types are spec.Range t rather than spec.toPFunctor.B t, so that instance search finds it for oracle goals.

class OracleSpec.IsUniformMeasureSpec {ι : Type u} (spec : OracleSpec ι) [(t : ι) → MeasurableSpace (spec.Range t)] [∀ (t : ι), DiscreteMeasurableSpace (spec.Range t)] extends spec.toPFunctor.IsMeasureSpec : Type (max u v)

A chosen measure interpretation that samples uniformly from each response type.

This is a proposition about the chosen response measures: each one is the uniform measure on its response type. It carries no finiteness or inhabitedness data. uniformOn Set.univ is a probability measure exactly on a finite, nonempty type, which IsMeasureSpec.isProbabilityMeasure records, so IsUniformMeasureSpec.finite_range and IsUniformMeasureSpec.nonempty_range recover both facts. Statements about cardinalities take [Fintype (spec.Range t)] for the queries they mention.

• toMeasure (a : spec.toPFunctor.A) : MeasureTheory.Measure (spec.toPFunctor.B a)
• isProbabilityMeasure (a : spec.toPFunctor.A) : MeasureTheory.IsProbabilityMeasure (toMeasure a)
• toMeasure_eq_uniform (t : spec.toPFunctor.A) : PFunctor.IsMeasureSpec.toMeasure t = ProbabilityTheory.uniformOn Set.univ

  Each query uses the uniform probability measure on its response type.

theorem OracleSpec.IsMeasureSpec.toMeasure_eq_uniformOn {ι : Type u} {spec : OracleSpec ι} [(t : ι) → MeasurableSpace (spec.Range t)] [∀ (t : ι), DiscreteMeasurableSpace (spec.Range t)] [spec.IsUniformMeasureSpec] (t : spec.Domain) : toMeasure t = ProbabilityTheory.uniformOn Set.univ

The response measure exposed by the oracle API is uniform for a uniform specification.

@[reducible]

noncomputable def OracleSpec.IsUniformMeasureSpec.ofFiniteNonempty {ι : Type u} (spec : OracleSpec ι) [∀ (t : ι), Finite (spec.Range t)] [∀ (t : ι), Nonempty (spec.Range t)] [(t : ι) → MeasurableSpace (spec.Range t)] [∀ (t : ι), DiscreteMeasurableSpace (spec.Range t)] : spec.IsUniformMeasureSpec

Select uniform measure semantics for an oracle specification whose response types are finite and nonempty.

@[reducible]

noncomputable instance OracleSpec.IsUniformMeasureSpec.unifSpec : _root_.unifSpec.IsUniformMeasureSpec

Native uniform measure semantics for the finite-range selection oracle.

@[reducible]

noncomputable instance OracleSpec.IsUniformMeasureSpec.coinSpec : _root_.coinSpec.IsUniformMeasureSpec

Native uniform measure semantics for the fair-coin oracle.

theorem OracleSpec.IsUniformMeasureSpec.finite_range {ι : Type u} {spec : OracleSpec ι} [(t : ι) → MeasurableSpace (spec.Range t)] [∀ (t : ι), DiscreteMeasurableSpace (spec.Range t)] [spec.IsUniformMeasureSpec] (t : spec.Domain) : Finite (spec.Range t)

A uniform response measure is a probability measure only on a finite response type.

Not an instance: for a generic spec its conclusion Finite (spec.Range t) would be a candidate for every Finite _ goal.

theorem OracleSpec.IsUniformMeasureSpec.nonempty_range {ι : Type u} {spec : OracleSpec ι} [(t : ι) → MeasurableSpace (spec.Range t)] [∀ (t : ι), DiscreteMeasurableSpace (spec.Range t)] [spec.IsUniformMeasureSpec] (t : spec.Domain) : Nonempty (spec.Range t)

A uniform response measure is a probability measure only on a nonempty response type.

Not an instance, for the reason given at finite_range.

theorem OracleSpec.IsUniformMeasureSpec.toMeasure_singleton_pos {ι : Type u} {spec : OracleSpec ι} [(t : ι) → MeasurableSpace (spec.Range t)] [∀ (t : ι), DiscreteMeasurableSpace (spec.Range t)] [spec.IsUniformMeasureSpec] (t : spec.Domain) (u : spec.Range t) : 0 < (IsMeasureSpec.toMeasure t) {u}

Every response has positive probability under a uniform response measure.

theorem OracleSpec.IsUniformMeasureSpec.toMeasure_singleton {ι : Type u} {spec : OracleSpec ι} [(t : ι) → MeasurableSpace (spec.Range t)] [∀ (t : ι), DiscreteMeasurableSpace (spec.Range t)] [spec.IsUniformMeasureSpec] (t : spec.Domain) [Fintype (spec.Range t)] (u : spec.Range t) : (IsMeasureSpec.toMeasure t) {u} = (↑(Fintype.card (spec.Range t)))⁻¹

On a finite response type, each response has probability the inverse cardinality.

@[reducible]

noncomputable instance OracleSpec.IsUniformMeasureSpec.add {ι : Type u} {spec : OracleSpec ι} {ι' : Type u_1} (spec' : OracleSpec ι') [(t : ι) → MeasurableSpace (spec.Range t)] [(t : ι') → MeasurableSpace (spec'.Range t)] [∀ (t : ι), DiscreteMeasurableSpace (spec.Range t)] [∀ (t : ι'), DiscreteMeasurableSpace (spec'.Range t)] [spec.IsUniformMeasureSpec] [spec'.IsUniformMeasureSpec] : (spec + spec').IsUniformMeasureSpec

Combining uniform specifications preserves each configured answer measure.

@[simp]

theorem OracleComp.evalDist_liftM_query {ι : Type u} {spec : OracleSpec ι} [(t : ι) → MeasurableSpace (spec.Range t)] [spec.IsMeasureSpec] (t : spec.Domain) : 𝒟[liftM (OracleSpec.query t)] = OracleSpec.IsMeasureSpec.toMeasure t

Lifting a primitive query denotes its configured answer measure.

theorem OracleComp.evalDist_query {ι : Type u} {spec : OracleSpec ι} [(t : ι) → MeasurableSpace (spec.Range t)] [spec.IsMeasureSpec] (t : spec.Domain) : 𝒟[query t] = OracleSpec.IsMeasureSpec.toMeasure t

A single oracle query denotes its configured answer measure.

theorem OracleComp.evalDist_query_uniform {ι : Type u} {spec : OracleSpec ι} [(t : ι) → MeasurableSpace (spec.Range t)] [∀ (t : ι), DiscreteMeasurableSpace (spec.Range t)] [spec.IsUniformMeasureSpec] (t : spec.Domain) : 𝒟[query t] = ProbabilityTheory.uniformOn Set.univ

A query in a uniform measure specification has the uniform response measure.

theorem OracleComp.evalDist_apply_univ_eq_one {ι : Type u} {spec : OracleSpec ι} [(t : ι) → MeasurableSpace (spec.Range t)] [∀ (t : ι), DiscreteMeasurableSpace (spec.Range t)] [spec.IsMeasureSpec] {α : Type v} [MeasurableSpace α] (mx : OracleComp spec α) : 𝒟[mx] Set.univ = 1

A program over discrete, lossless oracle responses has total output mass one.

@[simp]

theorem OracleComp.evalDist_bind_const {ι : Type u} {spec : OracleSpec ι} [(t : ι) → MeasurableSpace (spec.Range t)] [∀ (t : ι), DiscreteMeasurableSpace (spec.Range t)] [spec.IsMeasureSpec] {α β : Type v} [MeasurableSpace β] (mx : OracleComp spec α) (my : OracleComp spec β) : 𝒟[do let _ ← mx my] = 𝒟[my]

Discarding the result of a lossless oracle computation leaves the continuation's output measure unchanged. The discarded result type needs no ambient measurable-space instance.

@[simp]

theorem OracleComp.evalDist_map_const {ι : Type u} {spec : OracleSpec ι} [(t : ι) → MeasurableSpace (spec.Range t)] [∀ (t : ι), DiscreteMeasurableSpace (spec.Range t)] [spec.IsMeasureSpec] {α β : Type v} [MeasurableSpace β] (mx : OracleComp spec α) (b : β) : 𝒟[(fun (x : α) => b) <$> mx] = MeasureTheory.Measure.dirac b

A constant output map on a lossless oracle program is a Dirac measure. No measurable-space instance on the discarded result type is needed.