OAI/NumberTheory/Ostmann/Construction/TwoGiantIntegralTransport.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.two_giant_integral_transport line 14

   Source documentation

   Slice comparisons combine against the original outer prior and the ideal inner measure. This introduces neither conditional sampling nor a count of real partition boxes.

   theorem two_giant_integral_transport {A B X Y : Type*} [Fintype A] [Fintype B]
       [MeasurableSpace X] [MeasurableSpace Y]
       (α : A → ℝ) (β : B → ℝ) (x : A → X) (y : B → Y)
       (μ : Measure X) [IsFiniteMeasure μ] (ν : Measure Y) (H : X → Y → ℂ)
       (hβ : ∀ b, 0 ≤ β b) (δ ε : ℝ)
       (hH : ∀ b, Integrable (fun z => H z (y b)) μ)
       (hI : Integrable (fun z => ∫ t, H z t ∂ν) μ)
       (hleft : ∀ b, ‖(∑ a, (α a : ℂ) * H (x a) (y b)) - ∫ z, H z (y b) ∂μ‖ ≤ δ)
       (hright : ∀ᵐ z ∂μ, ‖(∑ b, (β b : ℂ) * H z (y b)) - ∫ t, H z t ∂ν‖ ≤ ε) :
       ‖(∑ b, (β b : ℂ) * ∑ a, (α a : ℂ) * H (x a) (y b)) -
         ∫ z, ∫ t, H z t ∂ν ∂μ‖ ≤ δ * (∑ b, β b) + ε * μ.real Set.univ := by
   …