English
A measure of a set can be decomposed into pieces where a function f does not fluctuate by more than t, using preimages of 0, ∞ and a telescoping sum over Ico of powers of t.
Русский
Мера множества разлагается на части, где функция f не изменяется более чем на t, через предобразные 0, ∞ и сумму по Ico степеней t.
LaTeX
$$μ s = μ (s ∩ f⁻¹'{0}) + μ (s ∩ f⁻¹' {∞}) + ∑' n : ℤ, μ (s ∩ f⁻¹' Ico ((t)^n) ((t)^(n+1)))$$
Lean4
/-- One can cut out `ℝ≥0∞` into the sets `{0}`, `Ico (t^n) (t^(n+1))` for `n : ℤ` and `{∞}`. This
gives a way to compute the measure of a set in terms of sets on which a given function `f` does not
fluctuate by more than `t`. -/
theorem measure_eq_measure_preimage_add_measure_tsum_Ico_zpow {α : Type*} {mα : MeasurableSpace α} (μ : Measure α)
{f : α → ℝ≥0∞} (hf : Measurable f) {s : Set α} (hs : MeasurableSet s) {t : ℝ≥0} (ht : 1 < t) :
μ s = μ (s ∩ f ⁻¹' {0}) + μ (s ∩ f ⁻¹' {∞}) + ∑' n : ℤ, μ (s ∩ f ⁻¹' Ico ((t : ℝ≥0∞) ^ n) ((t : ℝ≥0∞) ^ (n + 1))) :=
by
have A : μ s = μ (s ∩ f ⁻¹' {0}) + μ (s ∩ f ⁻¹' Ioi 0) :=
by
rw [← measure_union]
·
rw [← inter_union_distrib_left, ← preimage_union, singleton_union, Ioi_insert, ← _root_.bot_eq_zero, Ici_bot,
preimage_univ, inter_univ]
· exact disjoint_singleton_left.mpr notMem_Ioi_self |>.preimage f |>.inter_right' s |>.inter_left' s
· exact hs.inter (hf measurableSet_Ioi)
have B : μ (s ∩ f ⁻¹' Ioi 0) = μ (s ∩ f ⁻¹' {∞}) + μ (s ∩ f ⁻¹' Ioo 0 ∞) :=
by
rw [← measure_union]
· rw [← inter_union_distrib_left]
congr
ext x
simp only [mem_singleton_iff, mem_union, mem_Ioo, mem_Ioi, mem_preimage]
obtain (H | H) : f x = ∞ ∨ f x < ∞ := eq_or_lt_of_le le_top
· simp only [H, or_false, ENNReal.zero_lt_top, not_top_lt, and_false]
· simp only [H, H.ne, and_true, false_or]
· refine disjoint_left.2 fun x hx h'x => ?_
have : f x < ∞ := h'x.2.2
exact lt_irrefl _ (this.trans_le (le_of_eq hx.2.symm))
· exact hs.inter (hf measurableSet_Ioo)
have C : μ (s ∩ f ⁻¹' Ioo 0 ∞) = ∑' n : ℤ, μ (s ∩ f ⁻¹' Ico ((t : ℝ≥0∞) ^ n) ((t : ℝ≥0∞) ^ (n + 1))) :=
by
rw [← measure_iUnion, ENNReal.Ioo_zero_top_eq_iUnion_Ico_zpow (ENNReal.one_lt_coe_iff.2 ht) ENNReal.coe_ne_top,
preimage_iUnion, inter_iUnion]
· intro i j hij
wlog h : i < j generalizing i j
· exact (this hij.symm (hij.lt_or_gt.resolve_left h)).symm
refine disjoint_left.2 fun x hx h'x => lt_irrefl (f x) ?_
calc
f x < (t : ℝ≥0∞) ^ (i + 1) := hx.2.2
_ ≤ (t : ℝ≥0∞) ^ j := (ENNReal.zpow_le_of_le (ENNReal.one_le_coe_iff.2 ht.le) h)
_ ≤ f x := h'x.2.1
· intro n
exact hs.inter (hf measurableSet_Ico)
rw [A, B, C, add_assoc]
