VaryingConductorSequences.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The exceptional short-factor contradictions allow conductor scales with the required limiting exponent, without fixing the scales to exact powers.

theorem OAI.CubicFirstMoment.ShortFactorFamily.first_varying_conductor_sequence_impossible line 16

Source documentation

With a fixed gap below length one, an actual first-configuration moment cannot remain at exponent 7/3. All subsequences are constructed.

theorem ShortFactorFamily.first_varying_conductor_sequence_impossible (F : ShortFactorFamily ι)
    (Y N G : ℕ → ℝ) (S : ℕ → Finset Eisenstein) {δ H D : ℝ}
    (hδ : 0 < δ) (hH : 0 ≤ H) (hD : 0 ≤ D)
    (hY : Tendsto Y atTop atTop) (hY₂ : ∀ j, 2 ≤ Y j)
    (hG : ∀ j, 1 ≤ G j) (hGexp : HasPowerExponent Y G (7/3))
    (hN : ∀ j, 1 ≤ N j) (hNexp : HasPowerExponent Y N 1)
    (hS : ∀ j, ∀ p ∈ S j, gramDyad (N j) p)
    (hcard : ∀ j, ((S j).card:ℝ) ≤ (Y j)^D)
    (hshort : ∀ j i, F.length j i ≤ (Y j)^(1-δ))
    (htotal : HasPowerExponent Y (fun j => ∏ i, F.length j i) 1)
    (hbound : ∀ j, ∀ p ∈ S j, ∀ i, ‖F.cubicValue j i p‖ ≤ (Y j)^H)
    (hmoment : ∀ j, G j ≤ ∑ p ∈ S j, ‖∏ i, F.cubicValue j i p‖^2) : False := by
…

Mentions: OAI.CubicFirstMoment.ShortFactorFamily, OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.HasPowerExponent, OAI.CubicFirstMoment.gramDyad

theorem OAI.CubicFirstMoment.ShortFactorFamily.balanced_varying_conductor_sequence_impossible line 55

Source documentation

The balanced actual short-factor family also cannot retain an unsaved moment; its row and value limits are extracted inside the proof.

theorem ShortFactorFamily.balanced_varying_conductor_sequence_impossible (F : ShortFactorFamily ι)
    (hHuxley : HuxleyAdditiveLargeSieve) (Y L G : ℕ → ℝ)
    (S : ℕ → Finset (Eisenstein × Eisenstein)) {δ H D : ℝ}
    (hδ : 0 < δ) (hH : 0 ≤ H) (hD : 0 ≤ D)
    (hY : Tendsto Y atTop atTop) (hY₂ : ∀ j, 2 ≤ Y j)
    (hG : ∀ j, 1 ≤ G j) (hGexp : HasPowerExponent Y G (7/3))
    (hL : ∀ j, 1 ≤ L j) (hLexp : HasPowerExponent Y L (1/3))
    (hS : ∀ j, ∀ p ∈ S j, PrimarySquarefreePair p ∧
      norm p.1 ≤ L j ∧ norm p.2 ≤ L j)
    (hcard : ∀ j, ((S j).card:ℝ) ≤ (Y j)^D)
    (hshort : ∀ j i, F.length j i ≤ (Y j)^(1-δ))
    (htotal : HasPowerExponent Y (fun j => ∏ i, F.length j i) 1)
…

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