Documentation
LeanPool
.
ParameterFreeGradient
.
V7
.
Proofs
.
Stage3BelowTwo
.
Primal
Search
return to top
source
Imports
Init
LeanPool.ParameterFreeGradient.O3.Stage3Descent
LeanPool.ParameterFreeGradient.V7.Proofs.ResidualAlgebra
LeanPool.ParameterFreeGradient.V7.Proofs.Stage3BelowTwo.Geometry
Imported by
V7
.
Stage3BelowTwo
.
belowPrimal
V7
.
belowPrimal
The below-two primal potential identity and terminal objective-gap bound.
source
theorem
V7
.
Stage3BelowTwo
.
belowPrimal
:
BelowPrimalStatement
source
theorem
V7
.
belowPrimal
:
BelowPrimalStatement