The completed resisting objective has a controlled, symmetry-invariant distance to its minimizers.

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

The vector with common signed magnitude on the coordinates used by the resisting construction.

Equations

• V7.Stage5AboveTwoLowerS5A2Envelope.uniformSignedPoint data a = ∑ i ∈ Finset.range T, (a * data.xi i) • V7.Stage5AboveTwoLowerS5A2Envelope.coordinateUnit (data.sigma i)

theorem V7.Stage5AboveTwoLowerS5A2Envelope.uniformSignedPoint_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) (a : ℝ) : uniformSignedPoint data a (data.sigma i) = a * data.xi i

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

theorem V7.Stage5AboveTwoLowerS5A2Envelope.lpPower_uniformSignedPoint {p : ℝ} {d T : ℕ} (data : LowerCompletionData p d T) {r : ℝ} (hr : 0 < r) (hsteps : ∀ t < T, (∀ s < t, data.sigma s ≠ data.sigma t) ∧ (data.xi t = 1 ∨ data.xi t = -1)) (a : ℝ) : O3.lpPower r (uniformSignedPoint data a) = ↑T * |a| ^ r

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

The average of the signed coordinate directions used by the resisting construction.

Equations

• V7.Stage5AboveTwoLowerS5A2Envelope.averageDirection data = V7.Stage5AboveTwoLowerS5A2Envelope.uniformSignedPoint data (1 / ↑T)

theorem V7.Stage5AboveTwoLowerS5A2Envelope.lpNorm_averageDirection {p : ℝ} {d T : ℕ} (data : LowerCompletionData p d T) (hp : 1 < 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 (conjugateExponent p) (averageDirection data) = data.Delta

theorem V7.Stage5AboveTwoLowerS5A2Envelope.real_sum_range_id (T : ℕ) : ∑ i ∈ Finset.range T, ↑i = ↑T * ↑(T - 1) / 2

theorem V7.Stage5AboveTwoLowerS5A2Envelope.pairing_averageDirection {p : ℝ} {d T : ℕ} (data : LowerCompletionData p d T) (hsteps : ∀ t < T, ∀ s < t, data.sigma s ≠ data.sigma t) (x : Point d) : O3.pairing (averageDirection data) x = 1 / ↑T * ∑ i ∈ Finset.range T, data.xi i * x (data.sigma i)

theorem V7.Stage5AboveTwoLowerS5A2Envelope.partialG_final_average_lower {p : ℝ} {d T : ℕ} (data : LowerCompletionData p d T) (hp : 1 < 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) ∧ ResistingMaximumAt data t) (x : Point d) : -data.Delta * lpNorm p x - ↑(T - 1) * data.delta / 2 ≤ data.partialG (T - 1) x

theorem V7.Stage5AboveTwoLowerS5A2Envelope.global_minimizer_norm_ge_half {p : ℝ} {d T : ℕ} (data : LowerObjectiveData p d T) (hp : 2 < p) (hassum : LowerObjectiveAssumptions data) {minimizer : Point d} (hmin : ∀ (x : O3.Vec d), data.completedOracle.value minimizer ≤ data.completedOracle.value x) : 1 / 2 ≤ lpNorm p minimizer

theorem V7.Stage5AboveTwoLowerS5A2Envelope.minimizerDistance_range {p : ℝ} {d T : ℕ} (data : LowerObjectiveData p d T) (hp : 2 < p) (hassum : LowerObjectiveAssumptions data) : 1 / 4 < minimizerDistance p data.completedOracle data.x0 ∧ minimizerDistance p data.completedOracle data.x0 < 4

def V7.Stage5AboveTwoLowerS5A2Envelope.completionSigmaEmbedding {p : ℝ} {d T : ℕ} (data : LowerCompletionData p d T) (hdistinct : ∀ t < T, ∀ s < t, data.sigma s ≠ data.sigma t) : Fin T ↪ Fin d

The embedding of iteration indices into their distinct selected coordinates.

Equations

• V7.Stage5AboveTwoLowerS5A2Envelope.completionSigmaEmbedding data hdistinct = { toFun := fun (i : Fin T) => data.sigma ↑i, inj' := ⋯ }

noncomputable def V7.Stage5AboveTwoLowerS5A2Envelope.completionPerm {p : ℝ} {d T : ℕ} (data₁ data₂ : LowerCompletionData p d T) (hdistinct₁ : ∀ t < T, ∀ s < t, data₁.sigma s ≠ data₁.sigma t) (hdistinct₂ : ∀ t < T, ∀ s < t, data₂.sigma s ≠ data₂.sigma t) : Equiv.Perm (Fin d)

A coordinate permutation matching the selected coordinates of two completions.

Equations

• V7.Stage5AboveTwoLowerS5A2Envelope.completionPerm data₁ data₂ hdistinct₁ hdistinct₂ = Classical.choose ⋯

theorem V7.Stage5AboveTwoLowerS5A2Envelope.completionPerm_spec {p : ℝ} {d T : ℕ} (data₁ data₂ : LowerCompletionData p d T) (hdistinct₁ : ∀ t < T, ∀ s < t, data₁.sigma s ≠ data₁.sigma t) (hdistinct₂ : ∀ t < T, ∀ s < t, data₂.sigma s ≠ data₂.sigma t) (i : Fin T) : (completionPerm data₁ data₂ hdistinct₁ hdistinct₂) (data₁.sigma ↑i) = data₂.sigma ↑i

noncomputable def V7.Stage5AboveTwoLowerS5A2Envelope.completionSign {p : ℝ} {d T : ℕ} (data₁ data₂ : LowerCompletionData p d T) (k : Fin d) : ℝ

The coordinate signs matching two resisting completions, extended by one on unused coordinates.

Equations

• V7.Stage5AboveTwoLowerS5A2Envelope.completionSign data₁ data₂ k = if h : ∃ (i : Fin T), data₂.sigma ↑i = k then data₁.xi ↑(Classical.choose h) * data₂.xi ↑(Classical.choose h) else 1

theorem V7.Stage5AboveTwoLowerS5A2Envelope.completionSign_at_used {p : ℝ} {d T : ℕ} (data₁ data₂ : LowerCompletionData p d T) (hdistinct₂ : ∀ t < T, ∀ s < t, data₂.sigma s ≠ data₂.sigma t) (i : Fin T) : completionSign data₁ data₂ (data₂.sigma ↑i) = data₁.xi ↑i * data₂.xi ↑i

theorem V7.Stage5AboveTwoLowerS5A2Envelope.completionSign_sq {p : ℝ} {d T : ℕ} (data₁ data₂ : LowerCompletionData p d T) (hxi₁ : ∀ i < T, data₁.xi i = 1 ∨ data₁.xi i = -1) (hxi₂ : ∀ i < T, data₂.xi i = 1 ∨ data₂.xi i = -1) (k : Fin d) : completionSign data₁ data₂ k ^ 2 = 1

noncomputable def V7.Stage5AboveTwoLowerS5A2Envelope.completionQ {p : ℝ} {d T : ℕ} (data₁ data₂ : LowerCompletionData p d T) (hdistinct₁ : ∀ t < T, ∀ s < t, data₁.sigma s ≠ data₁.sigma t) (hdistinct₂ : ∀ t < T, ∀ s < t, data₂.sigma s ≠ data₂.sigma t) (x : Point d) : Point d

The signed coordinate permutation transporting one resisting completion to another.

Equations

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

theorem V7.Stage5AboveTwoLowerS5A2Envelope.completionQ_at_used {p : ℝ} {d T : ℕ} (data₁ data₂ : LowerCompletionData p d T) (hdistinct₁ : ∀ t < T, ∀ s < t, data₁.sigma s ≠ data₁.sigma t) (hdistinct₂ : ∀ t < T, ∀ s < t, data₂.sigma s ≠ data₂.sigma t) (x : Point d) (i : Fin T) : completionQ data₁ data₂ hdistinct₁ hdistinct₂ x (data₂.sigma ↑i) = data₁.xi ↑i * data₂.xi ↑i * x (data₁.sigma ↑i)

theorem V7.Stage5AboveTwoLowerS5A2Envelope.completionQ_lpPower {p : ℝ} {d T : ℕ} (data₁ data₂ : LowerCompletionData p d T) (hdistinct₁ : ∀ t < T, ∀ s < t, data₁.sigma s ≠ data₁.sigma t) (hdistinct₂ : ∀ t < T, ∀ s < t, data₂.sigma s ≠ data₂.sigma t) (hxi₁ : ∀ i < T, data₁.xi i = 1 ∨ data₁.xi i = -1) (hxi₂ : ∀ i < T, data₂.xi i = 1 ∨ data₂.xi i = -1) (r : ℝ) (x : Point d) : O3.lpPower r (completionQ data₁ data₂ hdistinct₁ hdistinct₂ x) = O3.lpPower r x

theorem V7.Stage5AboveTwoLowerS5A2Envelope.completionQ_lpNorm {p : ℝ} {d T : ℕ} (data₁ data₂ : LowerCompletionData p d T) (hdistinct₁ : ∀ t < T, ∀ s < t, data₁.sigma s ≠ data₁.sigma t) (hdistinct₂ : ∀ t < T, ∀ s < t, data₂.sigma s ≠ data₂.sigma t) (hxi₁ : ∀ i < T, data₁.xi i = 1 ∨ data₁.xi i = -1) (hxi₂ : ∀ i < T, data₂.xi i = 1 ∨ data₂.xi i = -1) (r : ℝ) (x : Point d) : lpNorm r (completionQ data₁ data₂ hdistinct₁ hdistinct₂ x) = lpNorm r x

theorem V7.Stage5AboveTwoLowerS5A2Envelope.completionQ_pairing {p : ℝ} {d T : ℕ} (data₁ data₂ : LowerCompletionData p d T) (hdistinct₁ : ∀ t < T, ∀ s < t, data₁.sigma s ≠ data₁.sigma t) (hdistinct₂ : ∀ t < T, ∀ s < t, data₂.sigma s ≠ data₂.sigma t) (hxi₁ : ∀ i < T, data₁.xi i = 1 ∨ data₁.xi i = -1) (hxi₂ : ∀ i < T, data₂.xi i = 1 ∨ data₂.xi i = -1) (s x : Point d) : O3.pairing (completionQ data₁ data₂ hdistinct₁ hdistinct₂ s) (completionQ data₁ data₂ hdistinct₁ hdistinct₂ x) = O3.pairing s x

theorem V7.Stage5AboveTwoLowerS5A2Envelope.completionQ_signedLpSymmetry {p : ℝ} {d T : ℕ} (data₁ data₂ : LowerCompletionData p d T) (hdistinct₁ : ∀ t < T, ∀ s < t, data₁.sigma s ≠ data₁.sigma t) (hdistinct₂ : ∀ t < T, ∀ s < t, data₂.sigma s ≠ data₂.sigma t) (hxi₁ : ∀ i < T, data₁.xi i = 1 ∨ data₁.xi i = -1) (hxi₂ : ∀ i < T, data₂.xi i = 1 ∨ data₂.xi i = -1) : SignedLpSymmetry p (completionQ data₁ data₂ hdistinct₁ hdistinct₂) (completionQ data₁ data₂ hdistinct₁ hdistinct₂)

theorem V7.Stage5AboveTwoLowerS5A2Envelope.completion_partialG_eq {p : ℝ} {d T : ℕ} (data₁ data₂ : LowerCompletionData p d T) (hT : 1 ≤ T) (hdelta : data₁.delta = data₂.delta) (hsteps₁ : ∀ t < T, (∀ s < t, data₁.sigma s ≠ data₁.sigma t) ∧ (data₁.xi t = 1 ∨ data₁.xi t = -1) ∧ ResistingMaximumAt data₁ t) (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₂.partialG (T - 1) (completionQ data₁ data₂ ⋯ ⋯ x) = data₁.partialG (T - 1) x

theorem V7.Stage5AboveTwoLowerS5A2Envelope.completion_partialH_eq {p : ℝ} {d T : ℕ} (data₁ data₂ : LowerCompletionData p d T) (hT : 1 ≤ T) (hdelta : data₁.delta = data₂.delta) (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)) (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)) (x : Point d) : data₂.partialH (T - 1) (completionQ data₁ data₂ ⋯ ⋯ x) = data₁.partialH (T - 1) x

theorem V7.Stage5AboveTwoLowerS5A2Envelope.completionQ_surjective {p : ℝ} {d T : ℕ} (data₁ data₂ : LowerCompletionData p d T) (hdistinct₁ : ∀ t < T, ∀ s < t, data₁.sigma s ≠ data₁.sigma t) (hdistinct₂ : ∀ t < T, ∀ s < t, data₂.sigma s ≠ data₂.sigma t) (hxi₁ : ∀ i < T, data₁.xi i = 1 ∨ data₁.xi i = -1) (hxi₂ : ∀ i < T, data₂.xi i = 1 ∨ data₂.xi i = -1) : Function.Surjective (completionQ data₁ data₂ hdistinct₁ hdistinct₂)

theorem V7.Stage5AboveTwoLowerS5A2Envelope.completedValue_completionQ_eq {p : ℝ} {d T : ℕ} (data₁ data₂ : LowerObjectiveData p d T) (hp : 2 < p) (hassum₁ : LowerObjectiveAssumptions data₁) (hassum₂ : LowerObjectiveAssumptions data₂) (hkernelEq : data₁.kernel = data₂.kernel) (x : Point d) : let base₁ := data₁.toLowerCompletionData; let base₂ := data₂.toLowerCompletionData; have Q := completionQ base₁ base₂ ⋯ ⋯; data₂.completedOracle.value (Q x) = data₁.completedOracle.value x

theorem V7.Stage5AboveTwoLowerS5A2Envelope.completion_minimizerDistance_eq {p : ℝ} {d T : ℕ} (data₁ data₂ : LowerObjectiveData p d T) (hp : 2 < p) (hassum₁ : LowerObjectiveAssumptions data₁) (hassum₂ : LowerObjectiveAssumptions data₂) (hkernelEq : data₁.kernel = data₂.kernel) : minimizerDistance p data₁.completedOracle data₁.x0 = minimizerDistance p data₂.completedOracle data₂.x0

theorem V7.aboveLowerOptimizerRadius : AboveLowerOptimizerRadiusStatement

Frozen S5-E: the optimizer radius is independent of the chronological completion because every completion is a signed-permutation isometric image of every other one.