Redefine conv using MeasureTheory.convolution

LeanAPAP.lean

@@ -4,6 +4,8 @@ import LeanAPAP.Integer
 import LeanAPAP.Mathlib.Analysis.Convolution
 import LeanAPAP.Mathlib.Data.Real.ConjExponents
 import LeanAPAP.Mathlib.MeasureTheory.Function.LpSeminorm.NNLpNorm
+import LeanAPAP.Mathlib.MeasureTheory.Integral.Bochner.Basic
+import LeanAPAP.Mathlib.Topology.Algebra.InfiniteSum.Basic
 import LeanAPAP.Physics.AlmostPeriodicity
 import LeanAPAP.Physics.DRC
 import LeanAPAP.Physics.Unbalancing

LeanAPAP/Mathlib/Analysis/Convolution.lean

@@ -79,16 +79,43 @@ theorem convolution_assoc'' (hL : ∀ x y z, L₂ (L x y) z = L₃ x (L₄ y z))
 
 end Assoc
 
+section reindex
+variable [AddCommGroup G] {f : G → E} {g : G → E'} {a : G}
+
+/-- This is the definition. -/
+lemma convolution_eq_integral_sub (a : G) (f : G → E) (g : G → E') :
+    (f ⋆[L, ν] g) a = ∫ t, L (f t) (g (a - t)) ∂ν := rfl
+
+lemma convolution_eq_integral_neg_add [MeasurableNeg G] [ν.IsNegInvariant] (f : G → E) (g : G → E')
+    (a : G) : (f ⋆[L, ν] g) a = ∫ t, L (f (-t)) (g (a + t)) ∂ν := by
+  rw [convolution_eq_integral_sub, ← integral_neg_eq_self]; simp
+
+variable [MeasurableAdd G] [ν.IsAddLeftInvariant]
+
+lemma convolution_eq_integral_add_neg (f : G → E) (g : G → E') (a : G) :
+    (f ⋆[L, ν] g) a = ∫ t, L (f (a + t)) (g (-t)) ∂ν := by
+  rw [convolution_eq_integral_sub, ← integral_add_left_eq_self _ a]; simp
+
+lemma convolution_apply_add (f : G → E) (g : G → E') (a b : G) :
+    (f ⋆[L, ν] g) (a + b) = ∫ t, L (f (a + t)) (g (b - t)) ∂ν := by
+  rw [convolution_eq_integral_sub, ← integral_add_left_eq_self _ a]; simp
+
+lemma convolution_eq_integral_sub' [MeasurableNeg G] [ν.IsNegInvariant] (f : G → E) (g : G → E')
+    (a : G) : (f ⋆[L, ν] g) a = ∫ t, L (f (a - t)) (g t) ∂ν := by
+  rw [convolution_eq_integral_sub, ← integral_sub_left_eq_self _ _ a]; simp
+
+end reindex
+
 section translate
-variable [AddCommGroup G]
+variable [AddCommGroup G] {f : G → E} {g : G → E'} {a : G}
 
-@[simp] lemma convolution_translate (a : G) (f : G → E) (g : G → E') :
+@[simp] lemma convolution_translate (f : G → E) (g : G → E') (a : G) :
     f ⋆[L, ν] τ a g = τ a (f ⋆[L, ν] g) := by
   ext b; simp [convolution, sub_right_comm]
 
-variable [MeasurableAdd G] [ν.IsAddRightInvariant]
+variable [MeasurableAdd G] [ν.IsAddLeftInvariant]
 
-@[simp] lemma translate_convolution (a : G) (f : G → E) (g : G → E') :
+@[simp] lemma translate_convolution (f : G → E) (g : G → E') (a : G) :
     τ a f ⋆[L, ν] g = τ a (f ⋆[L, ν] g) := by
   ext b; simpa using integral_sub_right_eq_self (fun t ↦ L (f t) (g (b - a - t))) a
 

LeanAPAP/Mathlib/MeasureTheory/Integral/Bochner/Basic.lean

@@ -0,0 +1,20 @@
+import Mathlib.MeasureTheory.Integral.Bochner.Basic
+
+/-!
+# TODO
+
+Rename
+* `integral_countable'` → `integral_countable`
+* `integral_countable` → `setIntegral_countable`
+-/
+namespace MeasureTheory
+variable {α E : Type*} [NormedAddCommGroup E] [CompleteSpace E] [NormedSpace ℝ E]
+  {m : MeasurableSpace α} {μ : Measure α} [MeasurableSingletonClass α] [Countable α] {f : α → E}
+
+open Measure
+
+@[simp]
+lemma integral_count' (hf : Integrable f .count) : ∫ a, f a ∂count = ∑' a, f a := by
+  simp [integral_countable' hf]
+
+end MeasureTheory

LeanAPAP/Mathlib/Topology/Algebra/InfiniteSum/Basic.lean

@@ -0,0 +1,7 @@
+import Mathlib.Topology.Algebra.InfiniteSum.Basic
+
+variable {ι κ M : Type*} [CommMonoid M] [TopologicalSpace M]
+
+@[to_additive]
+lemma tprod_equiv (e : ι ≃ κ) (f : ι → M) (g : κ → M) (h : ∀ x, f x = g (e x)) :
+    ∏' x, f x = ∏' x, g x := by simpa [h] using e.tprod_eq g

LeanAPAP/Physics/Unbalancing.lean

@@ -81,7 +81,7 @@ private lemma unbalancing'' (p : ℕ) (hp : 5 ≤ p) (hp₁ : Odd p) (hε₀ : 0
               (div_le_div_of_nonneg_left (by norm_num) hε₀ hε₁).trans' <| by norm_num))
           (by norm_num) ?_
     all_goals positivity
-  have : ε ^ p ≤ 2 * ∑ i, ↑(ν i) * ((f ^ (p - 1)) i * (f⁺) i) := by
+  have : ε ^ p ≤ 2 * ∑ i, ↑(ν i) * ((f ^ (p - 1)) i * f⁺ i) := by
     calc
       ε ^ p ≤ ‖f‖_[p, ν] ^ p := hp₁.strictMono_pow.monotone hε
       _ = ∑ i, ν i • ((f ^ (p - 1)) i * |f| i) := by

LeanAPAP/Prereqs/Convolution/Compact.lean

@@ -36,12 +36,7 @@ local notation a " /ℚ " q => (q : ℚ≥0)⁻¹ • a
 
 variable {G H R S : Type*} [Fintype G] [DecidableEq G] [AddCommGroup G]
 
-/-!
-### Convolution of functions
-
-In this section, we define the convolution `f ∗ₙ g` and difference convolution `f ○ₙ g` of functions
-`f g : G → R`, and show how they interact.
--/
+namespace Analysis.Compact
 
 /-! ### Trivial character -/
 

LeanAPAP/Prereqs/Convolution/Discrete/Basic.lean

@@ -54,7 +54,7 @@ variable [CommSemiring R] {f g : G → R}
 
 lemma indicate_conv_indicate_eq_sum (s t : Finset G) (a : G) :
     (𝟭_[R] s ∗ 𝟭 t) a = #{x ∈ s ×ˢ t | x.1 + x.2 = a} := by
-  simp only [conv_apply, indicate_apply, ← ite_and, filter_comm, boole_mul, sum_boole]
+  simp only [conv_eq_sum, indicate_apply, ← ite_and, filter_comm, boole_mul, sum_boole]
   simp_rw [← mem_product, filter_univ_mem]
 
 lemma indicate_conv (s : Finset G) (f : G → R) : 𝟭 s ∗ f = ∑ a ∈ s, τ a f := by