OAI/Algebra/DepthFive/ActualWeightParameters.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem335.LowerParameters.exists_weightParameters_cutoff line 13

   Source documentation

   All hypotheses of the circuit weight estimate hold simultaneously for the actual integer and analytic parameters beyond one uniform threshold.

   theorem exists_weightParameters_cutoff :
       ∃ n₀ : ℕ, ∀ n : ℕ, n₀ ≤ n → WeightParameters n (s n : ℝ) (q n) := by
   …

   Mentions: OAI.Problem335.WeightParameters, OAI.Problem335.LowerParameters.s, OAI.Problem335.LowerParameters.q

2. theorem OAI.Problem335.LowerParameters.eventually_weightParameters line 32

   Source documentation

   Filter form of the actual-parameter specialization, for final asymptotic assembly.

   theorem eventually_weightParameters :
       ∀ᶠ n : ℕ in Filter.atTop, WeightParameters n (s n : ℝ) (q n) :=
   …

   Mentions: OAI.Problem335.WeightParameters, OAI.Problem335.LowerParameters.s, OAI.Problem335.LowerParameters.q