ExceptionalRows.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Rigidity and contradiction for actual short-factor large-value rows.

theorem OAI.CubicFirstMoment.HasPowerExponent.le_of_small_power line 16

Source documentation

A bound by every arbitrarily enlarged power passes to the exact logarithmic exponent. The constants are allowed to depend on the enlargement.

theorem HasPowerExponent.le_of_small_power {Y f g : ℕ → ℝ} {a b : ℝ}
    (hf : HasPowerExponent Y f a) (hg : HasPowerExponent Y g b)
    (hY : Tendsto Y atTop atTop)
    (hfp : ∀ᶠ j in atTop, 0 < f j) (hgp : ∀ᶠ j in atTop, 0 < g j)
    (hbound : ∀ η : ℝ, 0 < η → ∃ C : ℝ, 0 < C ∧
      ∀ᶠ j in atTop, f j ≤ C*(g j)^(1+η)) : a ≤ b := by
…

Mentions: OAI.CubicFirstMoment.HasPowerExponent

theorem OAI.CubicFirstMoment.ShortFactorFamily.cubicValue_small_power line 38
theorem OAI.CubicFirstMoment.ShortFactorFamily.mixedValue_small_power line 52
theorem OAI.CubicFirstMoment.ShortFactorFamily.length_exponent_nonneg line 67
theorem OAI.CubicFirstMoment.ShortFactorFamily.cubic_value_exponent_le line 76
theorem OAI.CubicFirstMoment.ShortFactorFamily.mixed_value_exponent_le line 94

theorem OAI.CubicFirstMoment.balanced_rows_exponent_le line 115

Source documentation

The exponent 2/3 for balanced row cardinality is proved from the actual two component norm cutoffs, rather than imposed on the row count.

theorem balanced_rows_exponent_le {Y L : ℕ → ℝ}
    (P : ℕ → Finset (Eisenstein × Eisenstein)) {r : ℝ}
    (hY : Tendsto Y atTop atTop) (hL : ∀ j, 1 ≤ L j)
    (hP : ∀ j, ∀ p ∈ P j, primary p.1 ∧ primary p.2 ∧
      norm p.1 ≤ L j ∧ norm p.2 ≤ L j)
    (hPne : ∀ j, (P j).Nonempty)
    (hR : HasPowerExponent Y (fun j => ((P j).card:ℝ)) r)
    (hLexp : HasPowerExponent Y L (1/3)) : r ≤ 2/3 := by
…

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

theorem OAI.CubicFirstMoment.ShortFactorFamily.cubic_rows_rigidity line 137

Source documentation

Actual first-configuration short factors and their sharp moments force all values to have exponent 5/6 of their length and exactly 2/3 rows.

theorem ShortFactorFamily.cubic_rows_rigidity (F : ShortFactorFamily ι)
    {Y N : ℕ → ℝ} (P : ℕ → Finset Eisenstein) (B : ℕ → ι → ℝ)
    {a v : ι → ℝ} {r : ℝ}
    (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 1)
    (hXexp : ∀ i, HasPowerExponent Y (fun j => F.length j i) (a i))
    (hBexp : ∀ i, HasPowerExponent Y (fun j => B j i) (v i))
    (ha : ∀ i, a i < 1) (hsum : ∑ i, a i = 1)
…

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

theorem OAI.CubicFirstMoment.ShortFactorFamily.balanced_rows_contradiction line 164

Source documentation

No balanced sequence of actual short-factor large-value rows can satisfy the unsaved moment lower bound when every factor is shorter than one. The only published assumption here is Huxley's additive large sieve.

theorem ShortFactorFamily.balanced_rows_contradiction (F : ShortFactorFamily ι)
    (hHuxley : HuxleyAdditiveLargeSieve) {Y Q L : ℕ → ℝ}
    (P : ℕ → Finset (Eisenstein × Eisenstein)) (B : ℕ → ι → ℝ)
    {a v : ι → ℝ} {r : ℝ}
    (hY : Tendsto Y atTop atTop) (hQ : ∀ j, 1 ≤ Q j) (hL : ∀ j, 1 ≤ L j)
    (hP : ∀ j, ∀ p ∈ P j, PrimarySquarefreePair p ∧ norm (pairConductor p) ≤ Q j)
    (hLP : ∀ j, ∀ p ∈ P j, norm p.1 ≤ L j ∧ norm p.2 ≤ L 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 (2/3)) (hLexp : HasPowerExponent Y L (1/3))
    (hXexp : ∀ i, HasPowerExponent Y (fun j => F.length j i) (a i))
…

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