A single normalized hard instance makes finite-horizon randomized success arbitrarily unlikely.
theorem
V7.Stage7StrictRandomizedExpected.hard_causalTrace_eq_affine_of_left
{Ω : Type u_1}
[MeasurableSpace Ω]
(method : RandomizedStrictLocalMethod Ω)
(eps H : ℝ)
(x0 : StrictPoint)
(ω : Ω)
(N : ℕ)
(hleft : ∀ obs ∈ causalTrace method x0 (strictAffineOracle eps x0) N ω, obs.point 0 - x0 0 < H)
:
causalTrace method x0 (Stage6StrictDeterministic.hardOracle eps x0 H) N ω = causalTrace method x0 (strictAffineOracle eps x0) N ω
theorem
V7.Stage7StrictRandomizedExpected.hardGradientMagnitude_measurable
(eps : ℝ)
(x0 : StrictPoint)
(H : ℝ)
:
Measurable fun (x : StrictPoint) => |(Stage6StrictDeterministic.hardOracle eps x0 H).gradient x 0|
theorem
V7.Stage7StrictRandomizedExpected.causalTrace_coordinate_measurable
{Ω : Type u_1}
[MeasurableSpace Ω]
(method : RandomizedStrictLocalMethod Ω)
(x0 : StrictPoint)
(oracle : PairOracle 1)
(hobserve : Measurable (O3.PairOracle.observe oracle))
(n k : ℕ)
(hk : k < n)
:
Measurable fun (ω : Ω) => (causalTrace method x0 oracle n ω)[k]
theorem
V7.Stage7StrictRandomizedExpected.querySuccessEvent_measurable
{Ω : Type u_1}
[MeasurableSpace Ω]
(method : RandomizedStrictLocalMethod Ω)
(x0 : StrictPoint)
(oracle : PairOracle 1)
(hobserve : Measurable (O3.PairOracle.observe oracle))
(hgrad : Measurable fun (x : StrictPoint) => |oracle.gradient x 0|)
(eps : ℝ)
(heps : ∀ (ω : Ω), (method.run ω).eps = eps)
(n : ℕ)
:
theorem
V7.Stage7StrictRandomizedExpected.hardSuccessEvent_measurable
{Ω : Type u_1}
[MeasurableSpace Ω]
(method : RandomizedStrictLocalMethod Ω)
(x0 : StrictPoint)
(eps H : ℝ)
(heps : ∀ (ω : Ω), (method.run ω).eps = eps)
(N : ℕ)
:
MeasurableSet
{ω : Ω | StrictSuccessThrough (method.run ω) (Stage6StrictDeterministic.hardOracle eps x0 H)
(causalTrace method x0 (Stage6StrictDeterministic.hardOracle eps x0 H) N ω) N}
theorem
V7.Stage7StrictRandomizedExpected.success_impossible_on_bounded_affine_event
{Ω : 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) ∧ (method.run ω).output N (causalTrace method x0 (strictAffineOracle eps x0) N ω) 0 - x0 0 < H)
:
¬StrictSuccessThrough (method.run ω) (Stage6StrictDeterministic.hardOracle eps x0 H)
(causalTrace method x0 (Stage6StrictDeterministic.hardOracle eps x0 H) N ω) N
theorem
V7.Stage7StrictRandomizedExpected.probability_success_le_delta
{Ω : Type u_1}
[MeasurableSpace Ω]
(μ : MeasureTheory.Measure Ω)
[MeasureTheory.IsProbabilityMeasure μ]
{good success : Set Ω}
(hgood : MeasurableSet good)
(hsubset : success ⊆ goodᶜ)
{delta : ℝ}
(hdelta1 : delta < 1)
(hmass : ENNReal.ofReal (1 - delta) ≤ μ good)
: