OAI/MathematicalPhysics/Boltzmann/Branching/AveragedPairIntegrability.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.BoltzmannNonuniqueness.Compactness.uniformIntegrable_average_product line 17
2. theorem OAI.BoltzmannNonuniqueness.Compactness.uniformIntegrable_average_product_of_support line 47

   Source documentation

   Compact velocity support reduces the infinite velocity measure to finite fibres.

   theorem uniformIntegrable_average_product_of_support
       {μ : Measure X} {ν : Measure Y} [SFinite μ] [SFinite ν]
       {s : Set Y} [IsFiniteMeasure (ν.restrict s)]
       {f : ℕ → X × Y → ℝ} (hf : ∀ n, Measurable (f n))
       (hui : UniformIntegrable (fun (n : ℕ) (z : X × (Y × Y)) =>
         f n (z.1,z.2.1)*f n (z.1,z.2.2)) 1 (μ.prod (ν.prod ν)))
       {k l : X × Y → ℝ} (hk : Measurable k) (hl : Measurable l)
       (C D : ℝ≥0) (hC : ∀ z, |k z| ≤ C) (hD : ∀ z, |l z| ≤ D)
       (hks : ∀ x y, y ∉ s → k (x,y) = 0) (hls : ∀ x y, y ∉ s → l (x,y) = 0) :
       UniformIntegrable (fun n x => (∫ v, k (x,v)*f n (x,v) ∂ν)*
         (∫ w, l (x,w)*f n (x,w) ∂ν)) 1 μ := by
   …