Splitting a distribution

Adapted for Lean Pool by changing module paths and selecting explicit imports.

Komlos.split v P is supported on E × {0, 1}. At (x, 0) it has half the maximum of P (x + v) and P (x - v); at (x, 1) it has half their minimum.

Splitting preserves mass. For a probability distribution, the first component of the mean is unchanged and the last component is Komlos.splitBit v P. Claim 3.2, Komlos.shiftDist_split_le, bounds the shift distance in direction (u, 0) by the original shift distance in direction u.

def Komlos.incl {E : Type u_1} (b : ℝ) : E ↪ E × ℝ

The embedding of E as the slice at height b of E × ℝ.

Equations

• Komlos.incl b = { toFun := fun (x : E) => (x, b), inj' := ⋯ }

@[simp]

theorem Komlos.incl_apply {E : Type u_1} (b : ℝ) (x : E) : (incl b) x = (x, b)

theorem Komlos.embDomain_incl_self {E : Type u_1} (b : ℝ) (A : E →₀ ℝ) (x : E) : (Finsupp.embDomain (incl b) A) (x, b) = A x

theorem Komlos.embDomain_incl_of_ne {E : Type u_1} {b c : ℝ} (hbc : b ≠ c) (A : E →₀ ℝ) (x : E) : (Finsupp.embDomain (incl c) A) (x, b) = 0

theorem Komlos.sum_smul_mk {E : Type u_1} [AddCommGroup E] [Module ℝ E] (A : E →₀ ℝ) (c : ℝ) : (A.sum fun (x : E) (r : ℝ) => r • (x, c)) = (mean A, mass A * c)

theorem Komlos.sum_smul_inl {E : Type u_1} [AddCommGroup E] [Module ℝ E] {ι : Type u_2} (s : Finset ι) (ε : ι → ℝ) (v : ι → E) : ∑ i ∈ s, ε i • (v i, 0) = (∑ i ∈ s, ε i • v i, 0)

noncomputable def Komlos.split {E : Type u_1} [AddCommGroup E] (v : E) (P : E →₀ ℝ) : E × ℝ →₀ ℝ

Assign half of max (P (x + v)) (P (x - v)) to (x, 0) and half of the minimum to (x, 1).

Equations

• Komlos.split v P = Finsupp.embDomain (Komlos.incl 0) (2⁻¹ • (Komlos.tr (-v) P ⊔ Komlos.tr v P)) + Finsupp.embDomain (Komlos.incl 1) (2⁻¹ • (Komlos.tr (-v) P ⊓ Komlos.tr v P))

@[simp]

theorem Komlos.split_apply_zero {E : Type u_1} [AddCommGroup E] (v : E) (P : E →₀ ℝ) (x : E) : (split v P) (x, 0) = 2⁻¹ * max (P (x + v)) (P (x - v))

@[simp]

theorem Komlos.split_apply_one {E : Type u_1} [AddCommGroup E] (v : E) (P : E →₀ ℝ) (x : E) : (split v P) (x, 1) = 2⁻¹ * min (P (x + v)) (P (x - v))

theorem Komlos.split_apply_of_ne {E : Type u_1} [AddCommGroup E] (v : E) (P : E →₀ ℝ) {b : ℝ} (h0 : b ≠ 0) (h1 : b ≠ 1) (x : E) : (split v P) (x, b) = 0

theorem Komlos.snd_eq_zero_or_one_of_mem_support_split {E : Type u_1} [AddCommGroup E] {v : E} {P : E →₀ ℝ} {y : E × ℝ} (hy : y ∈ (split v P).support) : y.2 = 0 ∨ y.2 = 1

theorem Komlos.mk_zero_mem_support_split {E : Type u_1} [AddCommGroup E] {P : E →₀ ℝ} (hP : ∀ (x : E), 0 ≤ P x) (v x : E) : (x, 0) ∈ (split v P).support ↔ x + v ∈ P.support ∨ x - v ∈ P.support

theorem Komlos.mk_one_mem_support_split {E : Type u_1} [AddCommGroup E] {P : E →₀ ℝ} (hP : ∀ (x : E), 0 ≤ P x) (v x : E) : (x, 1) ∈ (split v P).support ↔ x + v ∈ P.support ∧ x - v ∈ P.support

theorem Komlos.split_nonneg {E : Type u_1} [AddCommGroup E] {P : E →₀ ℝ} (hP : ∀ (x : E), 0 ≤ P x) (v : E) (y : E × ℝ) : 0 ≤ (split v P) y

theorem Komlos.sum_split {E : Type u_1} [AddCommGroup E] {N : Type u_2} [AddCommMonoid N] (v : E) (P : E →₀ ℝ) (g : E × ℝ → ℝ → N) (h0 : ∀ (y : E × ℝ), g y 0 = 0) (hadd : ∀ (y : E × ℝ) (r s : ℝ), g y (r + s) = g y r + g y s) : (split v P).sum g = ((2⁻¹ • (tr (-v) P ⊔ tr v P)).sum fun (x : E) (r : ℝ) => g (x, 0) r) + (2⁻¹ • (tr (-v) P ⊓ tr v P)).sum fun (x : E) (r : ℝ) => g (x, 1) r

theorem Komlos.mass_split {E : Type u_1} [AddCommGroup E] (v : E) (P : E →₀ ℝ) : mass (split v P) = mass P

theorem Komlos.IsDist.split {E : Type u_1} [AddCommGroup E] {P : E →₀ ℝ} (hP : IsDist P) (v : E) : IsDist (Komlos.split v P)

noncomputable def Komlos.splitBit {E : Type u_1} [AddCommGroup E] (v : E) (P : E →₀ ℝ) : ℝ

The mass on the slice with last coordinate 1 after splitting.

Equations

• Komlos.splitBit v P = 2⁻¹ * Komlos.overlap (Komlos.tr (-v) P) (Komlos.tr v P)

theorem Komlos.splitBit_eq {E : Type u_1} [AddCommGroup E] [Module ℝ E] {P : E →₀ ℝ} (hP : IsDist P) (v : E) : splitBit v P = 2⁻¹ * (1 - shiftDist P (2 • v))

theorem Komlos.mean_split {E : Type u_1} [AddCommGroup E] [Module ℝ E] (v : E) (P : E →₀ ℝ) : mean (split v P) = (mean P, splitBit v P)

theorem Komlos.split_mono {E : Type u_1} [AddCommGroup E] (v : E) {P Q : E →₀ ℝ} (h : P ≤ Q) : split v P ≤ split v Q

theorem Komlos.split_tr {E : Type u_1} [AddCommGroup E] (v u : E) (P : E →₀ ℝ) : split v (tr u P) = tr (u, 0) (split v P)

Splitting commutes with translation in the directions coming from E.

theorem Komlos.shiftDist_split_le {E : Type u_1} [AddCommGroup E] {P : E →₀ ℝ} (hP : IsDist P) (u v : E) : shiftDist (split v P) (u, 0) ≤ shiftDist P u

Claim 3.2: splitting does not increase shift distances in directions coming from E.