OAI/NumberTheory/Ostmann/Arithmetic/HarmonicPairIntegral.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.norm_harmonic_pair_integral_le line 9
2. theorem OAI.Ostmann.finite_harmonic_pair_sum_norm line 38

   Source documentation

   A finite signed average is integrated before its norm is bounded. This retains cancellation in the arithmetic coefficient on each giant cell.

   theorem finite_harmonic_pair_sum_norm {A : Type*} [Fintype A]
       (u v r s C : ℝ) (hu : 1 ≤ u) (hr : 1 ≤ r)
       (huv : u ≤ v) (hrs : r ≤ s) (hv : v ≤ u + 1) (hs : s ≤ r + 1)
       (hC : 0 ≤ C) (w : A → ℂ) (F : A → ℝ → ℝ → ℂ)
       (hmeas : ∀ a, Measurable (Function.uncurry (F a)))
       (K : A → ℝ) (hK : ∀ a, 0 ≤ K a)
       (hbound : ∀ a x, x ∈ Set.Ioc u v → ∀ y, y ∈ Set.Ioc r s → ‖F a x y‖ ≤ K a)
       (hmean : ∀ x ∈ Set.Ioc u v, ∀ y ∈ Set.Ioc r s, ‖∑ a, w a * F a x y‖ ≤ C) :
       ‖∑ a, w a * ∫ x in Set.Ioc u v, ∫ y in Set.Ioc r s,
         F a x y / ((x : ℂ) * (y : ℂ))‖ ≤ C / (u * r) := by
   …