Documentation

LeanPool.Odlyzko.TestFunction.Basic

TODO: Add doc-string.

noncomputable def NumberField.Odlyzko.Tartar.weight (x : ℝ) :

A weight used in the Odlyzko-bound argument.

Equations

NumberField.Odlyzko.Tartar.weight x = max (1 - x ^ 2) 0

Instances For

noncomputable def NumberField.Odlyzko.Tartar.amplitude (x : ℝ) :

An amplitude used in the Odlyzko-bound argument.

Equations

NumberField.Odlyzko.Tartar.amplitude x = if x = 0 then 1 else 3 * (Real.sin x - x * Real.cos x) / x ^ 3

Instances For

noncomputable def NumberField.Odlyzko.Tartar.testFunction (x : ℝ) :

A test function used in the Odlyzko-bound argument.

Equations

NumberField.Odlyzko.Tartar.testFunction x = NumberField.Odlyzko.Tartar.amplitude x ^ 2

Instances For

@[simp]

theorem NumberField.Odlyzko.tartarAmplitude_zero :

Tartar.amplitude 0 = 1

@[simp]

theorem NumberField.Odlyzko.tartarTestFunction_zero :

Tartar.testFunction 0 = 1

theorem NumberField.Odlyzko.tartarWeight_nonneg (x : ℝ) :

0 ≤ Tartar.weight x

theorem NumberField.Odlyzko.tartarTestFunction_nonneg (x : ℝ) :

0 ≤ Tartar.testFunction x

theorem NumberField.Odlyzko.tartarWeight_eq_zero_of_one_le_abs {x : ℝ} (hx : 1 ≤ |x|) :

Tartar.weight x = 0

theorem NumberField.Odlyzko.tartarWeight_eq_one_sub_sq_of_abs_le_one {x : ℝ} (hx : |x| ≤ 1) :

Tartar.weight x = 1 - x ^ 2

theorem NumberField.Odlyzko.tartarWeight_neg (x : ℝ) :

Tartar.weight (-x) = Tartar.weight x

theorem NumberField.Odlyzko.tartarAmplitude_neg (x : ℝ) :

Tartar.amplitude (-x) = Tartar.amplitude x

theorem NumberField.Odlyzko.tartarTestFunction_neg (x : ℝ) :

Tartar.testFunction (-x) = Tartar.testFunction x

theorem NumberField.Odlyzko.tartarWeight_continuous :

Continuous Tartar.weight