PrimaryConvolutionEnergy.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Fixed-length convolutions of arbitrary primary elements. The divisor bound absorbs the tuple multiplicity in any positive norm power.

lemma OAI.CubicFirstMoment.orderedPrimarySupport_primary line 15

theorem OAI.CubicFirstMoment.primary_tuple_fiber_small_power line 23

Source documentation

The tuple multiplicity is uniformly a small power even when each factor has arbitrarily many distinct prime divisors.

theorem primary_tuple_fiber_small_power {ε : ℝ} (hε : 0 < ε) :
    ∃ C : ℝ, 0 < C ∧ ∀ (S : ι → Finset Eisenstein),
      (∀ i, ∀ a ∈ S i, primary a) → ∀ Y : ℝ, 1 ≤ Y →
      ∀ b ∈ orderedConvolutionSupport S, norm b ≤ Y →
      (((Fintype.piFinset S).filter (fun f => (∏ i, f i) = b)).card : ℝ) ≤ C*Y^ε := by
…

Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.orderedConvolutionSupport, OAI.CubicFirstMoment.norm

theorem OAI.CubicFirstMoment.primary_orderedConvolution_energy line 66
Source documentation
Exact independent coefficient energies, with only a small norm-power loss when collecting arbitrary primary tuples by their product.
```
theorem primary_orderedConvolution_energy {ε : ℝ} (hε : 0 < ε) :
    ∃ C : ℝ, 0 < C ∧ ∀ (S : ι → Finset Eisenstein)
      (w : ι → Eisenstein → ℂ), (∀ i, ∀ a ∈ S i, primary a) →
      ∀ Y : ℝ, 1 ≤ Y → (∀ f ∈ Fintype.piFinset S, norm (∏ i, f i) ≤ Y) →
      (∑ b ∈ orderedConvolutionSupport S, ‖orderedConvolution S w b‖^2) ≤
        C*Y^ε*primeConvolutionEnergy S w := by
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.norm, OAI.CubicFirstMoment.orderedConvolutionSupport, OAI.CubicFirstMoment.orderedConvolution, OAI.CubicFirstMoment.primeConvolutionEnergy
theorem OAI.CubicFirstMoment.primary_orderedConvolution_twisted_energy line 102

theorem OAI.CubicFirstMoment.primaryConvolution_cubic_moment line 121

Source documentation

The actual independent primary-element product has the unrestricted cubic moment with the proved divisor-power energy loss.

theorem primaryConvolution_cubic_moment {ε δ : ℝ}
    (hε : 0 < ε) (hε₁ : ε ≤ 1) (hδ : 0 < δ) :
    ∃ C : ℝ, 0 < C ∧ ∀ (S : ι → Finset Eisenstein)
      (w : ι → Eisenstein → ℂ), (∀ i, ∀ a ∈ S i, primary a) →
      ∀ (P : Finset Eisenstein) (N Y : ℝ), 1 ≤ N → 1 ≤ Y →
      (∀ a ∈ P, primary a ∧ Squarefree a ∧ norm a ≤ N) →
      (∀ f ∈ Fintype.piFinset S, norm (∏ i, f i) ≤ Y) →
      (∑ a ∈ P, ‖primeCubicProductPolynomial S w a‖^2) ≤
        C*(N*Y)^ε*(N*Y^(1/3:ℝ)+(N*Y)^(2/3:ℝ)+Y^(4/3:ℝ)+Y)*
          (Y^δ*primeConvolutionEnergy S w) := by
…

Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.norm, OAI.CubicFirstMoment.primeCubicProductPolynomial, OAI.CubicFirstMoment.primeConvolutionEnergy

theorem OAI.CubicFirstMoment.primaryConvolution_mixed_moment line 157

Source documentation

The corresponding ordinary mixed-character moment for actual independent primary factors. Huxley's additive large sieve is the only published analytic assumption.

theorem primaryConvolution_mixed_moment (hHuxley : HuxleyAdditiveLargeSieve)
    {ε δ : ℝ} (hε : 0 < ε) (hδ : 0 < δ) :
    ∃ C : ℝ, 0 < C ∧ ∀ (S : ι → Finset Eisenstein)
      (w : ι → Eisenstein → ℂ), (∀ i, ∀ a ∈ S i, primary a) →
      ∀ (P : Finset (Eisenstein × Eisenstein)) (Q Y : ℝ), 1 ≤ Q → 1 ≤ Y →
      (∀ p ∈ P, PrimarySquarefreePair p ∧ norm (pairConductor p) ≤ Q) →
      (∀ f ∈ Fintype.piFinset S, norm (∏ i, f i) ≤ Y) →
      (∑ p ∈ P, ‖∏ i, ∑ a ∈ S i, w i a*mixedCubic p.1 p.2 a‖^2) ≤
        C*Q^ε*(Q^2+Y)*(Y^δ*primeConvolutionEnergy S w) := by
…

Mentions: OAI.CubicFirstMoment.HuxleyAdditiveLargeSieve, OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.PrimarySquarefreePair, OAI.CubicFirstMoment.norm, OAI.CubicFirstMoment.pairConductor, OAI.CubicFirstMoment.mixedCubic, OAI.CubicFirstMoment.primeConvolutionEnergy