OAI/Analysis/CoulombTransport/CellOscillation.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem356.lintegral_le_of_same_cells line 14

   Source documentation

   Equal cell-label laws let one compare costs using only their oscillation inside matching cells. The target-cell condition is needed only on a full-measure set.

   theorem lintegral_le_of_same_cells
       {α : Type uAlpha} {β : Type uBeta} {ι : Type uIndex} [MeasurableSpace α] [MeasurableSpace β]
       [MeasurableSpace ι] [MeasurableSingletonClass ι] [Countable ι]
       (μ : Measure α) (ν : Measure β) [IsProbabilityMeasure μ]
       (p : α → ι) (q : β → ι) (hp : Measurable p) (hq : Measurable q)
       (hlaw : Measure.map p μ = Measure.map q ν)
       (f : α → ℝ≥0∞) (g : β → ℝ≥0∞) (ε : ℝ≥0∞)
       (t : Set β) (ht : ∀ᵐ y ∂ν, y ∈ t)
       (hosc : ∀ᵐ x ∂μ, ∀ y ∈ t, p x = q y → f x ≤ g y + ε) :
       (∫⁻ x, f x ∂μ) ≤ (∫⁻ y, g y ∂ν) + ε := by
   …