OAI/NumberTheory/CubicMoment/Estimates/ShortFactorSequences.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CubicFirstMoment.ShortFactorFamily.comp line 12
2. lemma OAI.CubicFirstMoment.ShortFactorFamily.comp_cubicValue line 22
3. lemma OAI.CubicFirstMoment.ShortFactorFamily.comp_mixedValue line 26
4. theorem OAI.CubicFirstMoment.ShortFactorFamily.lengths_subsequence line 35

   Source documentation

   Compactness produces the length exponents too. Thus the subsequent moment argument does not assume either the value or the length limits.

   theorem ShortFactorFamily.lengths_subsequence (F : ShortFactorFamily ι)
       {Y : ℕ → ℝ} {δ : ℝ} (_hY : Tendsto Y atTop atTop) (hY₁ : ∀ j, 1 < Y j)
       (hshort : ∀ j i, F.length j i ≤ (Y j)^(1-δ))
       (htotal : HasPowerExponent Y (fun j => ∏ i, F.length j i) 1) :
       ∃ (φ : ℕ → ℕ) (a : ι → ℝ), StrictMono φ ∧
         (∀ i, 0 ≤ a i ∧ a i ≤ 1-δ) ∧ (∑ i, a i = 1) ∧
         ∀ i, HasPowerExponent (Y ∘ φ) (fun j => F.length (φ j) i) (a i) := by
   …

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

5. theorem OAI.CubicFirstMoment.ShortFactorFamily.first_unsaved_sequence_impossible line 56

   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_unsaved_sequence_impossible (F : ShortFactorFamily ι)
       (Y 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))
       (hS : ∀ j, ∀ p ∈ S j, gramDyad (Y 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

6. theorem OAI.CubicFirstMoment.ShortFactorFamily.balanced_unsaved_sequence_impossible line 97

   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_unsaved_sequence_impossible (F : ShortFactorFamily ι)
       (hHuxley : HuxleyAdditiveLargeSieve) (Y 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))
       (hS : ∀ j, ∀ p ∈ S j, PrimarySquarefreePair p ∧
         norm p.1 ≤ (Y j)^(1/3:ℝ) ∧ norm p.2 ≤ (Y j)^(1/3:ℝ))
       (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.mixedValue j i p‖ ≤ (Y j)^H)
   …

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