Joint measurability and exactness of randomized causal queries, transcripts, and outputs.

theorem V7.Stage7StrictRandomizedExpected.measurable_strictTranscript_of_fixedLength {Ω : Type u_1} [MeasurableSpace Ω] {trace : Ω → StrictTranscript} {n : ℕ} (hlen : ∀ (ω : Ω), List.length (trace ω) = n) (hcoord : ∀ (k : ℕ) (hk : k < n), Measurable fun (ω : Ω) => (trace ω)[k]) : Measurable trace

A fixed-length transcript is measurable for the frozen cylinder sigma algebra once each of its finitely many coordinates is measurable.

def V7.Stage7StrictRandomizedExpected.causalQuery {Ω : Type u_1} [MeasurableSpace Ω] (method : RandomizedStrictLocalMethod Ω) (x0 : StrictPoint) (ω : Ω) (t : ℕ) (trace : StrictTranscript) : StrictPoint

The query selected by a seed-indexed method after a chronological prefix.

Equations

• V7.Stage7StrictRandomizedExpected.causalQuery method x0 ω t trace = if t = 0 then x0 else (method.run ω).nextQuery trace

noncomputable def V7.Stage7StrictRandomizedExpected.causalTrace {Ω : Type u_1} [MeasurableSpace Ω] (method : RandomizedStrictLocalMethod Ω) (x0 : StrictPoint) (oracle : PairOracle 1) : ℕ → Ω → StrictTranscript

Exact chronological transcript against one fixed oracle, simultaneously defined for every seed and every finite horizon.

Equations

• One or more equations did not get rendered due to their size.
• V7.Stage7StrictRandomizedExpected.causalTrace method x0 oracle 0 = fun (x : Ω) => []

@[simp]

theorem V7.Stage7StrictRandomizedExpected.causalTrace_zero {Ω : Type u_1} [MeasurableSpace Ω] (method : RandomizedStrictLocalMethod Ω) (x0 : StrictPoint) (oracle : PairOracle 1) (ω : Ω) : causalTrace method x0 oracle 0 ω = []

theorem V7.Stage7StrictRandomizedExpected.causalTrace_succ {Ω : Type u_1} [MeasurableSpace Ω] (method : RandomizedStrictLocalMethod Ω) (x0 : StrictPoint) (oracle : PairOracle 1) (n : ℕ) (ω : Ω) : causalTrace method x0 oracle (n + 1) ω = causalTrace method x0 oracle n ω ++ [O3.PairOracle.observe oracle (causalQuery method x0 ω n (causalTrace method x0 oracle n ω))]

@[simp]

theorem V7.Stage7StrictRandomizedExpected.causalTrace_length {Ω : Type u_1} [MeasurableSpace Ω] (method : RandomizedStrictLocalMethod Ω) (x0 : StrictPoint) (oracle : PairOracle 1) (n : ℕ) (ω : Ω) : List.length (causalTrace method x0 oracle n ω) = n

theorem V7.Stage7StrictRandomizedExpected.causalTrace_take {Ω : Type u_1} [MeasurableSpace Ω] (method : RandomizedStrictLocalMethod Ω) (x0 : StrictPoint) (oracle : PairOracle 1) {m n : ℕ} (hmn : m ≤ n) (ω : Ω) : List.take m (causalTrace method x0 oracle n ω) = causalTrace method x0 oracle m ω

theorem V7.Stage7StrictRandomizedExpected.causalTrace_get {Ω : Type u_1} [MeasurableSpace Ω] (method : RandomizedStrictLocalMethod Ω) (x0 : StrictPoint) (oracle : PairOracle 1) (n t : ℕ) (ht : t < n) (ω : Ω) : List.get (causalTrace method x0 oracle n ω) ⟨t, ⋯⟩ = O3.PairOracle.observe oracle (causalQuery method x0 ω t (causalTrace method x0 oracle t ω))

theorem V7.Stage7StrictRandomizedExpected.causalTrace_exact {Ω : Type u_1} [MeasurableSpace Ω] (method : RandomizedStrictLocalMethod Ω) (x0 : StrictPoint) (oracle : PairOracle 1) (n : ℕ) (ω : Ω) : StrictTranscriptExact oracle (causalTrace method x0 oracle n ω)

Exactness of the generated transcript against its fixed oracle.

theorem V7.Stage7StrictRandomizedExpected.strictAffineObserve_measurable (eps : ℝ) (x0 : StrictPoint) : Measurable (O3.PairOracle.observe (strictAffineOracle eps x0))

theorem V7.Stage7StrictRandomizedExpected.hardObserve_measurable (eps : ℝ) (x0 : StrictPoint) (H : ℝ) : Measurable (O3.PairOracle.observe (Stage6StrictDeterministic.hardOracle eps x0 H))

theorem V7.Stage7StrictRandomizedExpected.causalQuery_measurable {Ω : Type u_1} [MeasurableSpace Ω] (method : RandomizedStrictLocalMethod Ω) (x0 : StrictPoint) (n : ℕ) {trace : Ω → StrictTranscript} (htrace : Measurable trace) : Measurable fun (ω : Ω) => causalQuery method x0 ω n (trace ω)

theorem V7.Stage7StrictRandomizedExpected.causalTrace_measurable {Ω : Type u_1} [MeasurableSpace Ω] (method : RandomizedStrictLocalMethod Ω) (x0 : StrictPoint) (oracle : PairOracle 1) (hobserve : Measurable (O3.PairOracle.observe oracle)) (n : ℕ) : Measurable (causalTrace method x0 oracle n)

Measurability of the complete finite causal recursion, proved directly from the frozen cylinder generators and the joint method fields.

theorem V7.Stage7StrictRandomizedExpected.causalOutput_measurable {Ω : Type u_1} [MeasurableSpace Ω] (method : RandomizedStrictLocalMethod Ω) (N : ℕ) {trace : Ω → StrictTranscript} (htrace : Measurable trace) : Measurable fun (ω : Ω) => (method.run ω).output N (trace ω)

theorem V7.Stage7StrictRandomizedExpected.causalTrace_runConsistent {Ω : Type u_1} [MeasurableSpace Ω] (method : RandomizedStrictLocalMethod Ω) (x0 : StrictPoint) (oracle : PairOracle 1) (hx0 : ∀ (ω : Ω), (method.run ω).x0 = x0) (n : ℕ) (ω : Ω) : StrictRunConsistent (method.run ω) oracle (causalTrace method x0 oracle n ω)