OAI/NumberTheory/JointDickman/Probability/TensorBoxRegularity.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Published regularity loss on the actual compact tensor boxes

  1. def OAI.JointDickman.tensorIntervalLower line 12
  2. def OAI.JointDickman.tensorIntervalUpper line 13
  3. theorem OAI.JointDickman.tensorInterval_width line 15
  4. theorem OAI.JointDickman.tensorInterval_order line 25
  5. theorem OAI.JointDickman.tensorInterval_point line 30
  6. theorem OAI.JointDickman.tensorBox_signed_regularity_loss line 47

    Source documentation

    At a fixed dyadic box, the published three-form sieve bound has the normalization 1/(B*T) required before summing the dyadic partition.

    theorem tensorBox_signed_regularity_loss
    (hFord : PublishedInputs.FordUpperSieveInput)
    (hM : PublishedInputs.PrimeReciprocalMertensInput) :
    ∃ K : ℝ, 0 < K ∧ ∀ L : ℕ, ∀ τ : ℝ, 0 < L → 0 < τ →
      ∃ ε : ℕ → ℝ, (∀ B, 0 ≤ ε B) ∧ Tendsto ε atTop (𝓝 0) ∧
        ∀ᶠ B : ℕ in atTop, ∀ (C N T : ℝ) (j : ℕ),
          0 ≤ C → 1 ≤ N → 0 < T → 1 ≤ N/T → j ≠ 0 →
          Real.exp ((1/2 : ℝ)*B) ≤ 3*N →
          Real.exp ((1/2 : ℝ)*B) ≤ 3*(N/T) →
          (17/4 : ℝ)*N ≤ Real.exp ((16/5 : ℝ)*B) →
          ∀ g h : (auxiliaryPrimes B → Bool) → ℝ,
          (∀ x, |g x| ≤ 1) → (∀ x, |h x| ≤ 1) →
…

    Mentions: OAI.JointDickman.PublishedInputs.FordUpperSieveInput, OAI.JointDickman.PublishedInputs.PrimeReciprocalMertensInput, OAI.JointDickman.auxiliaryPrimes