English
If f is nonnegative real-valued and measurable, then the integral of f equals the tail integral against the measure of superlevel sets in t with f.
Русский
Для неотрицательной измеримой функции f существует связь между интегралом и хвостовой мерой суперуровней.
LaTeX
$$$$ \\int f \\, d\\mu = \\int_{0}^{\\infty} \\mu\\{a : f(a) \\ge t\\} dt. $$$$
Lean4
/-- **Monotone convergence theorem**, version with `Measurable` functions. -/
theorem lintegral_iSup {f : ℕ → α → ℝ≥0∞} (hf : ∀ n, Measurable (f n)) (h_mono : Monotone f) :
∫⁻ a, ⨆ n, f n a ∂μ = ⨆ n, ∫⁻ a, f n a ∂μ :=
by
set c : ℝ≥0 → ℝ≥0∞ := (↑)
set F := fun a : α => ⨆ n, f n a
refine le_antisymm ?_ (iSup_lintegral_le _)
rw [lintegral_eq_nnreal]
refine iSup_le fun s => iSup_le fun hsf => ?_
refine ENNReal.le_of_forall_lt_one_mul_le fun a ha => ?_
rcases ENNReal.lt_iff_exists_coe.1 ha with ⟨r, rfl, _⟩
have ha : r < 1 := ENNReal.coe_lt_coe.1 ha
let rs := s.map fun a => r * a
have eq_rs : rs.map c = (const α r : α →ₛ ℝ≥0∞) * map c s := rfl
have eq : ∀ p, rs.map c ⁻¹' { p } = ⋃ n, rs.map c ⁻¹' { p } ∩ {a | p ≤ f n a} :=
by
intro p
rw [← inter_iUnion]; nth_rw 1 [← inter_univ (map c rs ⁻¹' { p })]
refine Set.ext fun x => and_congr_right fun hx => (iff_of_eq (true_iff _)).2 ?_
by_cases p_eq : p = 0
· simp [p_eq]
simp only [coe_map, mem_preimage, Function.comp_apply, mem_singleton_iff] at hx
subst hx
have : r * s x ≠ 0 := by rwa [Ne, ← ENNReal.coe_eq_zero]
have : s x ≠ 0 := right_ne_zero_of_mul this
have : (rs.map c) x < ⨆ n : ℕ, f n x :=
by
refine lt_of_lt_of_le (ENNReal.coe_lt_coe.2 ?_) (hsf x)
suffices r * s x < 1 * s x by simpa
exact mul_lt_mul_of_pos_right ha (pos_iff_ne_zero.2 this)
rcases lt_iSup_iff.1 this with ⟨i, hi⟩
exact mem_iUnion.2 ⟨i, le_of_lt hi⟩
have mono : ∀ r : ℝ≥0∞, Monotone fun n => rs.map c ⁻¹' { r } ∩ {a | r ≤ f n a} :=
by
intro r i j h
refine inter_subset_inter_right _ ?_
simp_rw [subset_def, mem_setOf]
intro x hx
exact le_trans hx (h_mono h x)
have h_meas : ∀ n, MeasurableSet {a : α | map c rs a ≤ f n a} := fun n =>
measurableSet_le (SimpleFunc.measurable _) (hf n)
calc
(r : ℝ≥0∞) * (s.map c).lintegral μ = ∑ r ∈ (rs.map c).range, r * μ (rs.map c ⁻¹' { r }) := by
rw [← const_mul_lintegral, eq_rs, SimpleFunc.lintegral]
_ = ∑ r ∈ (rs.map c).range, r * μ (⋃ n, rs.map c ⁻¹' { r } ∩ {a | r ≤ f n a}) := by simp only [(eq _).symm]
_ = ∑ r ∈ (rs.map c).range, ⨆ n, r * μ (rs.map c ⁻¹' { r } ∩ {a | r ≤ f n a}) :=
(Finset.sum_congr rfl fun x _ => by rw [(mono x).measure_iUnion, ENNReal.mul_iSup])
_ = ⨆ n, ∑ r ∈ (rs.map c).range, r * μ (rs.map c ⁻¹' { r } ∩ {a | r ≤ f n a}) :=
by
refine ENNReal.finsetSum_iSup_of_monotone fun p i j h ↦ ?_
gcongr _ * μ ?_
exact mono p h
_ ≤ ⨆ n : ℕ, ((rs.map c).restrict {a | (rs.map c) a ≤ f n a}).lintegral μ :=
by
gcongr with n
rw [restrict_lintegral _ (h_meas n)]
refine le_of_eq (Finset.sum_congr rfl fun r _ => ?_)
congr 2 with a
refine and_congr_right ?_
simp +contextual
_ ≤ ⨆ n, ∫⁻ a, f n a ∂μ := by
simp only [← SimpleFunc.lintegral_eq_lintegral]
gcongr with n a
simp only [map_apply] at h_meas
simp only [coe_map, restrict_apply _ (h_meas _), (· ∘ ·)]
exact indicator_apply_le id
