OAI/NumberTheory/TotientAsymptotic/TailBoxAggregation.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Aggregate all discrete tails in a box before measuring the continuous prefix. No factor counting the number of tail witnesses occurs.

  1. def OAI.TotientAsymptotic.tailBoxLift line 15
  2. lemma OAI.TotientAsymptotic.measurableSet_tailBoxLift line 20
  3. lemma OAI.TotientAsymptotic.volume_tailBoxLift line 25
  4. lemma OAI.TotientAsymptotic.volumeReal_tailBoxLift line 40
  5. theorem OAI.TotientAsymptotic.tail_box_aggregation line 49

    Source documentation

    A common prefix envelope for every tail in one unit box costs only the reciprocal prime mass of that box. Summing disjoint tail boxes then gives one full-dimensional volume.

    theorem tail_box_aggregation {R T : ℕ} (K : Finset (Fin T → ℕ))
    (S : (Fin T → ℕ) → Set (Fin R → ℝ))
    (U : (Fin T → ℕ) → Set (Fin R → ℝ)) (C : ℝ)
    (hU : ∀ b ∈ K, MeasurableSet (U b)) (hfin : ∀ b ∈ K, volume (U b) ≠ ⊤)
    (hsub : ∀ b ∈ K, ∀ p ∈ primeBoxTuples b, S p ⊆ U b)
    (hmass : ∀ b ∈ K, (∏ i, unitPrimeWeight (b i)) ≤ C) :
    (∑ p ∈ gridPrimeTuples K, reciprocalShiftWeight p * volume.real (S p)) ≤
      C * volume.real (tailBoxLift K U) := by
…

    Mentions: OAI.TotientAsymptotic.R, OAI.TotientAsymptotic.primeBoxTuples, OAI.TotientAsymptotic.unitPrimeWeight, OAI.TotientAsymptotic.gridPrimeTuples, OAI.TotientAsymptotic.reciprocalShiftWeight, OAI.TotientAsymptotic.tailBoxLift