OAI/NumberTheory/Ostmann/ZeroDensity/GiantDensitySum.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.double_integral_finset_sum line 11
2. theorem OAI.Ostmann.bounded_density_pair_sum line 24

   Source documentation

   The complex residue coefficient is kept signed throughout this interchange.

   theorem bounded_density_pair_sum {A B : Type*} (S : Finset A) (T : Finset B)
       (μ ν : Measure ℝ) [IsFiniteMeasure μ] [IsFiniteMeasure ν]
       (H : ℝ → ℝ → ℂ) (hH : Measurable (Function.uncurry H))
       (K : ℝ) (hK : ∀ x y, ‖H x y‖ ≤ K)
       (α : A → ℝ → ℂ) (β : B → ℝ → ℂ)
       (hα : ∀ a ∈ S, Measurable (α a)) (hβ : ∀ b ∈ T, Measurable (β b))
       (U V : ℝ) (hU : 0 ≤ U) (_hV : 0 ≤ V)
       (hαU : ∀ a ∈ S, ∀ x, ‖α a x‖ ≤ U) (hβV : ∀ b ∈ T, ∀ x, ‖β b x‖ ≤ V)
       (c : A → B → ℂ) :
       (∑ a ∈ S, ∑ b ∈ T,
         ∫ x, ∫ y, c a b * H x y * α a x * β b y ∂ν ∂μ) =
         ∫ x, ∫ y, H x y * (∑ a ∈ S, ∑ b ∈ T, c a b * α a x * β b y) ∂ν ∂μ := by
   …