OAI/NumberTheory/Ostmann/Construction/GiantOuterFactors.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.onePolynomialFactor line 11
2. theorem OAI.Ostmann.onePolynomialFactor_polynomial line 24
3. def OAI.Ostmann.giantOuterFactors line 26
4. def OAI.Ostmann.giantOuterScalar line 34
5. theorem OAI.Ostmann.giantOuterFactors_value line 38

   Source documentation

   Both actual cutoff priors are retained. In the diagonal environment the remaining factor is precisely exp(G_R)/R, including all off-support zeros.

   theorem giantOuterFactors_value (L R : Polynomial ℝ) (φ : ℝ → ℝ)
       (Jleft Jright B D : ℝ) (hB : 0 ≤ B) (hD : 0 ≤ D)
       (hφ : ∀ x, |φ x| ≤ B) (hlip : ∀ x y, |φ x - φ y| ≤ D * |x - y|)
       (hout : ∀ x, 1 ≤ |x| → φ x = 0) (diagonal : Bool) (x : ℝ) :
       (giantOuterScalar diagonal : ℂ) *
         smoothPolynomialWeight (giantOuterFactors L R φ Jleft Jright B D hB hD hφ hlip diagonal) x =
           (positiveLogCutoff φ Jleft (L.eval x) : ℂ) * (positiveLogCutoff φ Jright (R.eval x) : ℂ) *
             (if diagonal then ((Real.exp Jright / R.eval x : ℝ) : ℂ) else 1) := by
   …

   Mentions: OAI.Ostmann.giantOuterScalar, OAI.Ostmann.smoothPolynomialWeight, OAI.Ostmann.giantOuterFactors, OAI.Ostmann.positiveLogCutoff

6. theorem OAI.Ostmann.giantOuterFactors_budget line 64