OAI/NumberTheory/Ostmann/Construction/GiantDiscreteTransport.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.primeResidueAtom line 12
2. theorem OAI.Ostmann.primeResidueAtom_nonneg line 15
3. theorem OAI.Ostmann.complexPrimeInterval_subtype line 19
4. theorem OAI.Ostmann.complexIntegerInterval_subtype line 30
5. theorem OAI.Ostmann.primeResidueAtom_subtype_mass line 41
6. theorem OAI.Ostmann.prime_pair_integral_transport line 49

   Source documentation

   The original finite sums are transported directly. All real measurability and integrability requirements are discharged from the bounded kernel.

   theorem prime_pair_integral_transport (q a b : ℕ) (u v r s : ℝ)
       (μ ν : Measure ℝ) [IsFiniteMeasure μ] [IsFiniteMeasure ν]
       (H : ℝ → ℝ → ℂ) (hH : Measurable (Function.uncurry H))
       (K : ℝ) (hK : ∀ x y, ‖H x y‖ ≤ K) (δ ε : ℝ)
       (hleft : ∀ y, ‖complexPrimeInterval q a u v (fun x => H x y) - ∫ x, H x y ∂μ‖ ≤ δ)
       (hright : ∀ x, ‖complexPrimeInterval q b r s (H x) - ∫ y, H x y ∂ν‖ ≤ ε) :
       ‖complexPrimeInterval q b r s (fun y => complexPrimeInterval q a u v (fun x => H x y)) -
         ∫ x, ∫ y, H x y ∂ν ∂μ‖ ≤
         δ * reciprocalPrimeInterval q b (Real.exp r) (Real.exp s) + ε * μ.real Set.univ := by
   …

   Mentions: OAI.Ostmann.complexPrimeInterval, OAI.Ostmann.reciprocalPrimeInterval

7. theorem OAI.Ostmann.mixed_pair_integral_transport line 72