Pushforward along injective additive maps

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

Pushforward along an injective additive map preserves mass, total variation distance, and shift distance. These results allow the integer-lattice distribution to be mapped to the real grid by g ↦ g / N when N > 0.

noncomputable def Komlos.push {E : Type u_1} {F : Type u_2} [AddCommGroup E] [AddCommGroup F] (e : E →+ F) (he : Function.Injective ⇑e) (P : E →₀ ℝ) : F →₀ ℝ

Push a finitely supported function forward along an injective additive map.

Equations

• Komlos.push e he P = Finsupp.embDomain { toFun := ⇑e, inj' := he } P

@[simp]

theorem Komlos.push_apply {E : Type u_1} {F : Type u_2} [AddCommGroup E] [AddCommGroup F] {e : E →+ F} {he : Function.Injective ⇑e} (P : E →₀ ℝ) (x : E) : (push e he P) (e x) = P x

theorem Komlos.sum_push {E : Type u_1} {F : Type u_2} [AddCommGroup E] [AddCommGroup F] {e : E →+ F} {he : Function.Injective ⇑e} {N : Type u_3} [AddCommMonoid N] (P : E →₀ ℝ) (g : F → ℝ → N) : (push e he P).sum g = P.sum fun (x : E) (r : ℝ) => g (e x) r

theorem Komlos.support_push {E : Type u_1} {F : Type u_2} [AddCommGroup E] [AddCommGroup F] {e : E →+ F} {he : Function.Injective ⇑e} (P : E →₀ ℝ) : (push e he P).support = Finset.map { toFun := ⇑e, inj' := he } P.support

theorem Komlos.mass_push {E : Type u_1} {F : Type u_2} [AddCommGroup E] [AddCommGroup F] {e : E →+ F} {he : Function.Injective ⇑e} (P : E →₀ ℝ) : mass (push e he P) = mass P

theorem Komlos.IsDist.push {E : Type u_1} {F : Type u_2} [AddCommGroup E] [AddCommGroup F] {e : E →+ F} {he : Function.Injective ⇑e} {P : E →₀ ℝ} (hP : IsDist P) : IsDist (Komlos.push e he P)

theorem Komlos.push_sub {E : Type u_1} {F : Type u_2} [AddCommGroup E] [AddCommGroup F] {e : E →+ F} {he : Function.Injective ⇑e} (P Q : E →₀ ℝ) : push e he (P - Q) = push e he P - push e he Q

theorem Komlos.tvDist_push {E : Type u_1} {F : Type u_2} [AddCommGroup E] [AddCommGroup F] {e : E →+ F} {he : Function.Injective ⇑e} (P Q : E →₀ ℝ) : tvDist (push e he P) (push e he Q) = tvDist P Q

theorem Komlos.tr_push {E : Type u_1} {F : Type u_2} [AddCommGroup E] [AddCommGroup F] {e : E →+ F} {he : Function.Injective ⇑e} (u : E) (P : E →₀ ℝ) : tr (e u) (push e he P) = push e he (tr u P)

theorem Komlos.shiftDist_push {E : Type u_1} {F : Type u_2} [AddCommGroup E] [AddCommGroup F] {e : E →+ F} {he : Function.Injective ⇑e} (u : E) (P : E →₀ ℝ) : shiftDist (push e he P) (e u) = shiftDist P u

theorem Komlos.mean_push {E : Type u_1} {F : Type u_2} [AddCommGroup E] [AddCommGroup F] {e : E →+ F} {he : Function.Injective ⇑e} [Module ℝ F] (P : E →₀ ℝ) : mean (push e he P) = P.sum fun (x : E) (r : ℝ) => r • e x