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 = RCLike.wInner 1 ((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 𝕜) (RCLike.wInner 1 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 → 𝕜) : RCLike.wInner 1 f (g ○ᵈ h) = RCLike.wInner 1 ((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 → 𝕜) : RCLike.wInner 1 f (g ∗ᵈ h) = RCLike.wInner 1 ((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 → 𝕜) : RCLike.wInner 1 (f ○ᵈ g) h = RCLike.wInner 1 ((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 → 𝕜) : RCLike.wInner 1 (f ∗ᵈ g) h = RCLike.wInner 1 ((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 → 𝕜) : RCLike.wInner 1 (f ○ᵈ g) h = RCLike.wInner 1 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 → 𝕜) : 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_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]