D Lp Norm ddconv le

lemma dLpNorm_ddconv_le {p : ℝ≥0} (hp : 1 ≤ p) (f g : G → 𝕜) :    ‖f ∗ᵈ g‖_[p] ≤ ‖f‖_[p] * ‖g‖_[1] := by  obtain rfl | hp := hp.eq_or_lt  · simp_rw [ENNReal.coe_one, dL1Norm_eq_sum_norm, sum_mul_sum, ddconv_eq_sum_sub']    calc      ∑ x, ‖∑ y, f y * g (x - y)‖ ≤ ∑ x, ∑ y, ‖f y * g (x - y)‖ :=        sum_le_sum fun x _ ↦ norm_sum_le _ _      _ = _ := ?_    rw [sum_comm]    simp_rw [norm_mul]    exact sum_congr rfl fun x _ ↦ Fintype.sum_equiv (Equiv.subRight x) _ _ fun _ ↦ rfl  have hp₀ := zero_lt_one.trans hp  rw [← rpow_le_rpow_iff _ _ hp₀, mul_rpow]  any_goals positivity  dsimp  simp_rw [dLpNorm_rpow_eq_sum_norm hp₀.ne', ddconv_eq_sum_sub']  have hpconj : (p : ℝ).HolderConjugate (1 - (p : ℝ)⁻¹)⁻¹ :=    ⟨by simp, mod_cast hp₀, by bound⟩  have (x : G) : ‖∑ y, f y * g (x - y)‖ ^ (p : ℝ) ≤      (∑ y, ‖f y‖ ^ (p : ℝ) * ‖g (x - y)‖) * (∑ y, ‖g (x - y)‖) ^ (p - 1 : ℝ) := by    rw [← le_rpow_inv_iff_of_pos, mul_rpow, ← rpow_mul, sub_one_mul, mul_inv_cancel₀]    any_goals positivity    calc      _ ≤ ∑ y, ‖f y * g (x - y)‖ := norm_sum_le _ _      _ = ∑ y, ‖f y‖ * ‖g (x - y)‖ ^ (p : ℝ)⁻¹ * ‖g (x - y)‖ ^ (1 - (p : ℝ)⁻¹) := ?_      _ ≤ _ := inner_le_Lp_mul_Lq _ _ _ hpconj      _ = _ := ?_    · congr with t      rw [norm_mul, mul_assoc, ← rpow_add' (by positivity), add_sub_cancel, rpow_one]      simp    · have : 1 - (p : ℝ)⁻¹ ≠ 0 := sub_ne_zero.2 (inv_ne_one.2 <| NNReal.coe_ne_one.2 hp.ne').symm      simp [mul_rpow, rpow_nonneg, hp₀.ne', this, abs_rpow_of_nonneg]  calc    ∑ x, ‖∑ y, f y * g (x - y)‖ ^ (p : ℝ) ≤        ∑ x, (∑ y, ‖f y‖ ^ (p : ℝ) * ‖g (x - y)‖) * (∑ y, ‖g (x - y)‖) ^ (p - 1 : ℝ) :=      sum_le_sum fun i _ ↦ this _    _ = _ := ?_  have hg : ∀ x, ∑ y, ‖g (x - y)‖ = ‖g‖_[1] := by    simp_rw [dL1Norm_eq_sum_norm]    exact fun x ↦ Fintype.sum_equiv (Equiv.subLeft _) _ _ fun _ ↦ rfl  have hg' : ∀ y, ∑ x, ‖g (x - y)‖ = ‖g‖_[1] := by    simp_rw [dL1Norm_eq_sum_norm]    exact fun x ↦ Fintype.sum_equiv (Equiv.subRight _) _ _ fun _ ↦ rfl  simp_rw [hg]  rw [← sum_mul, sum_comm]  simp_rw [← mul_sum, hg']  rw [← sum_mul, mul_assoc, ← rpow_one_add' (by positivity), add_sub_cancel]  rw [add_sub_cancel]  positivity