Norm of a convolution

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

theorem conv_eq_wInner_one {G : Type u_1} {𝕜 : Type u_2} [Fintype G] [DecidableEq G] [AddCommGroup G] [RCLike 𝕜] (f g : G → 𝕜) (a : G) : (f ∗ g) a = RCLike.wInner 1 ((starRingEnd (G → 𝕜)) f) (translate a fun (x : G) => g (-x))

theorem dconv_eq_wInner_one {G : Type u_1} {𝕜 : Type u_2} [Fintype G] [DecidableEq G] [AddCommGroup G] [RCLike 𝕜] (f g : G → 𝕜) (a : G) : (f ○ g) a = (starRingEnd 𝕜) (RCLike.wInner 1 f (translate a g))

theorem wInner_one_dconv {G : Type u_1} {𝕜 : Type u_2} [Fintype G] [DecidableEq G] [AddCommGroup G] [RCLike 𝕜] (f g h : G → 𝕜) : RCLike.wInner 1 f (g ○ h) = RCLike.wInner 1 ((starRingEnd (G → 𝕜)) g) ((starRingEnd (G → 𝕜)) f ∗ (starRingEnd (G → 𝕜)) h)

theorem wInner_one_conv {G : Type u_1} {𝕜 : Type u_2} [Fintype G] [DecidableEq G] [AddCommGroup G] [RCLike 𝕜] (f g h : G → 𝕜) : RCLike.wInner 1 f (g ∗ h) = RCLike.wInner 1 ((starRingEnd (G → 𝕜)) g) ((starRingEnd (G → 𝕜)) f ○ (starRingEnd (G → 𝕜)) h)

theorem dconv_wInner_one {G : Type u_1} {𝕜 : Type u_2} [Fintype G] [DecidableEq G] [AddCommGroup G] [RCLike 𝕜] (f g h : G → 𝕜) : RCLike.wInner 1 (f ○ g) h = RCLike.wInner 1 ((starRingEnd (G → 𝕜)) h ∗ (starRingEnd (G → 𝕜)) g) ((starRingEnd (G → 𝕜)) f)

theorem conv_wInner_one {G : Type u_1} {𝕜 : Type u_2} [Fintype G] [DecidableEq G] [AddCommGroup G] [RCLike 𝕜] (f g h : G → 𝕜) : RCLike.wInner 1 (f ∗ g) h = RCLike.wInner 1 ((starRingEnd (G → 𝕜)) h ○ (starRingEnd (G → 𝕜)) g) ((starRingEnd (G → 𝕜)) f)

theorem dconv_wInner_one_eq_wInner_one_conv {G : Type u_1} {𝕜 : Type u_2} [Fintype G] [DecidableEq G] [AddCommGroup G] [RCLike 𝕜] (f g h : G → 𝕜) : RCLike.wInner 1 (f ○ g) h = RCLike.wInner 1 f (h ∗ g)

theorem wInner_one_dconv_eq_conv_wInner_one {G : Type u_1} {𝕜 : Type u_2} [Fintype G] [DecidableEq G] [AddCommGroup G] [RCLike 𝕜] (f g h : G → 𝕜) : RCLike.wInner 1 f (h ○ g) = RCLike.wInner 1 (f ∗ g) h

@[simp]

theorem dLpNorm_trivChar {G : Type u_1} {𝕜 : Type u_2} [DecidableEq G] [AddCommGroup G] [RCLike 𝕜] {p : ENNReal} [MeasurableSpace G] [DiscreteMeasurableSpace G] [Finite G] (hp : p ≠ 0) : ‖trivChar‖_[p] = 1

theorem dLpNorm_conv_le {G : Type u_1} {𝕜 : Type u_2} [Fintype G] [DecidableEq G] [AddCommGroup G] [RCLike 𝕜] [MeasurableSpace G] [DiscreteMeasurableSpace G] {p : NNReal} (hp : 1 ≤ p) (f g : G → 𝕜) : ‖f ∗ g‖_[↑p] ≤ ‖f‖_[↑p] * ‖g‖_[1]

A special case of Young's convolution inequality.

theorem dLpNorm_dconv_le {G : Type u_1} {𝕜 : Type u_2} [Fintype G] [DecidableEq G] [AddCommGroup G] [RCLike 𝕜] [MeasurableSpace G] [DiscreteMeasurableSpace G] {p : NNReal} (hp : 1 ≤ p) (f g : G → 𝕜) : ‖f ○ g‖_[↑p] ≤ ‖f‖_[↑p] * ‖g‖_[1]

A special case of Young's convolution inequality.

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

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