Aggregate a bounded determinant expansion
ProvedOAI.PiExponent.LiteralAnalytic.actual_minor_bound_from_expansionnumber-theoryopenai-pi-exponent-017
Aggregate a finite determinant expansion using a term-count bound and a common exponential bound on its summands. The definition of analyticRemainder converts the count factor into the claimed exponent.
Preamble
import Definitions.Def_OAI_NumberTheory_PiExponent_Analysis_AnalyticAggregate_RemainderData open scoped BigOperators Topology open Filter open OAI.PiExponent OAI.PiExponent.DeterminantContradiction open OAI.PiExponent.LiteralAnalytic
Formal statement
theorem OAI.PiExponent.LiteralAnalytic.actual_minor_bound_from_expansion {nu : ℝ} (d : FixedData nu) (hnu : 0 ≤ nu) {H : ℝ} (hH : 0 < H) (selection : Row d H → Column d H) (N : ℕ) (terms : Fin N → ℂ) (hexp : (actualMinor d H selection).det = ∑ i, terms i) (hcount : (N : ℝ) ≤ Real.exp ((actualRowCount d H : ℝ) * Real.log (translationTermCount d.m d.v0 H : ℝ))) (hterms : ∀ i, ‖terms i‖ ≤ Real.exp (((actualRowCount d H : ℝ) * H) * (d.analyticError + Collision.collisionRemainder (actualRowCount d H) H + max (-collisionRate d H) (-nu * ((d.base.A : ℝ) * (1 - d.base.eta) - actualMean d H))))) : ‖(actualMinor d H selection).det‖ ≤ Real.exp (((actualRowCount d H : ℝ) * H) * (d.analyticError + analyticRemainder d H + max (-collisionRate d H) (-nu * ((d.base.A : ℝ) * (1 - d.base.eta) - actualMean d H)))) := by sorrySource