NormalizedFourierProfile.lean`

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Bounds for the actual normalized level-zero Fourier profile

theorem OAI.Ostmann.abs_inv_sub_inv_le_of_one_le line 14
theorem OAI.Ostmann.abs_sqrt_sub_sqrt_le_of_one_le line 22
theorem OAI.Ostmann.abs_inv_sqrt_sub_inv_sqrt_le line 32
def OAI.Ostmann.normalizedFourierProfile line 37
theorem OAI.Ostmann.normalizedFourierProfile_norm line 40
theorem OAI.Ostmann.normalizedFourierProfile_lipschitz line 48
theorem OAI.Ostmann.normalizedFourierProfile_original line 76
Source documentation
Normalizing by X exactly recovers the original Fourier factor, before its separate bounded support cutoff is applied.
```
theorem normalizedFourierProfile_original (ψ : ℝ → ℂ) (X M v : ℝ)
    (hX : X ≠ 0) (hM : M ≠ 0) :
    normalizedFourierProfile ψ v (M / X) = archimedeanLeafFactor X M v 1 ψ := by
…
```
Mentions: OAI.Ostmann.normalizedFourierProfile, OAI.Ostmann.archimedeanLeafFactor
theorem OAI.Ostmann.schwartz_profile_bounds line 86
Source documentation
A Schwartz profile supplies its bounded derivative and Lipschitz constant from existing library seminorms, with no analytic input left as an assumption.
```
theorem schwartz_profile_bounds (ψ : 𝓢(ℝ, ℂ)) :
    (∀ t, ‖ψ t‖ ≤ SchwartzMap.seminorm ℝ 0 0 ψ) ∧
    (∀ s t, ‖ψ s - ψ t‖ ≤ SchwartzMap.seminorm ℝ 0 1 ψ * |s - t|) := by
…
```
theorem OAI.Ostmann.schwartz_profile_lip_nonneg line 99
def OAI.Ostmann.fourierPolynomialFactor line 104
Source documentation
Concrete clipped factor for the Fourier weight on its declared M/X range.
```
noncomputable def fourierPolynomialFactor (P : Polynomial ℝ) (ψ : 𝓢(ℝ, ℂ))
    (v lo hi : ℝ) (hlo : 1 ≤ lo) (hhi : lo ≤ hi) : ClippedPolynomialFactor where
…
```
Mentions: OAI.Ostmann.ClippedPolynomialFactor
theorem OAI.Ostmann.fourierPolynomialFactor_original line 122