A persistent query gap and existence of a global minimizer for the completed hard objective.

noncomputable def V7.Stage5AboveTwoLowerS5A2Envelope.adversarialPoint {p : ℝ} {d T : ℕ} (data : LowerCompletionData p d T) : Point d

The comparison point with negative signed separation on each selected coordinate.

Equations

• V7.Stage5AboveTwoLowerS5A2Envelope.adversarialPoint data = ∑ i ∈ Finset.range T, (-data.Delta * data.xi i) • V7.Stage5AboveTwoLowerS5A2Envelope.coordinateUnit (data.sigma i)

theorem V7.Stage5AboveTwoLowerS5A2Envelope.sigma_injective_below {p : ℝ} {d T : ℕ} (data : LowerCompletionData p d T) (hsteps : ∀ t < T, ∀ s < t, data.sigma s ≠ data.sigma t) : Set.InjOn data.sigma {i : ℕ | i < T}

theorem V7.Stage5AboveTwoLowerS5A2Envelope.adversarialPoint_at_used {p : ℝ} {d T : ℕ} (data : LowerCompletionData p d T) (hsteps : ∀ t < T, ∀ s < t, data.sigma s ≠ data.sigma t) {i : ℕ} (hi : i < T) : adversarialPoint data (data.sigma i) = -data.Delta * data.xi i

theorem V7.Stage5AboveTwoLowerS5A2Envelope.adversarialPoint_at_unused {p : ℝ} {d T : ℕ} (data : LowerCompletionData p d T) {j : Fin d} (hj : j ∉ Finset.image data.sigma (Finset.range T)) : adversarialPoint data j = 0

theorem V7.Stage5AboveTwoLowerS5A2Envelope.abs_adversarialPoint_at_used {p : ℝ} {d T : ℕ} (data : LowerCompletionData p d T) (hDelta : 0 ≤ data.Delta) (hsteps : ∀ t < T, (∀ s < t, data.sigma s ≠ data.sigma t) ∧ (data.xi t = 1 ∨ data.xi t = -1)) {i : ℕ} (hi : i < T) : |adversarialPoint data (data.sigma i)| = data.Delta

theorem V7.Stage5AboveTwoLowerS5A2Envelope.lpPower_adversarialPoint {p : ℝ} {d T : ℕ} (data : LowerCompletionData p d T) (hp : 0 < p) (hDelta : 0 ≤ data.Delta) (hsteps : ∀ t < T, (∀ s < t, data.sigma s ≠ data.sigma t) ∧ (data.xi t = 1 ∨ data.xi t = -1)) : O3.lpPower p (adversarialPoint data) = ↑T * data.Delta ^ p

theorem V7.Stage5AboveTwoLowerS5A2Envelope.lpNorm_adversarialPoint_eq_one {p : ℝ} {d T : ℕ} (data : LowerCompletionData p d T) (hp : 0 < p) (hT : 1 ≤ T) (hDelta : data.Delta = ↑T ^ (-1 / p)) (hsteps : ∀ t < T, (∀ s < t, data.sigma s ≠ data.sigma t) ∧ (data.xi t = 1 ∨ data.xi t = -1)) : lpNorm p (adversarialPoint data) = 1

theorem V7.Stage5AboveTwoLowerS5A2Envelope.partialH_final_adversarialPoint_le {p : ℝ} {d T : ℕ} (data : LowerCompletionData p d T) (hp : 0 < p) (hT : 1 ≤ T) (hdelta : 0 < data.delta) (hDelta : data.Delta = ↑T ^ (-1 / p)) (hsteps : ∀ t < T, (∀ s < t, data.sigma s ≠ data.sigma t) ∧ (data.xi t = 1 ∨ data.xi t = -1) ∧ ResistingMaximumAt data t ∧ ∀ (x : Point d), data.partialH t x = max (data.partialG t x / 2) (lpNorm p x - 3 / 2)) : data.partialH (T - 1) (adversarialPoint data) ≤ -data.Delta / 2

theorem V7.Stage5AboveTwoLowerS5A2Envelope.partialH_query_lower {p : ℝ} {d T : ℕ} (data : LowerCompletionData p d T) {t : ℕ} (hstep : (data.xi t = 1 ∨ data.xi t = -1) ∧ data.xi t * data.queries t (data.sigma t) = |data.queries t (data.sigma t)| ∧ ResistingMaximumAt data t ∧ ∀ (x : Point d), data.partialH t x = max (data.partialG t x / 2) (lpNorm p x - 3 / 2)) : -↑t * data.delta / 2 ≤ data.partialH t (data.queries t)

theorem V7.Stage5AboveTwoLowerS5A2Envelope.exists_global_minimizer_of_coercive_lp {d : ℕ} {f : Point d → ℝ} {p : ℝ} (hp : 1 ≤ p) (hcontinuous : Continuous f) (hcoercive : IsCoerciveLp p f) : ∃ (minimizer : Point d), ∀ (x : Point d), f minimizer ≤ f x

Finite-dimensional continuous coercive functions attain a global minimum. The proof is the compact sublevel-ball reduction needed by the frozen carrier.

theorem V7.Stage5AboveTwoLowerS5A2Envelope.lower_gap_constant_identity {p Delta chi delta beta M : ℝ} {T : ℕ} (hp : 0 < p) (hT : 1 ≤ T) (hM : 0 < M) (hDelta : Delta = ↑T ^ (-1 / p)) (hdelta : delta = Delta / (2 * ↑T)) (hchi : chi = delta / 2) (hbeta : beta = chi / M) : beta * Delta / 4 = 1 / (16 * M * ↑T ^ (1 + 2 / p))

theorem V7.aboveLowerQueryGap : AboveLowerQueryGapStatement

Frozen S5-C: coercive attainment and the exact chronological query gap.