OAI/NumberTheory/TotientAsymptotic/WitnessAggregation.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TotientAsymptotic.witnessPrimeRegion line 15
2. def OAI.TotientAsymptotic.witnessBoxRegion line 19
3. lemma OAI.TotientAsymptotic.witnessPrimeRegion_eq line 23
4. theorem OAI.TotientAsymptotic.witness_tail_box_aggregation line 39

   Source documentation

   Aggregation counts the prime mass of each tail box once. The bound has no factor equal to the number of witnesses in the box.

   theorem witness_tail_box_aggregation {H R a : ℕ} {s : ℝ}
       (W : Finset (TailDatum H)) (S : TailDatum H → Set (Fin R → ℝ))
       (K : Finset (Fin (H-P H) → ℕ)) (T : Set (Fin (R+(H-P H)) → ℝ)) (C : ℝ)
       (hC : 0 ≤ C) (hW : ∀ η ∈ W, IsWitness H s η) (hcof : ∀ η ∈ W, η.cofactor=a)
       (hS : ∀ η ∈ W, MeasurableSet (S η)) (hT : volume T ≠ ⊤)
       (hcover : ∀ η ∈ W, tailPrimeVector η ∈ gridPrimeTuples K)
       (hbox : ∀ b ∈ K, (∏ i, unitPrimeWeight (b i)) ≤ C)
       (henclose : ∀ η ∈ W, ∀ b ∈ K, tailVector η ∈ unitGridCell b →
         ∀ u ∈ S η, ∀ v ∈ unitGridCell b, joinCoordinates R (H-P H) (u,v) ∈ T) :
       (∑ η ∈ W, reciprocalShiftWeight (tailPrimeVector η)*volume.real (S η)) ≤ C*volume.real T := by
   …

   Mentions: OAI.TotientAsymptotic.R, OAI.TotientAsymptotic.a, OAI.TotientAsymptotic.TailDatum, OAI.TotientAsymptotic.P, OAI.TotientAsymptotic.IsWitness, OAI.TotientAsymptotic.tailPrimeVector, OAI.TotientAsymptotic.gridPrimeTuples, OAI.TotientAsymptotic.unitPrimeWeight, OAI.TotientAsymptotic.tailVector, OAI.TotientAsymptotic.unitGridCell, OAI.TotientAsymptotic.joinCoordinates, OAI.TotientAsymptotic.reciprocalShiftWeight