OAI/NumberTheory/Ostmann/Arithmetic/SmoothPolynomialWeight.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Finite products of the smooth factors appearing in a history

Profiles are clipped to their prescribed argument ranges. This leaves their values unchanged on the retained range and requires no continuity of the sharp range indicator; those indicators are separate functions of the root cell.

  1. structure OAI.Ostmann.ClippedPolynomialFactor line 17
  2. def OAI.Ostmann.ClippedPolynomialFactor.value line 31
  3. theorem OAI.Ostmann.ClippedPolynomialFactor.value_of_mem line 34
  4. theorem OAI.Ostmann.ClippedPolynomialFactor.norm_value line 39
  5. theorem OAI.Ostmann.ClippedPolynomialFactor.variation line 43
  6. def OAI.Ostmann.smoothPolynomialWeight line 66
  7. def OAI.Ostmann.smoothPolynomialBudget line 69
  8. theorem OAI.Ostmann.smoothPolynomialBudget_nonneg line 72
  9. theorem OAI.Ostmann.smoothPolynomialWeight_norm line 79
  10. theorem OAI.Ostmann.smoothPolynomialWeight_variation line 88
  11. theorem OAI.Ostmann.smoothPolynomial_reciprocal_variation line 107

    Source documentation

    This is the weight used after the long-prime prior is extended to integers.

    theorem smoothPolynomial_reciprocal_variation {n : ℕ} (F : Fin n → ClippedPolynomialFactor)
    (S : Finset ℝ) (hroots : ∀ i r, r ∈ (F i).polynomial.derivative.roots → r ∈ S)
    (b d : ℝ) (hb : 0 < b) (hd : 0 ≤ d) (N : ℕ)
    (hcode : rootCellCode S b = rootCellCode S (b + d * ((N - 1 : ℕ) : ℝ))) :
    discreteVariation (fun j => Complex.ofReal ((b + d * j)⁻¹) *
      smoothPolynomialWeight F (b + d * j)) N ≤ 2 * b⁻¹ * smoothPolynomialBudget F := by
…

    Mentions: OAI.Ostmann.ClippedPolynomialFactor, OAI.Ostmann.rootCellCode, OAI.Ostmann.discreteVariation, OAI.Ostmann.smoothPolynomialWeight, OAI.Ostmann.smoothPolynomialBudget