Norm of a convolution

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

theorem ddconv_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 (G → 𝕜)) f, translate a fun (x : G) => g (-x)⟫_[𝕜]

theorem dddconv_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 𝕜) ⟪f, translate a g⟫_[𝕜]

theorem wInner_one_dddconv {G : Type u_1} {𝕜 : Type u_2} [Fintype G] [DecidableEq G] [AddCommGroup G] [RCLike 𝕜] (f g h : G → 𝕜) : ⟪f, g ○ᵈ h⟫_[𝕜] = ⟪(starRingEnd (G → 𝕜)) g, (starRingEnd (G → 𝕜)) f ∗ᵈ (starRingEnd (G → 𝕜)) h⟫_[𝕜]

theorem wInner_one_ddconv {G : Type u_1} {𝕜 : Type u_2} [Fintype G] [DecidableEq G] [AddCommGroup G] [RCLike 𝕜] (f g h : G → 𝕜) : ⟪f, g ∗ᵈ h⟫_[𝕜] = ⟪(starRingEnd (G → 𝕜)) g, (starRingEnd (G → 𝕜)) f ○ᵈ (starRingEnd (G → 𝕜)) h⟫_[𝕜]

theorem dddconv_wInner_one {G : Type u_1} {𝕜 : Type u_2} [Fintype G] [DecidableEq G] [AddCommGroup G] [RCLike 𝕜] (f g h : G → 𝕜) : ⟪f ○ᵈ g, h⟫_[𝕜] = ⟪(starRingEnd (G → 𝕜)) h ∗ᵈ (starRingEnd (G → 𝕜)) g, (starRingEnd (G → 𝕜)) f⟫_[𝕜]

theorem ddconv_wInner_one {G : Type u_1} {𝕜 : Type u_2} [Fintype G] [DecidableEq G] [AddCommGroup G] [RCLike 𝕜] (f g h : G → 𝕜) : ⟪f ∗ᵈ g, h⟫_[𝕜] = ⟪(starRingEnd (G → 𝕜)) h ○ᵈ (starRingEnd (G → 𝕜)) g, (starRingEnd (G → 𝕜)) f⟫_[𝕜]

theorem dddconv_wInner_one_eq_wInner_one_ddconv {G : Type u_1} {𝕜 : Type u_2} [Fintype G] [DecidableEq G] [AddCommGroup G] [RCLike 𝕜] (f g h : G → 𝕜) : ⟪f ○ᵈ g, h⟫_[𝕜] = ⟪f, h ∗ᵈ g⟫_[𝕜]

theorem wInner_one_dddconv_eq_ddconv_wInner_one {G : Type u_1} {𝕜 : Type u_2} [Fintype G] [DecidableEq G] [AddCommGroup G] [RCLike 𝕜] (f g h : G → 𝕜) : ⟪f, h ○ᵈ g⟫_[𝕜] = ⟪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_ddconv_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_dddconv_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_ddconv {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_dddconv {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]