BoundaryAggregation.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Tail-box aggregation of all prefix boxes crossing a witness boundary.

theorem OAI.TotientAsymptotic.witness_boundary_aggregation line 19

Source documentation

A simultaneous boundary estimate for any measurable union of crossing boxes, uniformly in the witnesses and the number of coordinates.

theorem witness_boundary_aggregation (hbox : FordUnitPrimeBoxInput)
    (hmertens : MertensProductInput) (hren : FordRenewalInput)
    (hford : FordCoordinateConcentrationInput) :
    ∃ ε : ℕ → ℝ, Tendsto ε atTop (nhds 0) ∧
      ∀ᶠ H : ℕ in atTop, ∀ᶠ x : ℝ in atTop,
      ∀ W : Finset (TailDatum H), (∀ η ∈ W, IsWitness H (theta x) η) →
      ∀ S : TailDatum H → Set (Fin (R x H) → ℝ), (∀ η ∈ W, MeasurableSet (S η)) →
      (∀ η ∈ W, ∀ u ∈ S η,
        ∃ u₀ ∈ perturbedTailPrefixRegion x H η ∩ prefixBandRegion x H,
          (∀ i, |u₀ i-u i| ≤ 1) ∧
          ∃ w, w ∉ perturbedTailPrefixRegion x H η ∩ prefixBandRegion x H ∧
            ∀ i, |w i-u i| ≤ 1) →
…

Mentions: OAI.TotientAsymptotic.FordUnitPrimeBoxInput, OAI.TotientAsymptotic.MertensProductInput, OAI.TotientAsymptotic.FordRenewalInput, OAI.TotientAsymptotic.FordCoordinateConcentrationInput, OAI.TotientAsymptotic.TailDatum, OAI.TotientAsymptotic.IsWitness, OAI.TotientAsymptotic.theta, OAI.TotientAsymptotic.R, OAI.TotientAsymptotic.perturbedTailPrefixRegion, OAI.TotientAsymptotic.prefixBandRegion, OAI.TotientAsymptotic.w