GiantReciprocalFactor.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The normalized reciprocal giant factor in the diagonal multiplier

def OAI.Ostmann.giantReciprocalFactor line 12
Source documentation
Reuse the existing reciprocal factor after scaling the polynomial by its lower cell endpoint. The variation budget is independent of the center.
```
noncomputable def giantReciprocalFactor (P : Polynomial ℝ) (G : ℝ) : ClippedPolynomialFactor :=
…
```
Mentions: OAI.Ostmann.ClippedPolynomialFactor
theorem OAI.Ostmann.giantReciprocalFactor_budget line 16
theorem OAI.Ostmann.giantReciprocalFactor_value line 21

theorem OAI.Ostmann.giantReciprocalFactor_cutoff line 40

Source documentation

Multiplication by the actual giant cutoff makes the clipped reciprocal identical to the manuscript's reciprocal everywhere, including zero terms.

theorem giantReciprocalFactor_cutoff (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) (x : ℝ) :
    (logCutoffPolynomialFactor P φ G B D hB hD hφ hlip).value x *
      ((Real.exp 1 : ℂ) * (giantReciprocalFactor P G).value x) =
        (positiveLogCutoff φ G (P.eval x) : ℂ) * (Real.exp G / P.eval x : ℝ) := by
…

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