OAI/NumberTheory/CubicMoment/Estimates/DominantFactorLengths.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.CubicFirstMoment.remaining_length_bound line 16

   Source documentation

   Removing a factor of length at least Y^(1-δ) leaves total length at most C*Y^δ, including the fixed dyadic discrepancy C.

   theorem remaining_length_bound (X : ι → ℝ) (i : ι) {Y C δ : ℝ}
       (hY : 0 < Y) (hX : ∀ k, 0 ≤ X k) (_hC : 0 ≤ C)
       (htotal : (∏ k, X k) ≤ C*Y) (hlong : Y^(1-δ) ≤ X i) :
       (∏ k ∈ Finset.univ.erase i, X k) ≤ C*Y^δ := by
   …

2. lemma OAI.CubicFirstMoment.single_le_remaining line 32
3. theorem OAI.CubicFirstMoment.dominant_factor_unique line 42

   Source documentation

   An explicit scale condition makes a dominant factor unique.

   theorem dominant_factor_unique (X : ι → ℝ) {Y C δ : ℝ}
       (hY : 0 < Y) (hX : ∀ k, 1 ≤ X k) (hC : 0 ≤ C)
       (htotal : (∏ k, X k) ≤ C*Y) (hscale : C < Y^(1-2*δ))
       {i k : ι} (hi : Y^(1-δ) ≤ X i) (hk : Y^(1-δ) ≤ X k) : i = k := by
   …

4. theorem OAI.CubicFirstMoment.dominant_factor_eventually_unique line 57

   Source documentation

   For δ<1/2 the uniqueness condition holds beyond one common threshold.

   theorem dominant_factor_eventually_unique {C δ : ℝ} (hC : 0 ≤ C) (hδ : δ < 1/2) :
       ∃ Y₀ : ℝ, 1 ≤ Y₀ ∧ ∀ (Y : ℝ), Y₀ ≤ Y → ∀ (X : ι → ℝ),
         (∀ k, 1 ≤ X k) → (∏ k, X k) ≤ C*Y →
         ∀ i k, Y^(1-δ) ≤ X i → Y^(1-δ) ≤ X k → i = k := by
   …

5. lemma OAI.CubicFirstMoment.remaining_value_product_bound line 70
6. theorem OAI.CubicFirstMoment.short_remaining_polynomial_bound line 99

   Source documentation

   Uniformly bounded twists of the actual short arithmetic polynomials have a small remaining product after one dominant factor is removed.

   theorem short_remaining_polynomial_bound {C δ ε : ℝ}
       (hC : 0 < C) (hδ : 0 ≤ δ) (hε : 0 < ε) :
       ∃ M : ℝ, 0 < M ∧ ∀ (F Y : ℝ) (X : ι → ℝ)
         (A : ι → EisensteinArithmeticFunction) (u : ι → Eisenstein → ℂ) (i : ι),
         1 ≤ Y → (∀ k, 1 ≤ X k) → (∀ k, ShortArithmeticFactor F (A k)) →
         (∀ k, ∀ n ∈ primaryElementBall (X k), ‖u k n‖ ≤ 1) →
         (∏ k, X k) ≤ C*Y → Y^(1-δ) ≤ X i →
         ‖∏ k ∈ Finset.univ.erase i, primaryIdealPolynomial (X k) (A k) (u k)‖ ≤
           M*Y^(δ+ε) := by
   …

   Mentions: OAI.CubicFirstMoment.EisensteinArithmeticFunction, OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.ShortArithmeticFactor, OAI.CubicFirstMoment.primaryElementBall, OAI.CubicFirstMoment.primaryIdealPolynomial

7. theorem OAI.CubicFirstMoment.remaining_cubic_values_bound line 133

   Source documentation

   The remaining actual cubic factor values contribute at most a constant multiple of Y^(δ+ε), uniformly over all short-factor data.

   theorem remaining_cubic_values_bound {C δ ε : ℝ}
       (hC : 0 < C) (hδ : 0 ≤ δ) (hε : 0 < ε) :
       ∃ M : ℝ, 0 < M ∧ ∀ (F : ShortFactorFamily ι) (j : ℕ) (Y : ℝ) (i : ι)
         (p : Eisenstein), 1 ≤ Y → primary p →
         (∏ k, F.length j k) ≤ C*Y → Y^(1-δ) ≤ F.length j i →
         ‖∏ k ∈ Finset.univ.erase i, F.cubicValue j k p‖ ≤ M*Y^(δ+ε) := by
   …

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

8. theorem OAI.CubicFirstMoment.remaining_mixed_values_bound line 151

   Source documentation

   The same remaining-product bound for the actual mixed cubic values.

   theorem remaining_mixed_values_bound {C δ ε : ℝ}
       (hC : 0 < C) (hδ : 0 ≤ δ) (hε : 0 < ε) :
       ∃ M : ℝ, 0 < M ∧ ∀ (F : ShortFactorFamily ι) (j : ℕ) (Y : ℝ) (i : ι)
         (p : Eisenstein × Eisenstein), 1 ≤ Y → primary p.1 → primary p.2 →
         (∏ k, F.length j k) ≤ C*Y → Y^(1-δ) ≤ F.length j i →
         ‖∏ k ∈ Finset.univ.erase i, F.mixedValue j k p‖ ≤ M*Y^(δ+ε) := by
   …

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

9. theorem OAI.CubicFirstMoment.moment_le_dominant_factor line 170

   Source documentation

   A common bound for the other factors reduces the full product moment to the moment of a single fixed dominant factor.

   theorem moment_le_dominant_factor {κ : Type*} (S : Finset κ)
       (f : ι → κ → ℂ) (i : ι) (B : ℝ)
       (hB : ∀ r ∈ S, ‖∏ k ∈ Finset.univ.erase i, f k r‖ ≤ B) :
       (∑ r ∈ S, ‖∏ k, f k r‖^2) ≤ B^2*(∑ r ∈ S, ‖f i r‖^2) := by
   …

10. theorem OAI.CubicFirstMoment.dominant_cubic_moment_reduction line 186

    Source documentation

    Moment reduction for a fixed dominant cubic factor; all the remaining short arithmetic coefficients and independent twists have been bounded.

    theorem dominant_cubic_moment_reduction {C δ ε : ℝ}
        (hC : 0 < C) (hδ : 0 ≤ δ) (hε : 0 < ε) :
        ∃ M : ℝ, 0 < M ∧ ∀ (F : ShortFactorFamily ι) (j : ℕ) (Y : ℝ) (i : ι)
          (S : Finset Eisenstein), 1 ≤ Y → (∀ p ∈ S, primary p) →
          (∏ k, F.length j k) ≤ C*Y → Y^(1-δ) ≤ F.length j i →
          (∑ p ∈ S, ‖∏ k, F.cubicValue j k p‖^2) ≤
            (M*Y^(δ+ε))^2*(∑ p ∈ S, ‖F.cubicValue j i p‖^2) := by
    …

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

11. theorem OAI.CubicFirstMoment.dominant_mixed_moment_reduction line 200

    Source documentation

    The corresponding moment reduction for a dominant mixed cubic factor.

    theorem dominant_mixed_moment_reduction {C δ ε : ℝ}
        (hC : 0 < C) (hδ : 0 ≤ δ) (hε : 0 < ε) :
        ∃ M : ℝ, 0 < M ∧ ∀ (F : ShortFactorFamily ι) (j : ℕ) (Y : ℝ) (i : ι)
          (S : Finset (Eisenstein × Eisenstein)), 1 ≤ Y →
          (∀ p ∈ S, primary p.1 ∧ primary p.2) →
          (∏ k, F.length j k) ≤ C*Y → Y^(1-δ) ≤ F.length j i →
          (∑ p ∈ S, ‖∏ k, F.mixedValue j k p‖^2) ≤
            (M*Y^(δ+ε))^2*(∑ p ∈ S, ‖F.mixedValue j i p‖^2) := by
    …

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