OAI/NumberTheory/TotientAsymptotic/TailBoxCoordinates.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TotientAsymptotic.joinCoordinates line 13
2. lemma OAI.TotientAsymptotic.joinCoordinates_left line 18
3. lemma OAI.TotientAsymptotic.joinCoordinates_right line 24
4. lemma OAI.TotientAsymptotic.joinCoordinates_preserves_volume line 30
5. lemma OAI.TotientAsymptotic.volume_joinCoordinates_image line 35
6. theorem OAI.TotientAsymptotic.tail_box_aggregation_enclosure line 45

   Source documentation

   A full-dimensional enclosure bounds the aggregated weighted prefix volumes without multiplying by the number of tail witnesses.

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

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