DegreeWeight.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem335.latticeMajorant line 12
Source documentation
The geometric majorant for weights at the integers around a chosen center.
```
def latticeMajorant (q d : ℝ) (z : ℤ) : ℝ :=
…
```
lemma OAI.Problem335.latticeMajorant_nonneg line 15
lemma OAI.Problem335.hasSum_latticeMajorant line 22
lemma OAI.Problem335.rpow_abs_sub_le_latticeMajorant line 51
lemma OAI.Problem335.sum_lattice_rpow_le line 77
lemma OAI.Problem335.sum_nat_rpow_le line 89
lemma OAI.Problem335.rpow_geometric_bound line 107
lemma OAI.Problem335.rpow_geometric_bound_le_five line 121
lemma OAI.Problem335.sum_nat_rpow_le_nearest line 131
lemma OAI.Problem335.sum_nat_rpow_le_five line 137

theorem OAI.Problem335.degreeWeight_le_nearest line 145

Source documentation

The nearest-integer geometric estimate for the manuscript's factor weight.

theorem degreeWeight_le_nearest {q : ℝ} (hq : 0 < q) (hqhalf : q ≤ 1 / 2)
    (lam : ℝ) (e : ℕ) :
    degreeWeight q lam e ≤
      q ^ nearestIntegerDistance (lam * e) *
        (1 + 4 * q ^ (1 - 2 * nearestIntegerDistance (lam * e))) :=
…

Mentions: OAI.Problem335.degreeWeight, OAI.Problem335.nearestIntegerDistance

theorem OAI.Problem335.degreeWeight_le_five_mul line 153
Source documentation
The sharper uniform estimate retaining the nearest-integer saving.
```
theorem degreeWeight_le_five_mul {q : ℝ} (hq : 0 < q) (hqhalf : q ≤ 1 / 2)
    (lam : ℝ) (e : ℕ) :
    degreeWeight q lam e ≤ 5 * q ^ nearestIntegerDistance (lam * e) := by
…
```
Mentions: OAI.Problem335.degreeWeight, OAI.Problem335.nearestIntegerDistance
theorem OAI.Problem335.degreeWeight_le_five line 164
Source documentation
Uniform upper bound for each factor weight, including arbitrarily high degrees.
```
theorem degreeWeight_le_five {q : ℝ} (hq : 0 < q) (hqhalf : q ≤ 1 / 2)
    (lam : ℝ) (e : ℕ) : degreeWeight q lam e ≤ 5 :=
…
```
Mentions: OAI.Problem335.degreeWeight