OAI/NumberTheory/TotientAsymptotic/TailVolume.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Exact finite-tail intersection volumes, before prime-box approximation.

  1. lemma OAI.TotientAsymptotic.prod_g_shifted line 14
  2. def OAI.TotientAsymptotic.tailPrefixRegion line 29
  3. def OAI.TotientAsymptotic.tailIntersection line 34
  4. def OAI.TotientAsymptotic.tailBudget line 38
  5. lemma OAI.TotientAsymptotic.tailIntersection_eq line 41
  6. theorem OAI.TotientAsymptotic.volume_tailIntersection line 51

    Source documentation

    The intersection-volume identity with the tail budget indexed by the prefix. This form avoids a reversed-index convention in subsequent finite sums.

    theorem volume_tailIntersection (x : ℝ) (H : ℕ) (T : Finset (TailDatum H))
    (hT : T.Nonempty) (hR : 0 < R x H) (hB : 0 < B x) :
    volume (tailIntersection x H T) =
      ENNReal.ofReal (G x (R x H) * (max (1-tailBudget x H T/B x) 0)^(R x H)) := by
…

    Mentions: OAI.TotientAsymptotic.TailDatum, OAI.TotientAsymptotic.R, OAI.TotientAsymptotic.B, OAI.TotientAsymptotic.tailIntersection, OAI.TotientAsymptotic.G, OAI.TotientAsymptotic.tailBudget