RepeatedPrimeSupport.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

The squarefree prime-convolution discrepancy has sparse support. This supplies the support saving before the character-moment estimates.

def OAI.CubicFirstMoment.squarefreeConvolutionError line 15
theorem OAI.CubicFirstMoment.convolutionError_mem_largeSquareSupport line 21
Source documentation
Every surviving discrepancy coefficient is divisible by the square of one of the large supported primes.
```
theorem convolutionError_mem_largeSquareSupport
    (S : ι → Finset Eisenstein) (w : ι → Eisenstein → ℂ) (Y D : ℝ)
    (hS : ∀ i, ∀ p ∈ S i, primaryPrime p ∧ D < norm p)
    (hY : ∀ f ∈ Fintype.piFinset S, norm (∏ i, f i) ≤ Y)
    {b : Eisenstein} (hb : squarefreeConvolutionError S w b ≠ 0) :
    b ∈ largeSquareSupport Y D := by
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primaryPrime, OAI.CubicFirstMoment.norm, OAI.CubicFirstMoment.squarefreeConvolutionError, OAI.CubicFirstMoment.largeSquareSupport

theorem OAI.CubicFirstMoment.convolutionError_energy_bound line 56

Source documentation

Uniform energy saving for the actual discrepancy coefficients. A divisor-type coefficient bound may be inserted as E; the support saving itself is unconditional and independent of that bound.

theorem convolutionError_energy_bound :
    ∃ C : ℝ, 0 < C ∧ ∀ (S : ι → Finset Eisenstein)
      (w : ι → Eisenstein → ℂ) (Y D E : ℝ),
      0 ≤ Y → 0 < D → 0 ≤ E →
      (∀ i, ∀ p ∈ S i, primaryPrime p ∧ D < norm p) →
      (∀ f ∈ Fintype.piFinset S, norm (∏ i, f i) ≤ Y) →
      (∀ b ∈ orderedConvolutionSupport S, ‖squarefreeConvolutionError S w b‖ ≤ E) →
      (∑ b ∈ orderedConvolutionSupport S, ‖squarefreeConvolutionError S w b‖^2) ≤
        C*Y*D^(-(1/2:ℝ))*E^2 := by
…

Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primaryPrime, OAI.CubicFirstMoment.norm, OAI.CubicFirstMoment.orderedConvolutionSupport, OAI.CubicFirstMoment.squarefreeConvolutionError

theorem OAI.CubicFirstMoment.primeConvolutionError_energy_bound line 93

Source documentation

The coefficient-amplitude hypothesis is discharged for the actual prime convolution by the uniform prime-tuple multiplicity bound.

theorem primeConvolutionError_energy_bound :
    ∃ C : ℝ, 0 < C ∧ ∀ (S : ι → Finset Eisenstein)
      (w : ι → Eisenstein → ℂ) (M : ι → ℝ) (Y D : ℝ),
      0 ≤ Y → 0 < D → (∀ i, 0 ≤ M i) →
      (∀ i, ∀ p ∈ S i, primaryPrime p ∧ D < norm p) →
      (∀ f ∈ Fintype.piFinset S, norm (∏ i, f i) ≤ Y) →
      (∀ i, ∀ p ∈ S i, ‖w i p‖ ≤ M i) →
      (∑ b ∈ orderedConvolutionSupport S, ‖squarefreeConvolutionError S w b‖^2) ≤
        C*Y*D^(-(1/2:ℝ))*
          (((Fintype.card ι)^(Fintype.card ι):ℕ)*(∏ i, M i))^2 := by
…

theorem OAI.CubicFirstMoment.primeConvolutionError_power_energy line 113

Source documentation

With every prime larger than Y^c, the repeated-prime error has a fixed support saving Y^(-c/2), before the harmless smooth-weight factors.

theorem primeConvolutionError_power_energy :
    ∃ C : ℝ, 0 < C ∧ ∀ (S : ι → Finset Eisenstein)
      (w : ι → Eisenstein → ℂ) (M : ι → ℝ) (Y c : ℝ),
      0 < Y → (∀ i, 0 ≤ M i) →
      (∀ i, ∀ p ∈ S i, primaryPrime p ∧ Y^c < norm p) →
      (∀ f ∈ Fintype.piFinset S, norm (∏ i, f i) ≤ Y) →
      (∀ i, ∀ p ∈ S i, ‖w i p‖ ≤ M i) →
      (∑ b ∈ orderedConvolutionSupport S, ‖squarefreeConvolutionError S w b‖^2) ≤
        C*Y^(1-c/2)*(((Fintype.card ι)^(Fintype.card ι):ℕ)*(∏ i, M i))^2 := by
…