OAI/NumberTheory/JointDickman/Counting/PeriodicProfileMeans.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.JointDickman.real_periodic_prefix_error line 11
2. theorem OAI.JointDickman.real_periodic_interval_error line 40
3. theorem OAI.JointDickman.finite_nat_convex_eq_interval line 55
4. theorem OAI.JointDickman.periodic_interval_profile_bound line 72

   Source documentation

   Only the boundary error depends on the number of cutoff profiles. The main term retains the uniform mean bound E.

   theorem periodic_interval_profile_bound {q : ℕ} [NeZero q]
       {α : Type*} [Fintype α] (F : α → ZMod q → ℝ)
       {C E : ℝ} (hC : 0 ≤ C) (hF : ∀ a r, |F a r| ≤ C)
       (hmean : ∀ a, (∑ r, F a r)/(q : ℝ) ≤ E)
       (profile : ℕ → α)
       (hconv : ∀ u v w, u ≤ v → v ≤ w → profile u = profile w → profile v = profile u)
       (N : ℕ) :
       (∑ n ∈ range N, F (profile n) n) ≤
         (N : ℝ)*E+(Fintype.card α : ℝ)*(2*q*C) := by
   …