Translation of finitely supported distributions

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

Komlos.tr u P x = P (x - u). Translation preserves mass and changes the mean by mass P • u, which is u when P is a probability distribution.

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

Translation of a finitely supported function, carrying the weight at x to x + u.

Equations

• Komlos.tr u P = Finsupp.equivMapDomain (Equiv.addRight u) P

@[simp]

theorem Komlos.tr_apply {E : Type u_1} [AddCommGroup E] (u : E) (P : E →₀ ℝ) (x : E) : (tr u P) x = P (x - u)

theorem Komlos.sum_tr {E : Type u_1} [AddCommGroup E] (u : E) (P : E →₀ ℝ) {N : Type u_2} [AddCommMonoid N] (g : E → ℝ → N) : (tr u P).sum g = P.sum fun (x : E) (r : ℝ) => g (x + u) r

theorem Komlos.tr_tr {E : Type u_1} [AddCommGroup E] (a b : E) (P : E →₀ ℝ) : tr a (tr b P) = tr (a + b) P

@[simp]

theorem Komlos.tr_zero {E : Type u_1} [AddCommGroup E] (P : E →₀ ℝ) : tr 0 P = P

theorem Komlos.tr_inf {E : Type u_1} [AddCommGroup E] (u : E) (P Q : E →₀ ℝ) : tr u P ⊓ tr u Q = tr u (P ⊓ Q)

theorem Komlos.mass_tr {E : Type u_1} [AddCommGroup E] (u : E) (P : E →₀ ℝ) : mass (tr u P) = mass P

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

theorem Komlos.mean_tr {E : Type u_1} [AddCommGroup E] [Module ℝ E] (u : E) (P : E →₀ ℝ) : mean (tr u P) = mean P + mass P • u