ExceptionalExponents.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

Exponent contradictions in the exceptional character moments

These are the real-variable steps in the proof of the exceptional-character-moment proposition (prop:dual) in An unconditional first moment for cubic Gauss sums. The analytic large-sieve and Gram estimates are separate inputs to these numerical steps.

theorem OAI.CubicFirstMoment.cubicSieve_exponent line 18
Source documentation
On the useful range, the mixed term in the cubic sieve dominates both endpoint terms.
```
theorem cubicSieve_exponent {z : ℝ} (hz₀ : 1 / 2 ≤ z) (hz₁ : z ≤ 2) :
    z + max (max 1 z) (2 * (1 + z) / 3) = 2 / 3 + 5 * z / 3 := by
…
```
theorem OAI.CubicFirstMoment.balanced_moment_saturation line 27
Source documentation
Cardinality and the fourth moment force saturation in the balanced exceptional configuration.
```
theorem balanced_moment_saturation {r v : ℝ}
    (hlarge : 7 / 3 - 2 * v ≤ r) (hcard : r ≤ 2 / 3)
    (hfourth : r + 4 * v ≤ 4) : r = 2 / 3 ∧ v = 5 / 6 := by
…
```
theorem OAI.CubicFirstMoment.balanced_extra_factor_gap line 34
Source documentation
Repeating an intermediate factor improves the balanced fourth-moment bound strictly beyond the saturated row count.
```
theorem balanced_extra_factor_gap {z : ℝ} (hz₀ : 1 < z) (hz₁ : z < 2) :
    max (4 / 3) z - 2 * z / 3 < 2 / 3 := by
…
```
theorem OAI.CubicFirstMoment.gram_exponent_gap line 44
Source documentation
The diagonal and off-diagonal Gram exponents are both strictly below the putative large-value exponent when 4/3 < z < 2.
```
theorem gram_exponent_gap {z : ℝ} (hz₀ : 4 / 3 < z) (hz₁ : z < 2) :
    max (z - 2 / 3) ((z + max 1 (2 - 2 * z / 3) - 2 / 3) / 2) <
      2 * z / 3 := by
…
```
theorem OAI.CubicFirstMoment.exists_copies_in_gram_range line 57
Source documentation
A positive short factor can be copied a fixed integer number of times so that its exponent is strictly inside the Gram range.
```
theorem exists_copies_in_gram_range {a : ℝ} (ha : 0 < a) (ha₁ : a ≤ 1 / 2) :
    ∃ m : ℕ, 4 / 3 < (m : ℝ) * a ∧ (m : ℝ) * a < 2 := by
…
```
theorem OAI.CubicFirstMoment.multiplicity_defect_nonpos line 77
Source documentation
The all-ones multiplicity vector and the vector with one extra copy force that factor's defect to be nonpositive.
```
theorem multiplicity_defect_nonpos {r total defect : ℝ}
    (hlower : 2 / 3 - 2 * total ≤ r)
    (hextra : r ≤ 2 / 3 - 2 * (total + defect)) : defect ≤ 0 := by
…
```

theorem OAI.CubicFirstMoment.short_multiplicity_defect_zero line 84

Source documentation

When deleting a short factor stays in the sieve range, the two multiplicity tests force its defect to vanish.

theorem short_multiplicity_defect_zero {r total defect : ℝ}
    (hlower : 2 / 3 - 2 * total ≤ r)
    (hextra : r ≤ 2 / 3 - 2 * (total + defect))
    (hdelete : r ≤ 2 / 3 - 2 * (total - defect)) : defect = 0 := by
…

theorem OAI.CubicFirstMoment.sum_omit_one line 95
theorem OAI.CubicFirstMoment.exceptional_multiplicity_rigidity line 112
Source documentation
The fixed-multiplicity argument in the first exceptional configuration. It forces every factor to have the same 5/6 exponent and forces the row count exponent to be 2/3, before the off-diagonal Gram estimate is applied.
Here d i is v i - 5 * a i / 6. The two sides of the large-value and large-sieve inequalities have already been expressed in terms of these factor defects.
```
theorem exceptional_multiplicity_rigidity {ι : Type*} [Fintype ι] [DecidableEq ι]
    (a d : ι → ℝ) (r : ℝ)
    (ha : ∀ i, 0 ≤ a i ∧ a i < 1) (hsum : ∑ i, a i = 1)
    (hlarge : 2 / 3 - 2 * (∑ i, d i) ≤ r)
    (hmoment : ∀ k : ι → ℕ,
      1 / 2 ≤ (∑ i, (k i : ℝ) * a i) → (∑ i, (k i : ℝ) * a i) ≤ 2 →
      r ≤ 2 / 3 - 2 * (∑ i, (k i : ℝ) * d i)) :
    (∀ i, d i = 0) ∧ r = 2 / 3 := by
…
```
theorem OAI.CubicFirstMoment.exists_balanced_factor line 193
Source documentation
In the balanced exceptional configuration, a saturated total value forces at least one positive-length factor to attain its 5/6 share. This is the factor that is repeated in the extra-moment argument.
```
theorem exists_balanced_factor {ι : Type*} [Fintype ι]
    (a v : ι → ℝ) (ha : ∀ i, 0 ≤ a i) (hv : ∀ i, v i ≤ a i)
    (ha_sum : ∑ i, a i = 1) (hv_sum : ∑ i, v i = 5 / 6) :
    ∃ i, 0 < a i ∧ 5 * a i / 6 ≤ v i := by
…
```