ShortFactorLargeValues.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Actual large-value rows for the short ideal factors.

lemma OAI.CubicFirstMoment.finite_power_product_large_values line 12
theorem OAI.CubicFirstMoment.HasPowerExponent.finset_prod line 29
theorem OAI.CubicFirstMoment.HasPowerExponent.prod_natPowers line 38
structure OAI.CubicFirstMoment.ShortFactorFamily line 49
Source documentation
The arithmetic data of the actual short factors, before choosing a set of characters on which their values are large.
```
structure ShortFactorFamily (ι : Type*) where
…
```
def OAI.CubicFirstMoment.ShortFactorFamily.cubicValue line 58
def OAI.CubicFirstMoment.ShortFactorFamily.mixedValue line 63

theorem OAI.CubicFirstMoment.ShortFactorFamily.cubic_large_values_exponent line 72

Source documentation

The first limiting moment inequality follows from the actual short-factor moment and the actual large-value rows.

theorem ShortFactorFamily.cubic_large_values_exponent (F : ShortFactorFamily ι)
    (k : ι → ℕ) {Y N : ℕ → ℝ} (P : ℕ → Finset Eisenstein)
    (B : ℕ → ι → ℝ) {a v : ι → ℝ} {r n : ℝ}
    (hY : Tendsto Y atTop atTop) (hN : ∀ j, 1 ≤ N j)
    (hP : ∀ j, ∀ x ∈ P j, primary x ∧ Squarefree x ∧ norm x ≤ N j)
    (hPne : ∀ j, (P j).Nonempty) (hB : ∀ j i, 0 < B j i)
    (hrow : ∀ j, ∀ x ∈ P j, ∀ i, B j i ≤ ‖F.cubicValue j i x‖)
    (hRexp : HasPowerExponent Y (fun j => ((P j).card:ℝ)) r)
    (hNexp : HasPowerExponent Y N n)
    (hXexp : ∀ i, HasPowerExponent Y (fun j => F.length j i) (a i))
    (hBexp : ∀ i, HasPowerExponent Y (fun j => B j i) (v i)) :
    r+2*(∑ i, (k i:ℝ)*v i) ≤ (∑ i, (k i:ℝ)*a i)+
…

Mentions: OAI.CubicFirstMoment.ShortFactorFamily, OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.norm, OAI.CubicFirstMoment.HasPowerExponent

theorem OAI.CubicFirstMoment.ShortFactorFamily.mixed_large_values_exponent line 109

Source documentation

The second limiting moment inequality retains the genuine ordinary mixed-character input and the same actual short factors.

theorem ShortFactorFamily.mixed_large_values_exponent (F : ShortFactorFamily ι)
    (hHuxley : HuxleyAdditiveLargeSieve) (k : ι → ℕ)
    {Y Q : ℕ → ℝ} (P : ℕ → Finset (Eisenstein × Eisenstein))
    (B : ℕ → ι → ℝ) {a v : ι → ℝ} {r q : ℝ}
    (hY : Tendsto Y atTop atTop) (hQ : ∀ j, 1 ≤ Q j)
    (hP : ∀ j, ∀ p ∈ P j, PrimarySquarefreePair p ∧ norm (pairConductor p) ≤ Q j)
    (hPne : ∀ j, (P j).Nonempty) (hB : ∀ j i, 0 < B j i)
    (hrow : ∀ j, ∀ p ∈ P j, ∀ i, B j i ≤ ‖F.mixedValue j i p‖)
    (hRexp : HasPowerExponent Y (fun j => ((P j).card:ℝ)) r)
    (hQexp : HasPowerExponent Y Q q)
    (hXexp : ∀ i, HasPowerExponent Y (fun j => F.length j i) (a i))
    (hBexp : ∀ i, HasPowerExponent Y (fun j => B j i) (v i)) :
…

Mentions: OAI.CubicFirstMoment.ShortFactorFamily, OAI.CubicFirstMoment.HuxleyAdditiveLargeSieve, OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.PrimarySquarefreePair, OAI.CubicFirstMoment.norm, OAI.CubicFirstMoment.pairConductor, OAI.CubicFirstMoment.HasPowerExponent