The normalized completed resisting oracle is a certified positive smooth optimization instance.
theorem
V7.Stage5AboveTwoLowerS5F.unitCompleted_smooth
{p : ℝ}
{d T : ℕ}
(algorithm : DeterministicExactPairAlgorithm d)
(hp : 2 < p)
(hd : 2 ≤ d)
(hT : 1 ≤ T)
(hTd : T ≤ d)
:
IsLpSmooth p 1 (unitObjectiveData p d T algorithm hT hTd).completedOracle
noncomputable def
V7.Stage5AboveTwoLowerS5F.unitPositiveInstance
{p : ℝ}
{d T : ℕ}
(algorithm : DeterministicExactPairAlgorithm d)
(hp : 2 < p)
(hd : 2 ≤ d)
(hT : 1 ≤ T)
(hTd : T ≤ d)
:
PositiveInstance p d 0
The normalized completed resisting oracle certified as a positive optimization instance.
Equations
- One or more equations did not get rendered due to their size.