English
Given f with range in [a,b], one can partition [a,b] into N pieces so that on the i-th piece f lies in (a+ε i, a+ε(i+1)], yielding a disjoint decomposition of the support.
Русский
Если диапазон f находится в [a,b], существует разбиение [a,b] на N полос так, чтобы на i-й полосе f лежал в (a+ε i, a+ε (i+1)], что даёт разложение опоры на непересекающиеся части.
LaTeX
$$$\\exists E: Fin N \\to \\mathcal P(X):\\ tsupport f = \\bigcup_j E_j,\\ E_j\\cap E_k=\\emptyset\\ (j\\neq k)\\land\\dots$$$
Lean4
/-- Given `f : C_c(X, ℝ)` such that `range f ⊆ [a, b]` we obtain a partition of the support of `f`
determined by partitioning `[a, b]` into `N` pieces. -/
theorem range_cut_partition (f : C_c(X, ℝ)) (a : ℝ) {ε : ℝ} (hε : 0 < ε) (N : ℕ) (hf : range f ⊆ Ioo a (a + N * ε)) :
∃ (E : Fin N → Set X),
tsupport f = ⋃ j, E j ∧
univ.PairwiseDisjoint E ∧
(∀ n : Fin N, ∀ x ∈ E n, a + ε * n < f x ∧ f x ≤ a + ε * (n + 1)) ∧ ∀ n : Fin N, MeasurableSet (E n) :=
by
let b := a + N * ε
let y : Fin N → ℝ := fun n ↦
a +
ε *
(n + 1)
-- By definition `y n` and `y m` are separated by at least `ε`.
have hy {n m : Fin N} (h : n < m) : y n + ε ≤ y m :=
calc
_ ≤ a + ε * m + ε := by
exact add_le_add_three (by rfl) ((mul_le_mul_iff_of_pos_left hε).mpr (by norm_cast)) (by rfl)
_ = _ := by dsimp [y];
rw [mul_add, mul_one, add_assoc]
-- Define `E n` as the inverse image of the interval `(y n - ε, y n]`.
let E (n : Fin N) := (f ⁻¹' Ioc (y n - ε) (y n)) ∩ (tsupport f)
use E
refine ⟨?_, ?_, ?_, ?_⟩
· -- The sets `E n` are a partition of the support of `f`.
have partition_aux : range f ⊆ ⋃ n, Ioc (y n - ε) (y n) :=
calc
_ ⊆ Ioc (a + (0 : ℕ) * ε) (a + N * ε) := by
intro _ hz
simpa using Ioo_subset_Ioc_self (hf hz)
_ ⊆ ⋃ i ∈ Finset.range N, Ioc (a + ↑i * ε) (a + ↑(i + 1) * ε) := (Ioc_subset_biUnion_Ioc N (fun n ↦ a + n * ε))
_ ⊆ _ := by
intro z
simp only [Finset.mem_range, mem_iUnion, mem_Ioc, forall_exists_index, and_imp, y]
refine fun n hn _ _ ↦ ⟨⟨n, hn⟩, ⟨by linarith, by simp_all [mul_comm ε _]⟩⟩
simp only [E, ← iUnion_inter, ← preimage_iUnion, eq_comm (a := tsupport _), inter_eq_right]
exact fun x _ ↦ partition_aux (mem_range_self x)
· -- The sets `E n` are pairwise disjoint.
intro m _ n _ hmn
apply Disjoint.preimage
simp_rw [mem_preimage, mem_Ioc, disjoint_left]
intro x hx
rw [mem_setOf_eq, and_assoc] at hx
simp_rw [mem_setOf_eq, not_and_or, not_lt, not_le, or_assoc]
rcases (by cutsat : m < n ∨ n < m) with hc | hc
· left
exact le_trans hx.2.1 (le_tsub_of_add_le_right (hy hc))
· right; left
exact lt_of_le_of_lt (le_tsub_of_add_le_right (hy hc)) hx.1
· -- Upper and lower bound on `f x` follow from the definition of `E n` .
intro _ _ hx
simp only [mem_inter_iff, mem_preimage, mem_Ioc, E, y] at hx
constructor <;> linarith
· exact fun _ ↦ (f.1.measurable measurableSet_Ioc).inter measurableSet_closure
