Finite-horizon failure probabilities force an unbounded worst-case expected hitting time.

noncomputable def V7.Stage7StrictRandomizedExpected.allHorizonDisplacementBound {Ω : Type u_1} [MeasurableSpace Ω] (method : RandomizedStrictLocalMethod Ω) (x0 : StrictPoint) (eps : ℝ) : ℕ → Ω → ℝ

One finite random bound controlling every affine query through N and every horizon-indexed output from zero through N.

Equations

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

theorem V7.Stage7StrictRandomizedExpected.allHorizonDisplacementBound_measurable {Ω : Type u_1} [MeasurableSpace Ω] (method : RandomizedStrictLocalMethod Ω) (x0 : StrictPoint) (eps : ℝ) (N : ℕ) : Measurable (allHorizonDisplacementBound method x0 eps N)

theorem V7.Stage7StrictRandomizedExpected.allHorizonDisplacementBound_lt_iff {Ω : Type u_1} [MeasurableSpace Ω] (method : RandomizedStrictLocalMethod Ω) (x0 : StrictPoint) (eps : ℝ) (N : ℕ) (ω : Ω) {H : ℝ} (hH : 0 < H) : allHorizonDisplacementBound method x0 eps N ω < H ↔ (∀ obs ∈ causalTrace method x0 (strictAffineOracle eps x0) N ω, obs.point 0 - x0 0 < H) ∧ ∀ m ≤ N, (method.run ω).output m (causalTrace method x0 (strictAffineOracle eps x0) m ω) 0 - x0 0 < H

theorem V7.Stage7StrictRandomizedExpected.allHorizonBoundedEvent_measurable {Ω : Type u_1} [MeasurableSpace Ω] (method : RandomizedStrictLocalMethod Ω) (x0 : StrictPoint) (eps : ℝ) (N : ℕ) {H : ℝ} (hH : 0 < H) : MeasurableSet {ω : Ω | (∀ obs ∈ causalTrace method x0 (strictAffineOracle eps x0) N ω, obs.point 0 - x0 0 < H) ∧ ∀ m ≤ N, (method.run ω).output m (causalTrace method x0 (strictAffineOracle eps x0) m ω) 0 - x0 0 < H}

theorem V7.Stage7StrictRandomizedExpected.no_success_before_of_allHorizonBound {Ω : Type u_1} [MeasurableSpace Ω] (method : RandomizedStrictLocalMethod Ω) (x0 : StrictPoint) (eps H : ℝ) (heps0 : 0 < eps) (heps : ∀ (ω : Ω), (method.run ω).eps = eps) (hx0 : ∀ (ω : Ω), (method.run ω).x0 = x0) (N : ℕ) (ω : Ω) (hgood : (∀ obs ∈ causalTrace method x0 (strictAffineOracle eps x0) N ω, obs.point 0 - x0 0 < H) ∧ ∀ m ≤ N, (method.run ω).output m (causalTrace method x0 (strictAffineOracle eps x0) m ω) 0 - x0 0 < H) (m : ℕ) : m ≤ N → ¬StrictSuccessThrough (method.run ω) (Stage6StrictDeterministic.hardOracle eps x0 H) (causalTrace method x0 (Stage6StrictDeterministic.hardOracle eps x0 H) m ω) m

theorem V7.Stage7StrictRandomizedExpected.strictHittingTime_eq_iInf (method : StrictLocalMethod) (oracle : PairOracle 1) (traces : ℕ → StrictTranscript) : strictHittingTime method oracle traces = ⨅ (N : ℕ), if StrictSuccessThrough method oracle (traces N) N then ↑N else ⊤

The frozen sInf hitting time is the countable infimum of measurable horizon values (finite at successful horizons, top otherwise).

theorem V7.Stage7StrictRandomizedExpected.strictHittingTime_measurable {Ω : Type u_1} [MeasurableSpace Ω] (method : RandomizedStrictLocalMethod Ω) (x0 : StrictPoint) (eps H : ℝ) (heps : ∀ (ω : Ω), (method.run ω).eps = eps) : Measurable fun (ω : Ω) => strictHittingTime (method.run ω) (Stage6StrictDeterministic.hardOracle eps x0 H) fun (N : ℕ) => causalTrace method x0 (Stage6StrictDeterministic.hardOracle eps x0 H) N ω

theorem V7.Stage7StrictRandomizedExpected.hittingTime_gt_of_no_success_before (method : StrictLocalMethod) (oracle : PairOracle 1) (traces : ℕ → StrictTranscript) (N : ℕ) (hfail : ∀ m ≤ N, ¬StrictSuccessThrough method oracle (traces m) m) : ↑N < strictHittingTime method oracle traces

theorem V7.Stage7StrictRandomizedExpected.strictHardInstance_normalized {eps H : ℝ} {x0 : StrictPoint} (heps : 0 < eps) (hH : 0 < H) : StrictNormalizedInstance eps x0 (2 * eps / H) (2 * H) (Stage6StrictDeterministic.hardOracle eps x0 H) (Stage6StrictDeterministic.hardMinimizer x0 H)

theorem V7.Stage7StrictRandomizedExpected.lintegral_lower_bound_of_tail {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) (T : Ω → ENNReal) {N : ℕ} {tail : Set Ω} (htail : MeasurableSet tail) (hpoint : ∀ ω ∈ tail, ↑N ≤ T ω) : ↑N * μ tail ≤ ∫⁻ (ω : Ω), T ω ∂μ

theorem V7.infiniteWorstCaseExpectedHittingTime : InfiniteWorstCaseExpectedHittingTimeStatement