Norm of a convolution

This file characterises the L1-norm of the convolution of two functions and proves the Young convolution inequality.

@[simp]

theorem lpNorm_trivChar {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [RCLike β] (p : ENNReal) : ‖trivChar‖_[p] = 1

theorem conv_eq_inner {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [RCLike β] (f : α → β) (g : α → β) (a : α) : (f ∗ g) a = l2Inner ((starRingEnd (α → β)) f) (τ a fun (x : α) => g (-x))

theorem dconv_eq_inner {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [RCLike β] (f : α → β) (g : α → β) (a : α) : (f ○ g) a = (starRingEnd β) (l2Inner f (τ a g))

theorem lpNorm_conv_le {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [RCLike β] {p : NNReal} (hp : 1 ≤ p) (f : α → β) (g : α → β) : ‖f ∗ g‖_[↑p] ≤ ‖f‖_[↑p] * ‖g‖_[1]

A special case of Young's convolution inequality.

theorem lpNorm_dconv_le {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [RCLike β] {p : NNReal} (hp : 1 ≤ p) (f : α → β) (g : α → β) : ‖f ○ g‖_[↑p] ≤ ‖f‖_[↑p] * ‖g‖_[1]

A special case of Young's convolution inequality.

theorem l1Norm_conv {α : Type u_1} [Fintype α] [DecidableEq α] [AddCommGroup α] {f : α → ℝ} {g : α → ℝ} (hf : 0 ≤ f) (hg : 0 ≤ g) : ‖f ∗ g‖_[1] = ‖f‖_[1] * ‖g‖_[1]

theorem l1Norm_dconv {α : Type u_1} [Fintype α] [DecidableEq α] [AddCommGroup α] {f : α → ℝ} {g : α → ℝ} (hf : 0 ≤ f) (hg : 0 ≤ g) : ‖f ○ g‖_[1] = ‖f‖_[1] * ‖g‖_[1]