The normalized resisting construction yields the physical known-parameter query lower bound.
theorem
V7.Stage5AboveTwoLowerS5F.physical_query_gradient
{p : ℝ}
{d T : ℕ}
(algorithm : DeterministicExactPairAlgorithm d)
(hp : 2 < p)
(hd : 2 ≤ d)
(hT : 1 ≤ T)
(hTd : T ≤ d)
(x0 : Point d)
{L R rT : ℝ}
(hL : 0 < L)
(hR : 0 < R)
(hrT : 0 < rT)
(hrTupper : rT < 4)
{t : ℕ}
(ht : t < T)
:
have normAlg := normalizedAdversaryAlgorithm x0 L R rT algorithm;
have data := unitObjectiveData p d T normAlg hT hTd;
lpNorm (conjugateExponent p)
((physicalOracle x0 L R rT data.completedOracle).gradient (physicalForward x0 R rT (data.queries t))) ≥ L * R / (512 * Stage5AboveTwoLowerS5A2Envelope.repairMpd p d * ↑T ^ (1 + 2 / p))
theorem
V7.Stage5AboveTwoLowerS5F.physical_charged_run
{p : ℝ}
{d T : ℕ}
(algorithm : DeterministicExactPairAlgorithm d)
(hp : 2 < p)
(hd : 2 ≤ d)
(hT : 1 ≤ T)
(hTd : T ≤ d)
(x0 : Point d)
{L R rT : ℝ}
(hR : 0 < R)
(hrT : 0 < rT)
:
have normAlg := normalizedAdversaryAlgorithm x0 L R rT algorithm;
have data := unitObjectiveData p d T normAlg hT hTd;
have trace := physicalTrace x0 L R rT (unitTrace p d T normAlg hT hTd);
ChargedKnownParameterRun algorithm x0 (physicalOracle x0 L R rT data.completedOracle) trace