PrimePowerSupport.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Higher prime powers in the von Mangoldt replacement have sparse support, even when the underlying prime is small.

lemma OAI.CubicFirstMoment.primePower_norm_pow line 13
lemma OAI.CubicFirstMoment.large_square_of_prime_power line 20
Source documentation
Extracting half the exponent produces a genuinely large square divisor. The bound depends on the prime-power norm, not the prime norm.
```
lemma large_square_of_prime_power {p b : Eisenstein} (hp : p ≠ 0) {j : ℕ}
    (hj : 2 ≤ j) {Y c : ℝ} (hY : 0 < Y)
    (hlarge : Y^c < norm (p^j)) (hdiv : p^j ∣ b) :
    ∃ d : Eisenstein, Y^(c/4) < norm d ∧ d^2 ∣ b := by
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.norm
def OAI.CubicFirstMoment.largePrimePowerSupport line 42
lemma OAI.CubicFirstMoment.largePrimePowerSupport_subset line 46
theorem OAI.CubicFirstMoment.largePrimePowerSupport_card_bound line 54
Source documentation
A fixed positive power is saved for every higher-prime-power error support.
```
theorem largePrimePowerSupport_card_bound :
    ∃ K : ℝ, 0 < K ∧ ∀ (Y c : ℝ), 0 < Y →
      ((largePrimePowerSupport Y c).card:ℝ) ≤ K*Y^(1-c/8) := by
…
```
Mentions: OAI.CubicFirstMoment.largePrimePowerSupport

theorem OAI.CubicFirstMoment.primePowerError_energy_bound line 76

Source documentation

Any bounded coefficients supported on these errors inherit the same saving in their quadratic energy.

theorem primePowerError_energy_bound :
    ∃ K : ℝ, 0 < K ∧ ∀ (Y c A : ℝ), 0 < Y → 0 ≤ A →
      ∀ v : Eisenstein → ℂ, (∀ b ∈ largePrimePowerSupport Y c, ‖v b‖ ≤ A) →
      (∑ b ∈ largePrimePowerSupport Y c, ‖v b‖^2) ≤ K*Y^(1-c/8)*A^2 := by
…

Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.largePrimePowerSupport