Measurable finite displacement bounds admit a deterministic threshold with high probability.

theorem V7.Stage7StrictRandomizedExpected.traceDisplacementBound_append_singleton (x0 : StrictPoint) (trace : StrictTranscript) (obs : StrictObservation) : Stage6StrictDeterministic.traceDisplacementBound x0 (trace ++ [obs]) = max (Stage6StrictDeterministic.traceDisplacementBound x0 trace) (obs.point 0 - x0 0)

theorem V7.Stage7StrictRandomizedExpected.traceDisplacementBound_lt_iff (x0 : StrictPoint) (trace : StrictTranscript) {H : ℝ} (hH : 0 < H) : Stage6StrictDeterministic.traceDisplacementBound x0 trace < H ↔ ∀ obs ∈ trace, obs.point 0 - x0 0 < H

theorem V7.Stage7StrictRandomizedExpected.causalTraceDisplacementBound_measurable {Ω : Type u_1} [MeasurableSpace Ω] (method : RandomizedStrictLocalMethod Ω) (x0 : StrictPoint) (oracle : PairOracle 1) (hobserve : Measurable (O3.PairOracle.observe oracle)) (n : ℕ) : Measurable fun (ω : Ω) => Stage6StrictDeterministic.traceDisplacementBound x0 (causalTrace method x0 oracle n ω)

noncomputable def V7.Stage7StrictRandomizedExpected.finiteDisplacementBound {Ω : Type u_1} [MeasurableSpace Ω] (method : RandomizedStrictLocalMethod Ω) (x0 : StrictPoint) (oracle : PairOracle 1) (N : ℕ) (ω : Ω) : ℝ

Maximum of zero, all affine-query displacements, and the horizon output.

Equations

• One or more equations did not get rendered due to their size.

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

theorem V7.Stage7StrictRandomizedExpected.finiteDisplacementBound_lt_iff {Ω : Type u_1} [MeasurableSpace Ω] (method : RandomizedStrictLocalMethod Ω) (x0 : StrictPoint) (oracle : PairOracle 1) (N : ℕ) (ω : Ω) {H : ℝ} (hH : 0 < H) : finiteDisplacementBound method x0 oracle N ω < H ↔ (∀ obs ∈ causalTrace method x0 oracle N ω, obs.point 0 - x0 0 < H) ∧ (method.run ω).output N (causalTrace method x0 oracle N ω) 0 - x0 0 < H

theorem V7.Stage7StrictRandomizedExpected.boundedDisplacementEvent_measurable {Ω : Type u_1} [MeasurableSpace Ω] (method : RandomizedStrictLocalMethod Ω) (x0 : StrictPoint) (oracle : PairOracle 1) (hobserve : Measurable (O3.PairOracle.observe oracle)) (N : ℕ) {H : ℝ} (hH : 0 < H) : MeasurableSet {ω : Ω | (∀ obs ∈ causalTrace method x0 oracle N ω, obs.point 0 - x0 0 < H) ∧ (method.run ω).output N (causalTrace method x0 oracle N ω) 0 - x0 0 < H}

theorem V7.Stage7StrictRandomizedExpected.exists_deterministic_threshold {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (M : Ω → ℝ) (hM : Measurable M) {delta : ℝ} (hdelta0 : 0 < delta) : ∃ (H : ℝ), 0 < H ∧ ENNReal.ofReal (1 - delta) ≤ μ {ω : Ω | M ω < H}

A finite measurable real random variable admits one deterministic positive threshold carrying any prescribed probability strictly below one.