Prerequisites to redefining conv in terms of `MeasureTheory.convolu…

…tion`

LeanAPAP.lean

@@ -1,6 +1,12 @@
 import LeanAPAP.Extras.BSG
 import LeanAPAP.FiniteField
 import LeanAPAP.Integer
+import LeanAPAP.Mathlib.Analysis.Convolution
+import LeanAPAP.Mathlib.Analysis.NormedSpace.OperatorNorm.Mul
+import LeanAPAP.Mathlib.Data.Set.Card
+import LeanAPAP.Mathlib.MeasureTheory.Group.Measure
+import LeanAPAP.Mathlib.MeasureTheory.Measure.Count
+import LeanAPAP.Mathlib.Topology.Algebra.InfiniteSum.ENNReal
 import LeanAPAP.Physics.AlmostPeriodicity
 import LeanAPAP.Physics.DRC
 import LeanAPAP.Physics.Unbalancing

LeanAPAP/Mathlib/Analysis/Convolution.lean

@@ -0,0 +1,24 @@
+import Mathlib.Analysis.Convolution
+
+/-!
+# TODO
+
+Extra arguments to `convolution_zero`
+-/
+
+-- TODO: Replace
+alias MeasureTheory.ConvolutionExistsAt.of_norm' := MeasureTheory.ConvolutionExistsAt.ofNorm'
+alias MeasureTheory.ConvolutionExistsAt.of_norm := MeasureTheory.ConvolutionExistsAt.ofNorm
+alias HasCompactSupport.convolutionExists_left := HasCompactSupport.convolutionExistsLeft
+alias HasCompactSupport.convolutionExists_right_of_continuous_left :=
+  HasCompactSupport.convolutionExistsRightOfContinuousLeft
+
+namespace MeasureTheory
+variable {𝕜 G E E' F : Type*} [NormedAddCommGroup E] [NormedAddCommGroup E'] [NormedAddCommGroup F]
+  {f : G → E} {g g' : G → E'} [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 E']
+  [NormedSpace 𝕜 F] {L : E →L[𝕜] E' →L[𝕜] F} [MeasurableSpace G] {μ : Measure G} [AddGroup G]
+
+lemma ConvolutionExists.of_finite [Finite G] [MeasurableSingletonClass G] [IsFiniteMeasure μ] :
+    ConvolutionExists f g L μ := fun _ ↦ .of_finite
+
+end MeasureTheory

LeanAPAP/Mathlib/Analysis/NormedSpace/OperatorNorm/Mul.lean

@@ -0,0 +1,9 @@
+import Mathlib.Analysis.NormedSpace.OperatorNorm.Mul
+
+namespace ContinuousLinearMap
+variable {𝕜 R : Type*} [NontriviallyNormedField 𝕜] [NonUnitalSeminormedCommRing R] [NormedSpace 𝕜 R]
+  [IsScalarTower 𝕜 R R] [SMulCommClass 𝕜 R R]
+
+@[simp] lemma flip_mul : (ContinuousLinearMap.mul 𝕜 R).flip = .mul 𝕜 R := by ext; simp [mul_comm]
+
+end ContinuousLinearMap

LeanAPAP/Mathlib/Data/Set/Card.lean

@@ -0,0 +1,9 @@
+import Mathlib.Data.Set.Card
+
+open Function
+
+namespace Set
+variable {α β : Type*} {f : α → β}
+
+lemma encard_preimage_of_bijective (hf : Bijective f) (t : Set β) : (f ⁻¹' t).encard = t.encard :=
+  encard_preimage_of_injective_subset_range hf.injective (by simp [hf.surjective.range_eq])

LeanAPAP/Mathlib/MeasureTheory/Group/Measure.lean

@@ -0,0 +1,40 @@
+import Mathlib.Algebra.Group.Pointwise.Set.Card
+import Mathlib.MeasureTheory.Group.Measure
+import LeanAPAP.Mathlib.Data.Set.Card
+import LeanAPAP.Mathlib.MeasureTheory.Measure.Count
+
+open Set
+
+namespace MeasureTheory.Measure
+variable {G : Type*} [MeasurableSpace G] [Group G]
+
+section MeasurableMul
+variable [MeasurableMul G]
+
+@[to_additive]
+instance : (count : Measure G).IsMulLeftInvariant where
+  map_mul_left_eq_self g := by
+    ext s hs
+    rw [count_apply' hs, map_apply (measurable_const_mul _) hs,
+      count_apply' (measurable_const_mul _ hs),
+      encard_preimage_of_bijective (Group.mulLeft_bijective _)]
+
+@[to_additive]
+instance : (count : Measure G).IsMulRightInvariant where
+  map_mul_right_eq_self g := by
+    ext s hs
+    rw [count_apply' hs, map_apply (measurable_mul_const _) hs,
+      count_apply' (measurable_mul_const _ hs),
+      encard_preimage_of_bijective (Group.mulRight_bijective _)]
+
+end MeasurableMul
+
+section MeasurableInv
+variable [MeasurableInv G]
+
+@[to_additive]
+instance : (count : Measure G).IsInvInvariant where
+  inv_eq_self := by ext s hs; rw [count_apply' hs, inv_apply, count_apply' hs.inv, encard_inv]
+
+end MeasurableInv
+end MeasureTheory.Measure

LeanAPAP/Mathlib/MeasureTheory/Measure/Count.lean

@@ -0,0 +1,8 @@
+import Mathlib.MeasureTheory.Measure.Count
+import LeanAPAP.Mathlib.Topology.Algebra.InfiniteSum.ENNReal
+
+namespace MeasureTheory.Measure
+variable {α : Type*} [MeasurableSpace α]{s : Set α}
+
+lemma count_apply' (hs : MeasurableSet s) : count s = s.encard := by
+  simp [count_apply hs, ENNReal.tsum_const, Set.encard]

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

@@ -0,0 +1,23 @@
+import Mathlib.Topology.Algebra.InfiniteSum.ENNReal
+
+open Set
+
+namespace ENNReal
+variable {α : Type*} (s : Set α)
+
+-- TODO: Replace
+alias tsum_set_one := tsum_set_one_eq
+alias tsum_set_const := tsum_set_const_eq
+
+@[simp]
+lemma tsum_one : ∑' _ : α, (1 : ℝ≥0∞) = ENat.card α := by
+  rw [← tsum_univ]
+  simpa [-tsum_set_one_eq, -tsum_set_const_eq, encard_univ, tsum_univ] using tsum_set_one univ
+
+-- TODO: Delete `tsum_const_eq`
+@[simp]
+lemma tsum_const (c : ℝ≥0∞) : ∑' _ : α, c = ENat.card α * c := by
+  rw [← tsum_univ]
+  simpa [-tsum_set_one_eq, -tsum_set_const_eq, encard_univ, tsum_univ] using tsum_set_const univ c
+
+end ENNReal