NoncubeFrequencyBounds.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Quantitative cubic-sieve bounds on the actual decomposed frequencies. The residual factor includes the ramified part; the cube variable causes only an exclusion and therefore costs its cardinality. No exceptional-moment estimate is assumed here.

theorem OAI.CubicFirstMoment.residualFrequency_sieve_bound line 17

Source documentation

Both orientations of the published cubic large sieve on a frequency block r*p*q²*j³, with the cube and ramified multiplicities explicit.

theorem residualFrequency_sieve_bound :
    ∀ ε : ℝ, 0 < ε → ∃ C₀ : ℝ, 0 < C₀ ∧
    ∀ (B R P Q J : Finset Eisenstein) (N U V : ℝ),
      1 ≤ N → 1 ≤ U → 1 ≤ V →
      (∀ b ∈ B, primary b ∧ Squarefree b ∧ norm b ≤ N) →
      (∀ p ∈ P, primary p ∧ Squarefree p ∧ norm p ≤ U) →
      (∀ q ∈ Q, primary q ∧ Squarefree q ∧ norm q ≤ V) →
      ∀ β : Eisenstein → ℂ,
      (∑ h ∈ residualCubeSupport R P Q J, ‖∑ b ∈ B, β b*cubicSymbol b h‖^2) ≤
        (R.card:ℝ)*J.card*C₀ *
          min ((Q.card:ℝ)*(U*N)^ε*(U+N+(U*N)^(2/3:ℝ)))
              ((P.card:ℝ)*(V*N)^ε*(V+N+(V*N)^(2/3:ℝ))) *
…

Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.norm, OAI.CubicFirstMoment.residualCubeSupport, OAI.CubicFirstMoment.cubicSymbol

theorem OAI.CubicFirstMoment.frequency_subset_mass_le line 55
Source documentation
Restricting the actual frequencies, for instance to noncubes and a norm dyad, can only decrease the positive quadratic mass.
```
theorem frequency_subset_mass_le (H F B : Finset Eisenstein)
    (hHF : H ⊆ F) (β : Eisenstein → ℂ) :
    (∑ h ∈ H, ‖∑ b ∈ B, β b*cubicSymbol b h‖^2) ≤
      ∑ h ∈ F, ‖∑ b ∈ B, β b*cubicSymbol b h‖^2 :=
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.cubicSymbol

theorem OAI.CubicFirstMoment.twisted_residualFrequency_sieve_bound line 63

Source documentation

A fixed norm or angular phase, or a fixed arithmetic exclusion, is absorbed into the coefficients without increasing their squared norm.

theorem twisted_residualFrequency_sieve_bound :
    ∀ ε : ℝ, 0 < ε → ∃ C₀ : ℝ, 0 < C₀ ∧
    ∀ (B R P Q J H : Finset Eisenstein) (N U V : ℝ),
      1 ≤ N → 1 ≤ U → 1 ≤ V →
      (∀ b ∈ B, primary b ∧ Squarefree b ∧ norm b ≤ N) →
      (∀ p ∈ P, primary p ∧ Squarefree p ∧ norm p ≤ U) →
      (∀ q ∈ Q, primary q ∧ Squarefree q ∧ norm q ≤ V) →
      H ⊆ residualCubeSupport R P Q J →
      ∀ β z : Eisenstein → ℂ, (∀ b ∈ B, ‖z b‖ ≤ 1) →
      (∑ h ∈ H, ‖∑ b ∈ B, β b*z b*cubicSymbol b h‖^2) ≤
        (R.card:ℝ)*J.card*C₀ *
          min ((Q.card:ℝ)*(U*N)^ε*(U+N+(U*N)^(2/3:ℝ)))
…

Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.norm, OAI.CubicFirstMoment.residualCubeSupport, OAI.CubicFirstMoment.cubicSymbol