chore: drop the aestronglyMeasurable field in BoundedFiniteSupport (#272)

as it's already contained in the `MemLp` assumption.

Also, I ran the linter on the project, and fixed a few of the things it mentioned.

Author: sgouezel

Carleson/Antichain/AntichainTileCount.lean

@@ -96,7 +96,6 @@ lemma tile_reach {ϑ : Θ X} {N : ℕ} {p p' : 𝔓 X} (hp : dist_(p) (𝒬 p) 
             ← zpow_zero (2 : ℝ)]
           rw [Nat.cast_mul, Nat.cast_ofNat, Nat.cast_pow]
           gcongr --uses h12
-          have : (2 : ℝ)^a = 2^(a : ℤ) := by rw [@zpow_natCast]
           ring_nf
           nlinarith only
       _ = (4 * 2 ^ (2 - 5 * (a : ℤ)  ^ 2 - 2 * ↑a)) * (D * D ^ 𝔰 p) := by ring

Carleson/Calculations.lean

@@ -199,18 +199,17 @@ lemma calculation_12 (s : ℝ) :
   have rightSide := calc 2 ^ (200 * a ^ 2 + 4) * (8 * ((2 : ℝ) ^ (100 * a ^ 2)) ^ s)
     _ = 2 ^ (200*a^2 + 4) * ((2^3)*((2 ^ (100 * a ^ 2)) ^ s)) := by
       norm_num
-    _ = 2 ^ (200*a^2 + 4) * (  2^3   *   2 ^ (100 * a ^ 2 * s)  ) := by
+    _ = 2 ^ (200*a^2 + 4) * (  2^3 * 2 ^ (100 * a ^ 2 * s)  ) := by
       rw [Real.rpow_mul (x:=2) (by positivity)]
       norm_cast
-    _ = 2 ^ (200*a^2 + 4) * 2 ^ (3    +   100 * a ^ 2 * s) := by
+    _ = 2 ^ (200*a^2 + 4) * 2 ^ (3 + 100 * a ^ 2 * s) := by
       have fact := Real.rpow_add (x:=2) (y:= 3) (z:= 100 * a ^ 2 * s) (by positivity)
       rw_mod_cast [fact]
-    _ = 2^(     200*a^2 + 4           +      (3    +   100 * a ^ 2 * s)  ) := by
-      have fact := Real.rpow_add (x:=2) (y:= 200*a^2 + 4) (z:= 3    +   100 * a ^ 2 * s) (by positivity)
+    _ = 2 ^ (200*a^2 + 4  + (3 + 100 * a ^ 2 * s)) := by
       nth_rw 2 [Real.rpow_add]
       norm_cast
       positivity
-    _ = 2^(7 + ((100 * a^2 * s) + (100 * a^2 * 2))) := by
+    _ = 2 ^ (7 + ((100 * a^2 * s) + (100 * a^2 * 2))) := by
       congrm 2 ^ ?_
       linarith
   rw_mod_cast [leftSide]
@@ -222,7 +221,7 @@ lemma calculation_13 : (2 : ℝ) ^ (200 * (a^3) + 4*a) = (defaultA a) ^ (200*a^2
   rw_mod_cast [← fact]
   ring
 
-lemma calculation_14 [PseudoMetricSpace X] [ProofData a q K σ₁ σ₂ F G] (n: ℕ) : 
+lemma calculation_14 [PseudoMetricSpace X] [ProofData a q K σ₁ σ₂ F G] (n: ℕ) :
     (2 : ℝ) ^ ((Z : ℝ) * n / 2 - 201 * a ^ 3) ≤ 2 ^ ((Z : ℝ) * n / 2 - (200 * a ^ 3 + 4 * a)) := by
   gcongr
   · linarith
@@ -240,7 +239,7 @@ lemma calculation_15 [PseudoMetricSpace X] [ProofData a q K σ₁ σ₂ F G]
     2 ^ (zon - (200 * a^3 + 4*a)) ≤ dist := by
   rw [Real.rpow_sub (hx := by linarith)]
   rw [show dist = 2 ^ (200 * a ^ 3 + 4 * a) * dist / 2 ^ (200 * a ^ 3 + 4 * a) by simp]
-  have := (div_le_div_iff_of_pos_right (c := 2 ^ (200 * a ^ 3 + 4 * a)) (hc := by have aIsBig := four_le_a X; positivity)).mpr h
+  have := (div_le_div_iff_of_pos_right (c := 2 ^ (200 * a ^ 3 + 4 * a)) (hc := by positivity)).mpr h
   exact_mod_cast this
 
 lemma calculation_16 [PseudoMetricSpace X] [ProofData a q K σ₁ σ₂ F G] (s: ℤ) :
@@ -266,4 +265,3 @@ lemma calculation_7_7_4 [PseudoMetricSpace X] [ProofData a q K σ₁ σ₂ F G]
     · norm_num
     omega
   exact Nat.mul_le_mul this (Nat.le_add_left 1 n)
-

Carleson/Classical/Helper.lean

@@ -10,12 +10,13 @@ theorem Real.volume_uIoc {a b : ℝ} : volume (Set.uIoc a b) = ENNReal.ofReal |b
   /- Cf. proof of Real.volume_interval-/
   rw [Set.uIoc, volume_Ioc, max_sub_min_eq_abs]
 
-lemma intervalIntegral.integral_conj' {μ : Measure ℝ} {𝕜 : Type} [RCLike 𝕜] {f : ℝ → 𝕜} {a b : ℝ}:
+lemma intervalIntegral.integral_conj' {μ : Measure ℝ} {𝕜 : Type*} [RCLike 𝕜] {f : ℝ → 𝕜} {a b : ℝ} :
     ∫ x in a..b, (starRingEnd 𝕜) (f x) ∂μ = (starRingEnd 𝕜) (∫ x in a..b, f x ∂μ) := by
   rw [intervalIntegral_eq_integral_uIoc, integral_conj, intervalIntegral_eq_integral_uIoc,
       RCLike.real_smul_eq_coe_mul, RCLike.real_smul_eq_coe_mul, map_mul, RCLike.conj_ofReal]
 
-lemma intervalIntegrable_of_bdd {a b : ℝ} {δ : ℝ} {g : ℝ → ℂ} (measurable_g : Measurable g) (bddg : ∀ x, ‖g x‖ ≤ δ) : IntervalIntegrable g volume a b := by
+lemma intervalIntegrable_of_bdd {a b : ℝ} {δ : ℝ} {g : ℝ → ℂ} (measurable_g : Measurable g)
+    (bddg : ∀ x, ‖g x‖ ≤ δ) : IntervalIntegrable g volume a b := by
   apply @IntervalIntegrable.mono_fun' _ _ _ _ _ _ (fun _ ↦ δ)
   · exact intervalIntegrable_const
   · exact measurable_g.aestronglyMeasurable
@@ -24,24 +25,26 @@ lemma intervalIntegrable_of_bdd {a b : ℝ} {δ : ℝ} {g : ℝ → ℂ} (measur
     rw [Subtype.forall]
     exact fun x _ ↦ bddg x
 
-lemma IntervalIntegrable.bdd_mul {F : Type} [NormedDivisionRing F] {f g : ℝ → F} {a b : ℝ} {μ : Measure ℝ}
-    (hg : IntervalIntegrable g μ a b) (hm : AEStronglyMeasurable f μ) (hfbdd : ∃ C, ∀ x, ‖f x‖ ≤ C) : IntervalIntegrable (fun x ↦ f x * g x) μ a b := by
+lemma IntervalIntegrable.bdd_mul {F : Type*} [NormedDivisionRing F] {f g : ℝ → F} {a b : ℝ}
+    {μ : Measure ℝ} (hg : IntervalIntegrable g μ a b) (hm : AEStronglyMeasurable f μ)
+    (hfbdd : ∃ C, ∀ x, ‖f x‖ ≤ C) : IntervalIntegrable (fun x ↦ f x * g x) μ a b := by
   rw [intervalIntegrable_iff, IntegrableOn]
   apply Integrable.bdd_mul _ hm.restrict hfbdd
   rwa [← IntegrableOn, ← intervalIntegrable_iff]
 
-lemma IntervalIntegrable.mul_bdd {F : Type} [NormedField F] {f g : ℝ → F} {a b : ℝ} {μ : Measure ℝ}
-    (hf : IntervalIntegrable f μ a b) (hm : AEStronglyMeasurable g μ) (hgbdd : ∃ C, ∀ x, ‖g x‖ ≤ C) : IntervalIntegrable (fun x ↦ f x * g x) μ a b := by
+lemma IntervalIntegrable.mul_bdd {F : Type*} [NormedField F] {f g : ℝ → F} {a b : ℝ}
+    {μ : Measure ℝ} (hf : IntervalIntegrable f μ a b) (hm : AEStronglyMeasurable g μ)
+    (hgbdd : ∃ C, ∀ x, ‖g x‖ ≤ C) : IntervalIntegrable (fun x ↦ f x * g x) μ a b := by
   conv => pattern (fun x ↦ f x * g x); ext x; rw [mul_comm]
   exact hf.bdd_mul hm hgbdd
 
-lemma IntegrableOn.sub {α : Type} {β : Type} {m : MeasurableSpace α}
-    {μ : Measure α} [NormedAddCommGroup β] {s : Set α} {f g : α → β} (hf : IntegrableOn f s μ) (hg : IntegrableOn g s μ) : IntegrableOn (f - g) s μ := by
+lemma IntegrableOn.sub {α : Type*} {β : Type*} {m : MeasurableSpace α} {μ : Measure α}
+    [NormedAddCommGroup β] {s : Set α} {f g : α → β}
+    (hf : IntegrableOn f s μ) (hg : IntegrableOn g s μ) : IntegrableOn (f - g) s μ := by
   apply Integrable.sub <;> rwa [← IntegrableOn]
 
-
-lemma ConditionallyCompleteLattice.le_biSup {α : Type} [ConditionallyCompleteLinearOrder α] {ι : Type} [Nonempty ι]
-    {f : ι → α} {s : Set ι} {a : α} (hfs : BddAbove (f '' s)) (ha : ∃ i ∈ s, f i = a) :
+lemma ConditionallyCompleteLattice.le_biSup {α : Type*} [ConditionallyCompleteLinearOrder α]
+    {ι : Type*} {f : ι → α} {s : Set ι} {a : α} (hfs : BddAbove (f '' s)) (ha : ∃ i ∈ s, f i = a) :
     a ≤ ⨆ i ∈ s, f i := by
   apply ConditionallyCompleteLattice.le_csSup
   · --TODO: improve this
@@ -75,15 +78,16 @@ lemma ConditionallyCompleteLattice.le_biSup {α : Type} [ConditionallyCompleteLi
   simp only [Set.mem_range, exists_prop] at hx
   rwa [hx.2] at fia
 
-
-/-Adapted from mathlib Function.Periodic.exists_mem_Ico₀-/
-theorem Function.Periodic.exists_mem_Ico₀' {α : Type} {β : Type} {f : α → β} {c : α}
-  [LinearOrderedAddCommGroup α] [Archimedean α] (h : Periodic f c) (hc : 0 < c) (x : α) : ∃ (n : ℤ), (x - n • c) ∈ Set.Ico 0 c ∧ f x = f (x - n • c) :=
+/- Adapted from mathlib Function.Periodic.exists_mem_Ico₀ -/
+theorem Function.Periodic.exists_mem_Ico₀' {α β : Type*} {f : α → β} {c : α}
+    [LinearOrderedAddCommGroup α] [Archimedean α] (h : Periodic f c) (hc : 0 < c) (x : α) :
+    ∃ (n : ℤ), (x - n • c) ∈ Set.Ico 0 c ∧ f x = f (x - n • c) :=
   let ⟨n, H, _⟩ := existsUnique_zsmul_near_of_pos' hc x
   ⟨n, H, (h.sub_zsmul_eq n).symm⟩
 
-/-Adapted from mathlib Function.Periodic.exists_mem_Ico₀-/
-theorem Function.Periodic.exists_mem_Ico' {α : Type} {β : Type} {f : α → β} {c : α}
-  [LinearOrderedAddCommGroup α] [Archimedean α] (h : Periodic f c) (hc : 0 < c) (x a: α) : ∃ (n : ℤ), (x - n • c) ∈ Set.Ico a (a + c) ∧ f x = f (x - n • c) :=
+/- Adapted from mathlib Function.Periodic.exists_mem_Ico₀ -/
+theorem Function.Periodic.exists_mem_Ico' {α β : Type*} {f : α → β} {c : α}
+    [LinearOrderedAddCommGroup α] [Archimedean α] (h : Periodic f c) (hc : 0 < c) (x a: α) :
+    ∃ (n : ℤ), (x - n • c) ∈ Set.Ico a (a + c) ∧ f x = f (x - n • c) :=
   let ⟨n, H, _⟩ := existsUnique_sub_zsmul_mem_Ico hc x a
   ⟨n, H, (h.sub_zsmul_eq n).symm⟩

Carleson/Defs.lean

@@ -320,7 +320,7 @@ lemma enorm_K_sub_le [ProperSpace X] [IsFiniteMeasureOnCompacts (volume : Measur
 
 lemma integrableOn_K_Icc [IsOpenPosMeasure (volume : Measure X)]
     [IsFiniteMeasureOnCompacts (volume : Measure X)] [ProperSpace X]
-    [Regular (volume : Measure X)] [IsOneSidedKernel a K] {x : X} {r R : ℝ} (hr : r > 0) :
+    [IsOneSidedKernel a K] {x : X} {r R : ℝ} (hr : r > 0) :
     IntegrableOn (K x) {y | dist x y ∈ Icc r R} volume := by
   use Measurable.aestronglyMeasurable (measurable_K_right x)
   rw [hasFiniteIntegral_def]

Carleson/ForestOperator/Forests.lean

@@ -373,8 +373,7 @@ theorem forest_operator' {n : ℕ} (𝔉 : Forest X n) {f : X → ℂ} {A : Set
     fun_prop
   · apply h'A.subset support_indicator_subset
   gcongr
-  · have := (q_mem_Ioc (X := X)).2
-    simp only [sub_nonneg, ge_iff_le, inv_le_inv₀ zero_lt_two (q_pos X)]
+  · simp only [sub_nonneg, ge_iff_le, inv_le_inv₀ zero_lt_two (q_pos X)]
     exact (q_mem_Ioc (X := X)).2
   · exact le_rfl
   calc

Carleson/ForestOperator/PointwiseEstimate.lean

@@ -714,9 +714,7 @@ lemma second_tree_pointwise (hu : u ∈ t) (hL : L ∈ 𝓛 (t u)) (hx : x ∈ L
   have x'p : x' ∈ 𝓘 p := (Grid.le_def.mp Lle).1 hx'
   refine le_iSup₂_of_le (𝓘 p) x'p <| le_iSup₂_of_le x xp <|
     le_iSup₂_of_le (𝔰 p') ⟨s_ineq, scale_mem_Icc.2⟩ <| le_iSup_of_le ?_ ?_
-  · have : ((D : ℝ≥0∞) ^ (𝔰 p' - 1)).toReal = D ^ (s₂ - 1) := by
-      rw [sp', ← ENNReal.toReal_zpow]; simp
-    apply le_upperRadius; convert d1
+  · apply le_upperRadius; convert d1
   · convert le_rfl; change (Icc (𝔰 p) _).toFinset = _; rw [sp, sp']
     apply subset_antisymm
     · rw [← Finset.toFinset_coe (t.σ u x), toFinset_subset_toFinset]

Carleson/ForestOperator/RemainingTiles.lean

@@ -229,7 +229,7 @@ lemma square_function_count (hJ : J ∈ 𝓙₆ t u₁) (s' : ℤ) :
     ⨍⁻ x in J, (∑ I ∈ {I : Grid X | s I = s J - s' ∧ Disjoint (I : Set X) (𝓘 u₁) ∧
     ¬ Disjoint (J : Set X) (ball (c I) (8 * D ^ s I)) },
     (ball (c I) (8 * D ^ s I)).indicator 1 x) ^ 2 ∂volume ≤ C7_6_4 a s' := by
-  cases' lt_or_ge (↑S + s J) s' with hs' hs'
+  rcases lt_or_ge (↑S + s J) s' with hs' | hs'
   · suffices ({I : Grid X | s I = s J - s' ∧ Disjoint (I : Set X) (𝓘 u₁) ∧
         ¬ Disjoint (J : Set X) (ball (c I) (8 * D ^ s I)) } : Finset (Grid X)) = ∅ by
       rw [this]

Carleson/Psi.lean

@@ -26,10 +26,12 @@ private lemma D_pow0' (r : ℤ) : 0 < (D : ℝ) ^ r := by positivity
 private lemma cDx0 {c x : ℝ} (hc : c > 0) (hx : 0 < x) : c * D * x > 0 := by positivity
 end
 
+/-- The function `ψ` used as a basis for a dyadic partition of unity. -/
 def ψ (D : ℕ) (x : ℝ) : ℝ :=
   max 0 <| min 1 <| min (4 * D * x - 1) (2 - 4 * x)
 
-set_option hygiene false
+set_option hygiene false in
+@[inherit_doc]
 scoped[ShortVariables] notation "ψ" => ψ (defaultD a)
 
 lemma zero_le_ψ (D : ℕ) (x : ℝ) : 0 ≤ ψ D x :=
@@ -140,8 +142,9 @@ lemma lipschitzWith_ψ' (hD : 1 ≤ D) (a b : ℝ) : ‖ψ D a - ψ D b‖ ≤ 4
   repeat rw [ENNReal.toReal_ofReal (by positivity)] at lipschitz
   norm_cast
 
-/- the one or two numbers `s` where `ψ (D ^ (-s) * x)` is possibly nonzero -/
-variable (D) in def nonzeroS (x : ℝ) : Finset ℤ :=
+variable (D) in
+/-- the one or two numbers `s` where `ψ (D ^ (-s) * x)` is possibly nonzero -/
+def nonzeroS (x : ℝ) : Finset ℤ :=
   Finset.Icc ⌊(1 + logb D (2 * x))⌋ ⌈logb D (4 * x)⌉
 
 ---------------------------------------------
@@ -519,7 +522,6 @@ lemma nnnorm_Ks_le {s : ℤ} {x y : X} :
 /-- Needed for Lemma 7.5.5. -/
 lemma enorm_Ks_le {s : ℤ} {x y : X} :
     ‖Ks s x y‖ₑ ≤ C2_1_3 a / volume (ball x (D ^ s)) * ‖ψ (D ^ (-s) * dist x y)‖ₑ := by
-  have : 0 ≤ C2_1_3 a / volume (ball x (D ^ s)) := by unfold C2_1_3; positivity
   by_cases hK : Ks s x y = 0
   · rw [hK, enorm_zero]; exact zero_le _
   rw [Ks, enorm_mul]; nth_rw 2 [← enorm_norm]; rw [norm_real, enorm_norm]
@@ -649,7 +651,8 @@ private lemma norm_Ks_sub_Ks_le₀₀ {s : ℤ} {x y y' : X} (hK : Ks s x y ≠
   have : (dist y y' / dist x y) ^ (a : ℝ)⁻¹ ≤ (dist y y' / D ^ s * (4 * D)) ^ (a : ℝ)⁻¹ := by
     apply Real.rpow_le_rpow (div_nonneg dist_nonneg dist_nonneg) this (by positivity)
   rw [Real.mul_rpow (div_nonneg dist_nonneg (Ds0 X s).le) (fourD0 D1).le] at this
-  apply le_trans <| mul_le_mul this (div_vol_le₀ C_K_pos_real hK) (by simp; positivity) (by positivity)
+  apply le_trans <| mul_le_mul this (div_vol_le₀ C_K_pos_real hK)
+    (by simp only [C_K, coe_rpow, NNReal.coe_ofNat, defaultA]; positivity) (by positivity)
   rw [(by ring : (dist y y' / D ^ s) ^ (a : ℝ)⁻¹ * (4 * D) ^ (a : ℝ)⁻¹ *
       (2 ^ (2 * a + 100 * a ^ 3) * C_K a / volume.real (ball x (D ^ s))) =
       (4 * D) ^ (a : ℝ)⁻¹ * 2 ^ (2 * a + 100 * a ^ 3) * C_K a / volume.real (ball x (D ^ s)) *

Carleson/TileExistence.lean

@@ -186,7 +186,7 @@ lemma chain_property_set_has_bound (k : ℤ):
   · exact fun s a ↦ subset_iUnion₂_of_subset s a fun ⦃a⦄ a ↦ a
 
 variable (X) in
-def zorn_apply_maximal_set (k : ℤ):
+lemma zorn_apply_maximal_set (k : ℤ):
     ∃ s ∈ property_set X k, ∀ s' ∈ property_set X k, s ⊆ s' → s' = s := by
   have := zorn_subset (property_set X k) (chain_property_set_has_bound X k)
   simp_rw [maximal_iff] at this; convert this using 6; exact eq_comm
@@ -300,20 +300,20 @@ lemma I_induction_proof {k:ℤ} (hk:-S ≤ k) (hneq : ¬ k = -S) : -S ≤ k - 1
   linarith [lt_of_le_of_ne hk fun a_1 ↦ hneq (id a_1.symm)]
 
 mutual
-  def I1 {k:ℤ} (hk : -S ≤ k) (y : Yk X k) : Set X :=
+  def I1 {k : ℤ} (hk : -S ≤ k) (y : Yk X k) : Set X :=
     if hk': k = -S then
       ball y (D^(-S:ℤ))
     else
       let hk'' : -S < k := lt_of_le_of_ne hk fun a_1 ↦ hk' (id a_1.symm)
-      have h1: 0 ≤ S + (k - 1) := by linarith
+      have h1 : 0 ≤ S + (k - 1) := by linarith
       have : (S + (k-1)).toNat < (S + k).toNat := by
         rw [Int.lt_toNat,Int.toNat_of_nonneg h1]
         linarith
       ⋃ (y': Yk X (k-1)),
         ⋃ (_ : y' ∈ Yk X (k-1) ↓∩ ball (y:X) (D^k)), I3 (I_induction_proof hk hk') y'
   termination_by (3 * (S+k).toNat, sizeOf y)
 
-  def I2 {k:ℤ} (hk : -S ≤ k) (y : Yk X k) : Set X :=
+  def I2 {k : ℤ} (hk : -S ≤ k) (y : Yk X k) : Set X :=
     if hk': k = -S then
       ball y (2 * D^(-S:ℤ))
     else
@@ -344,25 +344,22 @@ lemma I1_subset_I3 {k : ℤ} (hk : -S ≤ k) (y:Yk X k) :
   left
   exact hi
 
-lemma I1_subset_I2 {k:ℤ} (hk : -S ≤ k) (y:Yk X k) :
+@[nolint unusedHavesSuffices]
+lemma I1_subset_I2 {k : ℤ} (hk : -S ≤ k) (y : Yk X k) :
     I1 hk y ⊆ I2 hk y := by
-  rw [I1,I2]
-  if hk_s : k = -S then
-    intro y'
-    rw [dif_pos hk_s,dif_pos hk_s]
+  rw [I1, I2]
+  split_ifs with hk_s
+  · intro y'
     apply ball_subset_ball
     nth_rw 1 [← one_mul (D^(-S:ℤ):ℝ)]
     gcongr
     norm_num
-  else
-    rw [dif_neg hk_s, dif_neg hk_s]
-    simp only [iUnion_subset_iff]
+  · simp only [iUnion_subset_iff]
     intro y' hy' z hz
     simp only [mem_iUnion, exists_prop, exists_and_left]
     use y'
     rw [and_iff_left hz]
-    revert hy'
-    apply ball_subset_ball
+    apply ball_subset_ball _ hy'
     nth_rw 1 [← one_mul (D^k : ℝ)]
     gcongr
     norm_num

Carleson/ToMathlib/Analysis/Convolution.lean

@@ -40,7 +40,7 @@ protected theorem AEStronglyMeasurable.convolution [NormedSpace ℝ F] [AddGroup
 
 /-- This implies both of the following theorems `convolutionExists_of_memLp_memLp` and
 `enorm_convolution_le_eLpNorm_mul_eLpNorm`. -/
-lemma lintegral_enorm_convolution_integrand_le_eLpNorm_mul_eLpNorm [NormedSpace ℝ F] [AddGroup G]
+lemma lintegral_enorm_convolution_integrand_le_eLpNorm_mul_eLpNorm [AddGroup G]
     [MeasurableAdd₂ G] [MeasurableNeg G] {μ : Measure G} [SFinite μ] [μ.IsNegInvariant]
     [μ.IsAddLeftInvariant] {p q : ENNReal} (hpq : p.IsConjExponent q)
     (hL : ∀ (x y : G), ‖L (f x) (g y)‖ ≤ ‖f x‖ * ‖g y‖)
@@ -57,7 +57,7 @@ lemma lintegral_enorm_convolution_integrand_le_eLpNorm_mul_eLpNorm [NormedSpace
 
 /-- If `MemLp f p μ` and `MemLp g q μ`, where `p` and `q` are Hölder conjugates, then the
 convolution of `f` and `g` exists everywhere. -/
-theorem ConvolutionExists.of_memLp_memLp [NormedSpace ℝ F] [AddGroup G] [MeasurableAdd₂ G]
+theorem ConvolutionExists.of_memLp_memLp [AddGroup G] [MeasurableAdd₂ G]
     [MeasurableNeg G] (μ : Measure G) [SFinite μ] [μ.IsNegInvariant] [μ.IsAddLeftInvariant]
     [μ.IsAddRightInvariant] {p q : ENNReal} (hpq : p.IsConjExponent q)
     (hL : ∀ (x y : G), ‖L (f x) (g y)‖ ≤ ‖f x‖ * ‖g y‖) (hf : AEStronglyMeasurable f μ)
@@ -71,7 +71,7 @@ theorem ConvolutionExists.of_memLp_memLp [NormedSpace ℝ F] [AddGroup G] [Measu
 by `eLpNorm f p μ * eLpNorm g q μ`. -/
 theorem enorm_convolution_le_eLpNorm_mul_eLpNorm [NormedSpace ℝ F] [AddGroup G]
     [MeasurableAdd₂ G] [MeasurableNeg G] (μ : Measure G) [SFinite μ] [μ.IsNegInvariant]
-    [μ.IsAddLeftInvariant] [μ.IsAddRightInvariant] {p q : ENNReal} (hpq : p.IsConjExponent q)
+    [μ.IsAddLeftInvariant] {p q : ENNReal} (hpq : p.IsConjExponent q)
     (hL : ∀ (x y : G), ‖L (f x) (g y)‖ ≤ ‖f x‖ * ‖g y‖)
     (hf : AEStronglyMeasurable f μ) (hg : AEStronglyMeasurable g μ) (x₀ : G) :
     ‖(f ⋆[L, μ] g) x₀‖ₑ ≤ eLpNorm f p μ * eLpNorm g q μ :=