Documentation

MathlibNt.Wu2004MeanValue.OpenIntervals

Open product intervals and the upper-endpoint atom #

The frozen manuscript's B_H has two open endpoints. Wu's prime count on printed p. 220 instead has a closed upper endpoint. Subtracting two Wu counts therefore requires removal of one possible upper-endpoint prime, not an unqualified equality with the open interval.

source
noncomputable def Wu2004MeanValue.openScaledPrimeSet (lo hi : ℝ) (d b m : ℕ) :
Finset ℕ
Equations
Instances For
    Inspect dependencies

    Wu2004MeanValue.openScaledPrimeSet · compiled type and proof/definition references.

    source
    noncomputable def Wu2004MeanValue.upperEndpointSet (hi : ℝ) (d b m : ℕ) :
    Finset ℕ
    Equations
    Instances For
      Inspect dependencies

      Wu2004MeanValue.upperEndpointSet · compiled type and proof/definition references.

      source
      theorem Wu2004MeanValue.scaledPrimeSet_partition (lo hi : ℝ) (d b m : ℕ) (hlo : 0 ≤ lo) (hlt : lo < hi) (hm : 0 < m) :
      scaledPrimeSet hi d b m = scaledPrimeSet lo d b m ∪ openScaledPrimeSet lo hi d b m ∪ upperEndpointSet hi d b m
      Inspect dependencies

      Wu2004MeanValue.scaledPrimeSet_partition · compiled type and proof/definition references.

      source
      theorem Wu2004MeanValue.scaledPrimeCount_partition (lo hi : ℝ) (d b m : ℕ) (hlo : 0 ≤ lo) (hlt : lo < hi) (hm : 0 < m) :
      scaledPrimeCount hi d b m = scaledPrimeCount lo d b m + (openScaledPrimeSet lo hi d b m).card + (upperEndpointSet hi d b m).card
      Inspect dependencies

      Wu2004MeanValue.scaledPrimeCount_partition · compiled type and proof/definition references.

      source
      theorem Wu2004MeanValue.upperEndpointSet_card_le_one (hi : ℝ) (d b m : ℕ) (hm : 0 < m) :
      (upperEndpointSet hi d b m).card ≤ 1
      Inspect dependencies

      Wu2004MeanValue.upperEndpointSet_card_le_one · compiled type and proof/definition references.

      source
      theorem Wu2004MeanValue.openInterval_error_identity (lo hi : ℝ) (d b m : ℕ) (hlo : 0 ≤ lo) (hlt : lo < hi) (hm : 0 < m) :
      ↑(openScaledPrimeSet lo hi d b m).card - (wuLi (hi / ↑m) - wuLi (lo / ↑m)) / ↑d.totient = ebar hi d b m - ebar lo d b m - ↑(upperEndpointSet hi d b m).card

      Exact open-interval error, with no endpoint convention hidden in li.

      Inspect dependencies

      Wu2004MeanValue.openInterval_error_identity · compiled type and proof/definition references.

      source
      theorem Wu2004MeanValue.abs_sum_upperEndpoint_le (S : Finset ℕ) (hi f : ℕ → ℝ) (d b : ℕ) (F : ℝ) (hF : 0 ≤ F) (hpos : ∀ m ∈ S, 0 < m) (hf : ∀ m ∈ S, |f m| ≤ F) :
      |∑ m ∈ S, f m * ↑(upperEndpointSet (hi m) d b m).card| ≤ F * ↑S.card

      One possible upper-endpoint atom per positive coefficient index.

      Inspect dependencies

      Wu2004MeanValue.abs_sum_upperEndpoint_le · compiled type and proof/definition references.