The original analytic aggregate bound for admissible selected minors
ProvedOAI.PiExponent.LiteralAnalytic.analyticAggregatenumber-theoryopenai-pi-exponent-017
For every real and fixed admissible datum , there is an error as . Eventually, every selected minor with nonzero determinant satisfies
Here is the row count, the analytic error parameter, the collision rate, and the fixed-data parameters, and the normalized weighted row mean. The bound is uniform over the original column selections and is precisely the source analytic aggregate statement.
Preamble
import Definitions.Def_OAI_PiExponent_ApproximationDefinitions import Definitions.Def_OAI_NumberTheory_PiExponent_Approximation_DeterminantContradiction_CoreData open OAI.PiExponent OAI.PiExponent.DeterminantContradiction
Formal statement
theorem OAI.PiExponent.LiteralAnalytic.analyticAggregate : AnalyticAggregateStatement := by sorry
Source