Measurable Partition By Local-Slope Bands

This theorem constructs a measurable partition adapted to the local slope of a globally Lipschitz function.

Let $V$ be a second-countable Borel measurable normed additive group, let $f:V\to\mathbb R$ be globally $L$-Lipschitz with $L\in[0,\infty)$, and let $\alpha>0$ be represented by NNReal. Then there exist sets $D_i\subseteq V$ and constants $c_i\in[0,\infty)$, indexed by $i\in\mathbb N$, such that

1. every $D_i$ is measurable;
2. the sets $D_i$ are pairwise disjoint and cover $V$;
3. $c_i\le L+\alpha$ for every $i$;
4. $f$ is $c_i$-Lipschitz on $D_i$;
5. for every $x\in D_i$,

The Lean declaration is exists_partition_readable. The local slope and the final comparison are expressed in ENNReal, while $L$, $\alpha$, and $c_i$ are nonnegative real constants represented by NNReal. This is a technical partition lemma used in patching arguments.

Original Lean declaration header

Within namespace FunctionalInequalities.Energy.LocalSlope. Shown in its original module context. Proof omitted.

theorem exists_partition {f : V → ℝ} {L : ℝ≥0} (hf : LipschitzWith L f) {α : ℝ≥0} (hα : 0 < α) :
    ∃ (D : ℕ → Set V) (c : ℕ → ℝ≥0),
      (∀ i, MeasurableSet (D i)) ∧ Pairwise (Function.onFun Disjoint D) ∧
      (⋃ i, D i) = Set.univ ∧ (∀ i, c i ≤ L + α) ∧
      (∀ i, LipschitzOnWith (c i) f (D i)) ∧
      (∀ i, ∀ x ∈ D i, ((c i : ℝ≥0∞)) ≤ apply f x + (α : ℝ≥0∞))

Module navigation

Module: Energy/Euclidean/Slope/Density.

Definition modules: Energy/LocalSlope/Basic.

Supporting theorems: lowerSemicontinuous_secant.

Previous: exists_patch_of_isCompact · Next: exists_patch.

Source excerpt, lines 567–572 · Frozen source 408915f.