OAI/NumberTheory/CubicMoment/Decomposition/StoppedPrimeIntervals.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CubicFirstMoment.stoppingPrimeSetTest line 13
2. def OAI.CubicFirstMoment.stoppingSideTest line 19
3. lemma OAI.CubicFirstMoment.primaryPrimeFactors_prime_mul line 23
4. lemma OAI.CubicFirstMoment.stoppingPrimeSetTest_insert_same_bin line 36
5. theorem OAI.CubicFirstMoment.stoppingSideTest_free_prime_same_bin line 47
6. theorem OAI.CubicFirstMoment.failedStage_free_prime_same_bin line 60
7. theorem OAI.CubicFirstMoment.stoppingSideTest_free_distinguished_interval line 74

   Source documentation

   If the free prime is distinguished, the actual stopping inequalities are a single norm interval; the selected divisor remains fixed.

   theorem stoppingSideTest_free_distinguished_interval
       (bin : Eisenstein → ℕ) (ell : ℕ → ℝ) (j k : ℕ) (Z : ℝ)
       {c : Eisenstein} (hc : c ≠ 0) (d p : Eisenstein)
       (hell : 0 < ell j)
       (hS : 0 < primeSurrogate (primaryPrimeFactors d) bin ell) :
       stoppingSideTest bin ell j k Z (c*p) d ↔
         (∀ q ∈ primaryPrimeFactors d, bin q ≤ j) ∧
         (primeBin (primaryPrimeFactors d) bin j).card = k ∧
         Z/(norm c*primeSurrogate (primaryPrimeFactors d) bin ell) ≤ norm p ∧
         norm p < Z*ell j/(norm c*primeSurrogate (primaryPrimeFactors d) bin ell) := by
   …

   Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primeSurrogate, OAI.CubicFirstMoment.primaryPrimeFactors, OAI.CubicFirstMoment.stoppingSideTest, OAI.CubicFirstMoment.primeBin, OAI.CubicFirstMoment.norm

8. lemma OAI.CubicFirstMoment.failedStage_free_distinguished_interval line 87
9. theorem OAI.CubicFirstMoment.sum_stoppingSide_same_bin line 95

   Source documentation

   The selected-prime role can therefore remove its concrete stopping predicate on a fixed bin without a multiplicity or a variation loss.

   theorem sum_stoppingSide_same_bin (S : Finset Eisenstein)
       (bin : Eisenstein → ℕ) (ell : ℕ → ℝ) (j k : ℕ) (Z : ℝ) (r : Eisenstein)
       {c p₀ : Eisenstein} (hc : primary c) (hsc : Squarefree c)
       (hp₀ : p₀ ∈ S) (hS : ∀ p ∈ S, primaryPrime p)
       (hcop : ∀ p ∈ S, ¬p ∣ c) (hbin : ∀ p ∈ S, bin p = bin p₀)
       (F : Eisenstein → ℂ) :
       (∑ p ∈ S with stoppingSideTest bin ell j k Z r (p*c), F p) =
         if stoppingSideTest bin ell j k Z r (p₀*c) then ∑ p ∈ S, F p else 0 := by
   …

   Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.primaryPrime, OAI.CubicFirstMoment.stoppingSideTest