OAI/NumberTheory/Ostmann/Characters/LogCutoffPolynomial.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.log_lipschitz_on_positive_ray line 10
2. def OAI.Ostmann.positiveLogCutoff line 32
3. def OAI.Ostmann.logCutoffPolynomialFactor line 37

   Source documentation

   The center appears in the lower endpoint and its reciprocal Lipschitz constant. These cancel in the total variation budget.

   noncomputable def logCutoffPolynomialFactor (P : Polynomial ℝ) (φ : ℝ → ℝ)
       (G B D : ℝ) (hB : 0 ≤ B) (hD : 0 ≤ D)
       (hφ : ∀ x, |φ x| ≤ B) (hlip : ∀ x y, |φ x - φ y| ≤ D * |x - y|) :
       ClippedPolynomialFactor where
   …

   Mentions: OAI.Ostmann.ClippedPolynomialFactor

4. theorem OAI.Ostmann.logCutoffPolynomialFactor_value line 62

   Source documentation

   Clipping changes no node factor, including nonpositive inserted values and both boundary points of the compact logarithmic cutoff.

   theorem logCutoffPolynomialFactor_value (P : Polynomial ℝ) (φ : ℝ → ℝ)
       (G 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) (z : ℝ) :
       (logCutoffPolynomialFactor P φ G B D hB hD hφ hlip).value z =
         (positiveLogCutoff φ G (P.eval z) : ℂ) := by
   …

   Mentions: OAI.Ostmann.logCutoffPolynomialFactor, OAI.Ostmann.positiveLogCutoff

5. theorem OAI.Ostmann.logCutoffPolynomialFactor_budget line 102

   Source documentation

   No large-center cost occurs in a logarithmic node cutoff's variation.

   theorem logCutoffPolynomialFactor_budget (P : Polynomial ℝ) (φ : ℝ → ℝ)
       (G B D : ℝ) (hB : 0 ≤ B) (hD : 0 ≤ D)
       (hφ : ∀ x, |φ x| ≤ B) (hlip : ∀ x y, |φ x - φ y| ≤ D * |x - y|) :
       let f := logCutoffPolynomialFactor P φ G B D hB hD hφ hlip
   …

   Mentions: OAI.Ostmann.logCutoffPolynomialFactor