OAI/NumberTheory/JointDickman/Amplification/SignedRegularityLoss.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.JointDickman.coefficientTripleRegular line 12
2. theorem OAI.JointDickman.coefficientTripleRegular_swap line 17
3. theorem OAI.JointDickman.coefficientForm_regular_iff line 21
4. def OAI.JointDickman.discardedRelationWeight line 32
5. def OAI.JointDickman.signedDiscardedCoefficientMass line 35
6. theorem OAI.JointDickman.discardedRelationWeight_neg line 39
7. theorem OAI.JointDickman.signedDiscardedCoefficientMass_neg line 47
8. theorem OAI.JointDickman.discardedRelationWeight_nat line 53
9. theorem OAI.JointDickman.discardedCoefficientWeight_nonneg line 64
10. theorem OAI.JointDickman.signedDiscardedCoefficientMass_nat_le line 71
11. theorem OAI.JointDickman.signed_coefficient_regularity_loss line 89

    Source documentation

    Manuscript (9) on the actual signed support a - b = jc.

    theorem signed_coefficient_regularity_loss
        (hFord : PublishedInputs.FordUpperSieveInput)
        (hM : PublishedInputs.PrimeReciprocalMertensInput)
        {δ : ℝ} (hδ : 0 < δ) (hδ32 : δ ≤ 32) :
        ∃ K : ℝ, 0 < K ∧ ∀ (L : ℕ) (τ : ℝ), 0 < L → 0 < τ →
          ∃ ε : ℕ → ℝ, (∀ B, 0 ≤ ε B) ∧ Tendsto ε atTop (𝓝 0) ∧
            ∀ᶠ B : ℕ in atTop, ∀ (C : ℝ) (j : ℤ) (l₁ r₁ l₂ r₂ : ℕ),
              0 ≤ C → j ≠ 0 → l₁ ≤ r₁ → l₂ ≤ r₂ →
              Real.exp (δ * B) ≤ (r₁ : ℝ) - l₁ → Real.exp (δ * B) ≤ (r₂ : ℝ) - l₂ →
              signedDiscardedCoefficientMass B L τ C j (Ico l₁ r₁) (Ico l₂ r₂) ≤
                K * ((r₁ : ℝ) - l₁) * ((r₂ : ℝ) - l₂) * singularFactor 24 j.natAbs *
                  (ε B + Real.exp (-(1 / 10 : ℝ) * C)) := by
    …

    Mentions: OAI.JointDickman.PublishedInputs.FordUpperSieveInput, OAI.JointDickman.PublishedInputs.PrimeReciprocalMertensInput, OAI.JointDickman.signedDiscardedCoefficientMass, OAI.JointDickman.singularFactor