MassMajorant.lean`

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Summing over witnesses is an upper bound, including repeated tail primes.

lemma OAI.TotientAsymptotic.sum_image_nonneg_le line 14
def OAI.TotientAsymptotic.basicRemainderFinset line 27
lemma OAI.TotientAsymptotic.mem_basicRemainderFinset line 30
lemma OAI.TotientAsymptotic.prefixDataFinset_eq_image line 34
lemma OAI.TotientAsymptotic.prod_fin_shifted line 41
lemma OAI.TotientAsymptotic.prod_Icc_split_at line 55
def OAI.TotientAsymptotic.remainderReciprocalWeight line 70
lemma OAI.TotientAsymptotic.prefix_reciprocal_majorant line 73
theorem OAI.TotientAsymptotic.mass_le_remainder_sum line 114
Source documentation
The finite prefix mass is bounded by a sum over complete witnesses with the reciprocal totient of the small cofactor separated out.
```
theorem mass_le_remainder_sum {x : ℝ} {H : ℕ} (hPH : P H ≤ H)
    (f : ℝ → ℝ) (hf : ∀ r, f r ≤ 1) :
    M x H f ≤ ∑ η ∈ basicRemainderFinset x H, remainderReciprocalWeight η := by
…
```
Mentions: OAI.TotientAsymptotic.P, OAI.TotientAsymptotic.M, OAI.TotientAsymptotic.basicRemainderFinset, OAI.TotientAsymptotic.remainderReciprocalWeight
def OAI.TotientAsymptotic.fullPrimeTuples line 126
theorem OAI.TotientAsymptotic.mass_le_cofactor_sum_mul_prime_sum line 131
Source documentation
The entire cost of the discrete cofactor separates from the reciprocal prime sum. The latter still retains all the basic simplex restrictions.
```
theorem mass_le_cofactor_sum_mul_prime_sum {x : ℝ} {H : ℕ}
    (hPH : P H < H) (hHm : H ≤ m x) (hs : theta x ∈ Set.Ico (0 : ℝ) 1)
    (f : ℝ → ℝ) (hf : ∀ r, f r ≤ 1) :
    M x H f ≤ (∑ a ∈ Finset.Icc 1 (tailCofactorBound H), (a.totient : ℝ)⁻¹)*
      ∑ p ∈ fullPrimeTuples x H, reciprocalShiftWeight p := by
…
```
Mentions: OAI.TotientAsymptotic.P, OAI.TotientAsymptotic.m, OAI.TotientAsymptotic.theta, OAI.TotientAsymptotic.M, OAI.TotientAsymptotic.a, OAI.TotientAsymptotic.tailCofactorBound, OAI.TotientAsymptotic.fullPrimeTuples, OAI.TotientAsymptotic.reciprocalShiftWeight