MassTailSupport.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Fixed finite tail support and exact grouping of the actual prefix mass.

lemma OAI.TotientAsymptotic.witness_w_pos line 15
lemma OAI.TotientAsymptotic.prefix_tail_support line 22
def OAI.TotientAsymptotic.prefixDataFinset line 36
lemma OAI.TotientAsymptotic.mem_prefixDataFinset line 39
def OAI.TotientAsymptotic.prefixPrimeFiber line 43
lemma OAI.TotientAsymptotic.mem_prefixPrimeFiber line 46
lemma OAI.TotientAsymptotic.mass_eq_sum_prefixData line 58
theorem OAI.TotientAsymptotic.mass_eq_finite_tail_sum line 73
Source documentation
Each prime prefix is included once in its tail-totient fiber, regardless of how many basic witnesses it admits. The outer support is fixed by H.
```
theorem mass_eq_finite_tail_sum {x : ℝ} {H : ℕ}
    (hPH : P H < H) (hHm : H ≤ m x) (hs : theta x ∈ Set.Ico (0 : ℝ) 1)
    (f : ℝ → ℝ) :
    M x H f = ∑ d ∈ Finset.Icc 1 (tailValueBound H),
      f ((ell d : ℝ)/d)/d * ∑ p ∈ prefixPrimeFiber x H d, reciprocalShiftWeight p := by
…
```
Mentions: OAI.TotientAsymptotic.P, OAI.TotientAsymptotic.m, OAI.TotientAsymptotic.theta, OAI.TotientAsymptotic.M, OAI.TotientAsymptotic.tailValueBound, OAI.TotientAsymptotic.ell, OAI.TotientAsymptotic.prefixPrimeFiber, OAI.TotientAsymptotic.reciprocalShiftWeight