From 7e00b8bada0cde15e8b7ee53876dae525e52b85a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= Date: Wed, 9 Apr 2025 18:09:20 +0000 Subject: [PATCH 1/2] Redefine `conv` using `MeasureTheory.convolution` --- .../MeasureTheory/Integral/Bochner/Basic.lean | 20 ++ .../Topology/Algebra/InfiniteSum/Basic.lean | 7 + LeanAPAP/Physics/Unbalancing.lean | 2 +- LeanAPAP/Prereqs/Convolution/Compact.lean | 7 +- .../Prereqs/Convolution/Discrete/Basic.lean | 2 +- .../Prereqs/Convolution/Discrete/Defs.lean | 225 ++++++++++++------ 6 files changed, 178 insertions(+), 85 deletions(-) create mode 100644 LeanAPAP/Mathlib/MeasureTheory/Integral/Bochner/Basic.lean create mode 100644 LeanAPAP/Mathlib/Topology/Algebra/InfiniteSum/Basic.lean diff --git a/LeanAPAP/Mathlib/MeasureTheory/Integral/Bochner/Basic.lean b/LeanAPAP/Mathlib/MeasureTheory/Integral/Bochner/Basic.lean new file mode 100644 index 0000000000..6178e85ff3 --- /dev/null +++ b/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 diff --git a/LeanAPAP/Mathlib/Topology/Algebra/InfiniteSum/Basic.lean b/LeanAPAP/Mathlib/Topology/Algebra/InfiniteSum/Basic.lean new file mode 100644 index 0000000000..472e6620ab --- /dev/null +++ b/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 diff --git a/LeanAPAP/Physics/Unbalancing.lean b/LeanAPAP/Physics/Unbalancing.lean index 37eaabecef..da7dd4304a 100644 --- a/LeanAPAP/Physics/Unbalancing.lean +++ b/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 diff --git a/LeanAPAP/Prereqs/Convolution/Compact.lean b/LeanAPAP/Prereqs/Convolution/Compact.lean index 8950396d6e..c4787fb0c5 100644 --- a/LeanAPAP/Prereqs/Convolution/Compact.lean +++ b/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 -/ diff --git a/LeanAPAP/Prereqs/Convolution/Discrete/Basic.lean b/LeanAPAP/Prereqs/Convolution/Discrete/Basic.lean index 3440f1e7a9..422bde2d85 100644 --- a/LeanAPAP/Prereqs/Convolution/Discrete/Basic.lean +++ b/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 diff --git a/LeanAPAP/Prereqs/Convolution/Discrete/Defs.lean b/LeanAPAP/Prereqs/Convolution/Discrete/Defs.lean index a0dca49c9f..c2872db221 100644 --- a/LeanAPAP/Prereqs/Convolution/Discrete/Defs.lean +++ b/LeanAPAP/Prereqs/Convolution/Discrete/Defs.lean @@ -1,3 +1,7 @@ +import LeanAPAP.Mathlib.Analysis.Convolution +import LeanAPAP.Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable +import LeanAPAP.Mathlib.MeasureTheory.Integral.Bochner.Basic +import LeanAPAP.Mathlib.Topology.Algebra.InfiniteSum.Basic import Mathlib.Algebra.Group.Translate import Mathlib.Algebra.Star.Conjneg import Mathlib.Analysis.Complex.Basic @@ -33,15 +37,16 @@ point in time. Multiplicativise? Probably ugly and not very useful. -/ -open Finset Fintype Function +open Finset Fintype Function MeasureTheory open scoped ComplexConjugate NNReal Pointwise translate -variable {G H R S : Type*} [DecidableEq G] [AddCommGroup G] +namespace Analysis.Discrete +variable {G H R S : Type*} [AddCommGroup G] /-! ### Trivial character -/ section CommSemiring -variable [CommSemiring R] +variable [DecidableEq G] [CommSemiring R] /-- The trivial character. -/ def trivChar : G → R := fun a ↦ if a = 0 then 1 else 0 @@ -57,103 +62,175 @@ variable [StarRing R] end CommSemiring -variable [Fintype G] - /-! ### Convolution -/ -section CommSemiring -variable [CommSemiring R] {f g : G → R} - -/-- Convolution -/ -def conv (f g : G → R) : G → R := fun a ↦ ∑ x : G × G with x.1 + x.2 = a , f x.1 * g x.2 +section NormedRing +variable [NormedRing R] [NormedSpace ℝ R] [IsScalarTower ℝ R R] [SMulCommClass ℝ R R] + [NormedRing S] [NormedSpace ℝ S] [IsScalarTower ℝ S S] [SMulCommClass ℝ S S] + [MeasurableSpace G] {f g : G → R} {a b : G} -infixl:71 " ∗ " => conv +/-- Discrete convolution. -/ +noncomputable abbrev conv (f g : G → R) : G → R := convolution f g (.mul ℝ _) .count -lemma conv_apply (f g : G → R) (a : G) : - (f ∗ g) a = ∑ x : G × G with x.1 + x.2 = a, f x.1 * g x.2 := rfl +scoped infixl:71 " ∗ " => conv -@[simp] lemma conv_zero (f : G → R) : f ∗ 0 = 0 := by ext; simp [conv_apply] -@[simp] lemma zero_conv (f : G → R) : 0 ∗ f = 0 := by ext; simp [conv_apply] +lemma conv_zero (f : G → R) : f ∗ 0 = 0 := convolution_zero +lemma zero_conv (f : G → R) : 0 ∗ f = 0 := zero_convolution -lemma conv_add (f g h : G → R) : f ∗ (g + h) = f ∗ g + f ∗ h := by - ext; simp [conv_apply, mul_add, sum_add_distrib] +section SMul +variable [CommSemiring H] [Algebra H ℝ] [Module H R] [IsScalarTower H ℝ R] -lemma add_conv (f g h : G → R) : (f + g) ∗ h = f ∗ h + g ∗ h := by - ext; simp [conv_apply, add_mul, sum_add_distrib] +lemma smul_conv (c : H) (f g : G → R) : c • f ∗ g = c • (f ∗ g) := by + rw [conv, ← algebraMap_smul ℝ, smul_convolution, algebraMap_smul] -lemma smul_conv [DistribSMul H R] [IsScalarTower H R R] (c : H) (f g : G → R) : - c • f ∗ g = c • (f ∗ g) := by ext a; simp [conv_apply, smul_sum, smul_mul_assoc] +lemma conv_smul (c : H) (f g : G → R) : f ∗ c • g = c • (f ∗ g) := by + rw [conv, ← algebraMap_smul ℝ, convolution_smul, algebraMap_smul] -lemma conv_smul [DistribSMul H R] [SMulCommClass H R R] (c : H) (f g : G → R) : - f ∗ c • g = c • (f ∗ g) := by ext a; simp [conv_apply, smul_sum, mul_smul_comm] +lemma mul_smul_conv_comm (c d : H) (f g : G → R) : (c * d) • (f ∗ g) = c • f ∗ d • g := by + rw [smul_conv, conv_smul, mul_smul] alias smul_conv_assoc := smul_conv alias smul_conv_left_comm := conv_smul -@[simp] lemma translate_conv (a : G) (f g : G → R) : τ a f ∗ g = τ a (f ∗ g) := - funext fun b ↦ sum_equiv ((Equiv.subRight a).prodCongr <| Equiv.refl _) - (by simp [sub_add_eq_add_sub]) (by simp) +end SMul @[simp] lemma conv_translate (a : G) (f g : G → R) : f ∗ τ a g = τ a (f ∗ g) := - funext fun b ↦ sum_equiv ((Equiv.refl _).prodCongr <| Equiv.subRight a) - (by simp [← add_sub_assoc]) (by simp) + convolution_translate .. -lemma conv_comm (f g : G → R) : f ∗ g = g ∗ f := - funext fun a ↦ sum_equiv (Equiv.prodComm _ _) (by simp [add_comm]) <| by simp [mul_comm] +@[simp] lemma translate_conv [MeasurableAdd G] (a : G) (f g : G → R) : τ a f ∗ g = τ a (f ∗ g) := + translate_convolution .. -lemma mul_smul_conv_comm [Monoid H] [DistribMulAction H R] [IsScalarTower H R R] - [SMulCommClass H R R] (c d : H) (f g : G → R) : (c * d) • (f ∗ g) = c • f ∗ d • g := by - rw [smul_conv, conv_smul, mul_smul] +/-- The convolution of `f` and `g` exists at `a` when the function `t ↦ f t * g (a - t)` is +summable. -/ +def ConvExistsAt (f g : G → R) (a : G) : Prop := Summable fun t ↦ ‖f t‖ * ‖g (a - t)‖ -lemma conv_assoc (f g h : G → R) : f ∗ g ∗ h = f ∗ (g ∗ h) := by - ext a - simp only [sum_mul, mul_sum, conv_apply, Finset.sum_sigma'] - apply sum_nbij' (fun ⟨(_b, c), (d, e)⟩ ↦ ⟨(d, e + c), (e, c)⟩) - (fun ⟨(b, _c), (d, e)⟩ ↦ ⟨(b + d, e), (b, d)⟩) <;> aesop (add simp [add_assoc, mul_assoc]) +/-- The convolution of `f` and `g` exists when the function `t ↦ f t * g (a - t)` is summable +for all `a`. -/ +def ConvExists (f g : G → R) : Prop := ∀ a, ConvExistsAt f g a -lemma conv_right_comm (f g h : G → R) : f ∗ g ∗ h = f ∗ h ∗ g := by - rw [conv_assoc, conv_assoc, conv_comm g] +lemma convolutionExistsAt_mul_count [NormMulClass R] [MeasurableSingletonClass G] : + ConvolutionExistsAt f g a (.mul ℝ R) .count ↔ ConvExistsAt f g a := by + simp [ConvolutionExistsAt, ConvExistsAt, integrable_count_iff, norm_mul] -lemma conv_left_comm (f g h : G → R) : f ∗ (g ∗ h) = g ∗ (f ∗ h) := by - rw [← conv_assoc, ← conv_assoc, conv_comm g] +lemma convolutionExists_mul_count [NormMulClass R] [MeasurableSingletonClass G] : + ConvolutionExists f g (.mul ℝ R) .count ↔ ConvExists f g := by + simp [ConvolutionExists, ConvExists, convolutionExistsAt_mul_count] -lemma conv_rotate (f g h : G → R) : f ∗ g ∗ h = g ∗ h ∗ f := by rw [conv_assoc, conv_comm] -lemma conv_rotate' (f g h : G → R) : f ∗ (g ∗ h) = g ∗ (h ∗ f) := by rw [conv_comm, ← conv_assoc] +alias ⟨_, ConvExistsAt.convolutionExistsAt⟩ := convolutionExistsAt_mul_count +alias ⟨_, ConvExists.convolutionExists⟩ := convolutionExists_mul_count -lemma conv_conv_conv_comm (f g h i : G → R) : f ∗ g ∗ (h ∗ i) = f ∗ h ∗ (g ∗ i) := by - rw [conv_assoc, conv_assoc, conv_left_comm g] +section Countable +variable [CompleteSpace R] [NormMulClass R] [Countable G] [MeasurableSingletonClass G] -lemma map_conv [CommSemiring S] (m : R →+* S) (f g : G → R) (a : G) : - m ((f ∗ g) a) = (m ∘ f ∗ m ∘ g) a := by simp [conv_apply, map_sum, map_mul] +lemma conv_eq_tsum_sub (hfg : ConvExistsAt f g a) : (f ∗ g) a = ∑' t, f t * g (a - t) := by + simpa using integral_countable' hfg.convolutionExistsAt -lemma comp_conv [CommSemiring S] (m : R →+* S) (f g : G → R) : m ∘ (f ∗ g) = m ∘ f ∗ m ∘ g := - funext <| map_conv _ _ _ +lemma conv_eq_tsum_sub' (hfg : ConvExistsAt f g a) : (f ∗ g) a = ∑' t, f (a - t) * g t := by + rw [conv_eq_tsum_sub hfg]; exact tsum_equiv (.subLeft a) _ _ (by simp) + +lemma conv_eq_tsum_add (hfg : ConvExistsAt f g a) : (f ∗ g) a = ∑' t, f (a + t) * g (-t) := by + rw [conv_eq_tsum_sub hfg]; exact tsum_equiv (.subRight a) _ _ (by simp) + +lemma conv_eq_tsum_add' (hfg : ConvExistsAt f g a) : (f ∗ g) a = ∑' t, f (-t) * g (a + t) := by + rw [conv_eq_tsum_sub hfg]; exact tsum_equiv (.neg _) _ _ (by simp [sub_eq_add_neg]) + +lemma conv_apply_add (hfg : ConvExistsAt f g (a + b)) : + (f ∗ g) (a + b) = ∑' t, f (a + t) * g (b - t) := by + rw [conv_eq_tsum_sub hfg]; exact tsum_equiv (.subRight a) _ _ (by simp [sub_sub_eq_add_sub, add_comm]) + +lemma sum_conv_mul (f g h : G → R) : ∑' a, (f ∗ g) a * h a = ∑' a, ∑' b, f a * g b * h (a + b) := by + simp_rw [conv_eq_tsum_sub, sum_mul] + rw [sum_comm] + exact sum_congr rfl fun x _ ↦ sum_equiv (.subRight x) _ _ fun y ↦ by simp + +lemma sum_conv (f g : G → R) : ∑ a, (f ∗ g) a = (∑ a, f a) * ∑ a, g a := by + simpa only [Countable.sum_mul_sum, Pi.one_apply, mul_one] using sum_conv_mul f g 1 -lemma conv_eq_sum_sub (f g : G → R) (a : G) : (f ∗ g) a = ∑ t, f (a - t) * g t := by - rw [conv_apply]; apply sum_nbij' Prod.snd (fun b ↦ (a - b, b)) <;> aesop +lemma conv_eq_sum [DecidableEq G] (hfg : ConvExistsAt f g a) : + (f ∗ g) a = ∑ x : G × G with x.1 + x.2 = a, f x.1 * g x.2 := by + rw [conv_eq_sum_sub]; symm; apply sum_nbij' Prod.snd (fun b ↦ (a - b, b)) <;> aesop -lemma conv_eq_sum_add (f g : G → R) (a : G) : (f ∗ g) a = ∑ t, f (a + t) * g (-t) := - (conv_eq_sum_sub _ _ _).trans <| Fintype.sum_equiv (Equiv.neg _) _ _ fun t ↦ by - simp only [sub_eq_add_neg, Equiv.neg_apply, neg_neg] +end Countable -lemma conv_eq_sum_sub' (f g : G → R) (a : G) : (f ∗ g) a = ∑ t, f t * g (a - t) := by - rw [conv_comm, conv_eq_sum_sub]; simp_rw [mul_comm] +section Fintype +variable [CompleteSpace R] [Fintype G] [MeasurableSingletonClass G] + +lemma conv_eq_sum_sub (f g : G → R) (a : G) : (f ∗ g) a = ∑ t, f t * g (a - t) := by + simp [conv, convolution, tsum_fintype] + +lemma conv_eq_sum_sub' (f g : G → R) (a : G) : (f ∗ g) a = ∑ t, f (a - t) * g t := by + rw [conv_eq_sum_sub]; exact sum_equiv (.subLeft a) _ _ (by simp) + +lemma conv_eq_sum_add (f g : G → R) (a : G) : (f ∗ g) a = ∑ t, f (a + t) * g (-t) := by + rw [conv_eq_sum_sub]; exact sum_equiv (.subRight a) _ _ (by simp) lemma conv_eq_sum_add' (f g : G → R) (a : G) : (f ∗ g) a = ∑ t, f (-t) * g (a + t) := by - rw [conv_comm, conv_eq_sum_add]; simp_rw [mul_comm] + rw [conv_eq_sum_sub]; exact sum_equiv (.neg _) _ _ (by simp [sub_eq_add_neg]) -lemma conv_apply_add (f g : G → R) (a b : G) : (f ∗ g) (a + b) = ∑ t, f (a + t) * g (b - t) := - (conv_eq_sum_sub _ _ _).trans <| Fintype.sum_equiv (Equiv.subLeft b) _ _ fun t ↦ by - simp [add_sub_assoc, ← sub_add] +lemma conv_apply_add (f g : G → R) (a b : G) : (f ∗ g) (a + b) = ∑ t, f (a + t) * g (b - t) := by + rw [conv_eq_sum_sub]; exact sum_equiv (.subRight a) _ _ (by simp [sub_sub_eq_add_sub, add_comm]) lemma sum_conv_mul (f g h : G → R) : ∑ a, (f ∗ g) a * h a = ∑ a, ∑ b, f a * g b * h (a + b) := by - simp_rw [conv_eq_sum_sub', sum_mul] + simp_rw [conv_eq_sum_sub, sum_mul] rw [sum_comm] - exact sum_congr rfl fun x _ ↦ Fintype.sum_equiv (Equiv.subRight x) _ _ fun y ↦ by simp + exact sum_congr rfl fun x _ ↦ sum_equiv (.subRight x) _ _ fun y ↦ by simp lemma sum_conv (f g : G → R) : ∑ a, (f ∗ g) a = (∑ a, f a) * ∑ a, g a := by simpa only [Fintype.sum_mul_sum, Pi.one_apply, mul_one] using sum_conv_mul f g 1 +lemma conv_eq_sum [DecidableEq G] (f g : G → R) (a : G) : + (f ∗ g) a = ∑ x : G × G with x.1 + x.2 = a, f x.1 * g x.2 := by + rw [conv_eq_sum_sub]; symm; apply sum_nbij' Prod.snd (fun b ↦ (a - b, b)) <;> aesop + +end Fintype + +section Finite +variable [Finite G] [MeasurableSingletonClass G] + +lemma conv_add (f g h : G → R) : f ∗ (g + h) = f ∗ g + f ∗ h := + ConvolutionExists.distrib_add .of_finite .of_finite + +lemma add_conv (f g h : G → R) : (f + g) ∗ h = f ∗ h + g ∗ h := + ConvolutionExists.add_distrib .of_finite .of_finite + +lemma map_conv (m : R →+* S) (f g : G → R) (a : G) : m ((f ∗ g) a) = (m ∘ f ∗ m ∘ g) a := by + cases nonempty_fintype G + simp [conv_eq_sum, map_sum, map_mul] + +lemma comp_conv [CommSemiring S] (m : R →+* S) (f g : G → R) : m ∘ (f ∗ g) = m ∘ f ∗ m ∘ g := + funext $ map_conv _ _ _ + +variable [CompleteSpace R] + +lemma conv_assoc (f g h : G → R) : f ∗ g ∗ h = f ∗ (g ∗ h) := + convolution_assoc'' _ _ _ _ mul_assoc .of_discrete .of_discrete .of_discrete + (.of_forall fun _ ↦ .of_finite) (.of_forall fun _ ↦ .of_finite) .of_finite + +end Finite + +end NormedRing + +section NormedCommRing +variable [NormedCommRing R] [NormedSpace ℝ R] [IsScalarTower ℝ R R] [SMulCommClass ℝ R R] + [MeasurableSpace G] {f g : G → R} + +lemma conv_comm [MeasurableAdd G] [MeasurableNeg G] (f g : G → R) : f ∗ g = g ∗ f := + .trans (by simp) (convolution_flip _) + +variable [MeasurableSingletonClass G] [Finite G] [CompleteSpace R] + +lemma conv_right_comm (f g h : G → R) : f ∗ g ∗ h = f ∗ h ∗ g := by + rw [conv_assoc, conv_assoc, conv_comm g] + +lemma conv_left_comm (f g h : G → R) : f ∗ (g ∗ h) = g ∗ (f ∗ h) := by + rw [← conv_assoc, ← conv_assoc, conv_comm g] + +lemma conv_rotate (f g h : G → R) : f ∗ g ∗ h = g ∗ h ∗ f := by rw [conv_assoc, conv_comm] +lemma conv_rotate' (f g h : G → R) : f ∗ (g ∗ h) = g ∗ (h ∗ f) := by rw [conv_comm, ← conv_assoc] + +lemma conv_conv_conv_comm (f g h i : G → R) : f ∗ g ∗ (h ∗ i) = f ∗ h ∗ (g ∗ i) := by + rw [conv_assoc, conv_assoc, conv_left_comm g] + @[simp] lemma conv_const (f : G → R) (b : R) : f ∗ const _ b = const _ ((∑ x, f x) * b) := by ext; simp [conv_eq_sum_sub', sum_mul] @@ -211,7 +288,7 @@ lemma dconv_smul [Star H] [DistribSMul H R] [SMulCommClass H R R] [StarModule H rw [← conv_conjneg, conjneg_conjneg] @[simp] lemma conj_conv_apply (f g : G → R) (a : G) : conj ((f ∗ g) a) = (conj f ∗ conj g) a := by - simp only [Pi.conj_apply, conv_apply, map_sum, map_mul] + simp only [Pi.conj_apply, conv_eq_sum, map_sum, map_mul] @[simp] lemma conj_dconv_apply (f g : G → R) (a : G) : conj ((f ○ g) a) = (conj f ○ conj g) a := by simp_rw [← conv_conjneg, conj_conv_apply, conjneg_conj] @@ -230,7 +307,7 @@ lemma IsSelfAdjoint.dconv (hf : IsSelfAdjoint f) (hg : IsSelfAdjoint g) : IsSelf @[simp]lemma conjneg_conv (f g : G → R) : conjneg (f ∗ g) = conjneg f ∗ conjneg g := by funext a - simp only [conv_apply, conjneg_apply, map_sum, map_mul] + simp only [conv_eq_sum, conjneg_apply, map_sum, map_mul] exact sum_equiv (Equiv.neg _) (by simp [← neg_eq_iff_eq_neg, add_comm]) (by simp) @[simp] lemma conjneg_dconv (f g : G → R) : conjneg (f ○ g) = g ○ f := by @@ -313,8 +390,8 @@ end CommSemiring section CommRing variable [CommRing R] -@[simp] lemma conv_neg (f g : G → R) : f ∗ -g = -(f ∗ g) := by ext; simp [conv_apply] -@[simp] lemma neg_conv (f g : G → R) : -f ∗ g = -(f ∗ g) := by ext; simp [conv_apply] +@[simp] lemma conv_neg (f g : G → R) : f ∗ -g = -(f ∗ g) := by ext; simp [conv_eq_sum] +@[simp] lemma neg_conv (f g : G → R) : -f ∗ g = -(f ∗ g) := by ext; simp [conv_eq_sum] lemma conv_sub (f g h : G → R) : f ∗ (g - h) = f ∗ g - f ∗ h := by simp only [sub_eq_add_neg, conv_add, conv_neg] @@ -474,18 +551,12 @@ lemma conjneg_iterConv (f : G → R) : ∀ n, conjneg (f ∗^ n) = conjneg f ∗ end CommSemiring -namespace NNReal - @[simp, norm_cast] -lemma ofReal_iterConv (f : G → ℝ≥0) (n : ℕ) (a : G) : (↑((f ∗^ n) a) : ℝ) = ((↑) ∘ f ∗^ n) a := +lemma nnrealToReal_iterConv (f : G → ℝ≥0) (n : ℕ) (a : G) : (↑((f ∗^ n) a) : ℝ) = ((↑) ∘ f ∗^ n) a := map_iterConv NNReal.toRealHom _ _ _ -end NNReal - -namespace Complex - @[simp, norm_cast] -lemma ofReal_iterConv (f : G → ℝ) (n : ℕ) (a : G) : (↑((f ∗^ n) a) : ℂ) = ((↑) ∘ f ∗^ n) a := - map_iterConv ofRealHom _ _ _ +lemma complexOfReal_iterConv (f : G → ℝ) (n : ℕ) (a : G) : (↑((f ∗^ n) a) : ℂ) = ((↑) ∘ f ∗^ n) a := + map_iterConv Complex.ofRealHom _ _ _ -end Complex +end Analysis.Discrete From 2768c2956d4bb2775cc3d01d3ff842242abfe5f1 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= Date: Wed, 9 Apr 2025 19:26:29 +0000 Subject: [PATCH 2/2] more --- LeanAPAP.lean | 2 + LeanAPAP/Mathlib/Analysis/Convolution.lean | 35 +++++- .../Prereqs/Convolution/Discrete/Defs.lean | 112 ++++++++++-------- 3 files changed, 95 insertions(+), 54 deletions(-) diff --git a/LeanAPAP.lean b/LeanAPAP.lean index 7b42652f24..c4c44b346f 100644 --- a/LeanAPAP.lean +++ b/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 diff --git a/LeanAPAP/Mathlib/Analysis/Convolution.lean b/LeanAPAP/Mathlib/Analysis/Convolution.lean index 698d738c07..672d938206 100644 --- a/LeanAPAP/Mathlib/Analysis/Convolution.lean +++ b/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 diff --git a/LeanAPAP/Prereqs/Convolution/Discrete/Defs.lean b/LeanAPAP/Prereqs/Convolution/Discrete/Defs.lean index c2872db221..60bd4f1f29 100644 --- a/LeanAPAP/Prereqs/Convolution/Discrete/Defs.lean +++ b/LeanAPAP/Prereqs/Convolution/Discrete/Defs.lean @@ -41,7 +41,7 @@ open Finset Fintype Function MeasureTheory open scoped ComplexConjugate NNReal Pointwise translate namespace Analysis.Discrete -variable {G H R S : Type*} [AddCommGroup G] +variable {G H K R S : Type*} [AddCommGroup G] /-! ### Trivial character -/ @@ -65,9 +65,32 @@ end CommSemiring /-! ### Convolution -/ section NormedRing -variable [NormedRing R] [NormedSpace ℝ R] [IsScalarTower ℝ R R] [SMulCommClass ℝ R R] +variable [NormedRing R] {f g : G → R} {a b : G} + +/-- The convolution of `f` and `g` exists at `a` when the function `t ↦ f t * g (a - t)` is +summable. -/ +def ConvExistsAt (f g : G → R) (a : G) : Prop := Summable fun t ↦ ‖f t * g (a - t)‖ + +/-- The convolution of `f` and `g` exists when the function `t ↦ f t * g (a - t)` is summable +for all `a`. -/ +def ConvExists (f g : G → R) : Prop := ∀ a, ConvExistsAt f g a + +@[simp] lemma ConvExistsAt.of_finite [Finite G] : ConvExistsAt f g a := Summable.of_finite +@[simp] lemma ConvExists.of_finite [Finite G] : ConvExists f g := fun _ ↦ .of_finite + +variable [MeasurableSpace G] [NormedSpace ℝ R] [IsScalarTower ℝ R R] [SMulCommClass ℝ R R] [NormedRing S] [NormedSpace ℝ S] [IsScalarTower ℝ S S] [SMulCommClass ℝ S S] - [MeasurableSpace G] {f g : G → R} {a b : G} + +lemma convolutionExistsAt_mul_count [MeasurableSingletonClass G] : + ConvolutionExistsAt f g a (.mul ℝ R) .count ↔ ConvExistsAt f g a := by + simp [ConvolutionExistsAt, ConvExistsAt, integrable_count_iff] + +lemma convolutionExists_mul_count [MeasurableSingletonClass G] : + ConvolutionExists f g (.mul ℝ R) .count ↔ ConvExists f g := by + simp [ConvolutionExists, ConvExists, convolutionExistsAt_mul_count] + +alias ⟨_, ConvExistsAt.convolutionExistsAt⟩ := convolutionExistsAt_mul_count +alias ⟨_, ConvExists.convolutionExists⟩ := convolutionExists_mul_count /-- Discrete convolution. -/ noncomputable abbrev conv (f g : G → R) : G → R := convolution f g (.mul ℝ _) .count @@ -100,27 +123,8 @@ end SMul @[simp] lemma translate_conv [MeasurableAdd G] (a : G) (f g : G → R) : τ a f ∗ g = τ a (f ∗ g) := translate_convolution .. -/-- The convolution of `f` and `g` exists at `a` when the function `t ↦ f t * g (a - t)` is -summable. -/ -def ConvExistsAt (f g : G → R) (a : G) : Prop := Summable fun t ↦ ‖f t‖ * ‖g (a - t)‖ - -/-- The convolution of `f` and `g` exists when the function `t ↦ f t * g (a - t)` is summable -for all `a`. -/ -def ConvExists (f g : G → R) : Prop := ∀ a, ConvExistsAt f g a - -lemma convolutionExistsAt_mul_count [NormMulClass R] [MeasurableSingletonClass G] : - ConvolutionExistsAt f g a (.mul ℝ R) .count ↔ ConvExistsAt f g a := by - simp [ConvolutionExistsAt, ConvExistsAt, integrable_count_iff, norm_mul] - -lemma convolutionExists_mul_count [NormMulClass R] [MeasurableSingletonClass G] : - ConvolutionExists f g (.mul ℝ R) .count ↔ ConvExists f g := by - simp [ConvolutionExists, ConvExists, convolutionExistsAt_mul_count] - -alias ⟨_, ConvExistsAt.convolutionExistsAt⟩ := convolutionExistsAt_mul_count -alias ⟨_, ConvExists.convolutionExists⟩ := convolutionExists_mul_count - section Countable -variable [CompleteSpace R] [NormMulClass R] [Countable G] [MeasurableSingletonClass G] +variable [CompleteSpace R] [Countable G] [MeasurableSingletonClass G] lemma conv_eq_tsum_sub (hfg : ConvExistsAt f g a) : (f ∗ g) a = ∑' t, f t * g (a - t) := by simpa using integral_countable' hfg.convolutionExistsAt @@ -128,27 +132,16 @@ lemma conv_eq_tsum_sub (hfg : ConvExistsAt f g a) : (f ∗ g) a = ∑' t, f t * lemma conv_eq_tsum_sub' (hfg : ConvExistsAt f g a) : (f ∗ g) a = ∑' t, f (a - t) * g t := by rw [conv_eq_tsum_sub hfg]; exact tsum_equiv (.subLeft a) _ _ (by simp) -lemma conv_eq_tsum_add (hfg : ConvExistsAt f g a) : (f ∗ g) a = ∑' t, f (a + t) * g (-t) := by +lemma conv_eq_tsum_add_neg (hfg : ConvExistsAt f g a) : (f ∗ g) a = ∑' t, f (a + t) * g (-t) := by rw [conv_eq_tsum_sub hfg]; exact tsum_equiv (.subRight a) _ _ (by simp) -lemma conv_eq_tsum_add' (hfg : ConvExistsAt f g a) : (f ∗ g) a = ∑' t, f (-t) * g (a + t) := by +lemma conv_eq_tsum_neg_add (hfg : ConvExistsAt f g a) : (f ∗ g) a = ∑' t, f (-t) * g (a + t) := by rw [conv_eq_tsum_sub hfg]; exact tsum_equiv (.neg _) _ _ (by simp [sub_eq_add_neg]) -lemma conv_apply_add (hfg : ConvExistsAt f g (a + b)) : +lemma conv_apply_add_eq_tsum_add_sub (hfg : ConvExistsAt f g (a + b)) : (f ∗ g) (a + b) = ∑' t, f (a + t) * g (b - t) := by - rw [conv_eq_tsum_sub hfg]; exact tsum_equiv (.subRight a) _ _ (by simp [sub_sub_eq_add_sub, add_comm]) - -lemma sum_conv_mul (f g h : G → R) : ∑' a, (f ∗ g) a * h a = ∑' a, ∑' b, f a * g b * h (a + b) := by - simp_rw [conv_eq_tsum_sub, sum_mul] - rw [sum_comm] - exact sum_congr rfl fun x _ ↦ sum_equiv (.subRight x) _ _ fun y ↦ by simp - -lemma sum_conv (f g : G → R) : ∑ a, (f ∗ g) a = (∑ a, f a) * ∑ a, g a := by - simpa only [Countable.sum_mul_sum, Pi.one_apply, mul_one] using sum_conv_mul f g 1 - -lemma conv_eq_sum [DecidableEq G] (hfg : ConvExistsAt f g a) : - (f ∗ g) a = ∑ x : G × G with x.1 + x.2 = a, f x.1 * g x.2 := by - rw [conv_eq_sum_sub]; symm; apply sum_nbij' Prod.snd (fun b ↦ (a - b, b)) <;> aesop + rw [conv_eq_tsum_sub hfg] + exact tsum_equiv (.subRight a) _ _ (by simp [sub_sub_eq_add_sub, add_comm]) end Countable @@ -156,16 +149,16 @@ section Fintype variable [CompleteSpace R] [Fintype G] [MeasurableSingletonClass G] lemma conv_eq_sum_sub (f g : G → R) (a : G) : (f ∗ g) a = ∑ t, f t * g (a - t) := by - simp [conv, convolution, tsum_fintype] + simp [conv_eq_tsum_sub, tsum_fintype] lemma conv_eq_sum_sub' (f g : G → R) (a : G) : (f ∗ g) a = ∑ t, f (a - t) * g t := by - rw [conv_eq_sum_sub]; exact sum_equiv (.subLeft a) _ _ (by simp) + simp [conv_eq_tsum_sub', tsum_fintype] -lemma conv_eq_sum_add (f g : G → R) (a : G) : (f ∗ g) a = ∑ t, f (a + t) * g (-t) := by - rw [conv_eq_sum_sub]; exact sum_equiv (.subRight a) _ _ (by simp) +lemma conv_eq_sum_add_neg (f g : G → R) (a : G) : (f ∗ g) a = ∑ t, f (a + t) * g (-t) := by + simp [conv_eq_tsum_add_neg, tsum_fintype] lemma conv_eq_sum_add' (f g : G → R) (a : G) : (f ∗ g) a = ∑ t, f (-t) * g (a + t) := by - rw [conv_eq_sum_sub]; exact sum_equiv (.neg _) _ _ (by simp [sub_eq_add_neg]) + simp [conv_eq_tsum_neg_add, tsum_fintype] lemma conv_apply_add (f g : G → R) (a b : G) : (f ∗ g) (a + b) = ∑ t, f (a + t) * g (b - t) := by rw [conv_eq_sum_sub]; exact sum_equiv (.subRight a) _ _ (by simp [sub_sub_eq_add_sub, add_comm]) @@ -180,7 +173,7 @@ lemma sum_conv (f g : G → R) : ∑ a, (f ∗ g) a = (∑ a, f a) * ∑ a, g a lemma conv_eq_sum [DecidableEq G] (f g : G → R) (a : G) : (f ∗ g) a = ∑ x : G × G with x.1 + x.2 = a, f x.1 * g x.2 := by - rw [conv_eq_sum_sub]; symm; apply sum_nbij' Prod.snd (fun b ↦ (a - b, b)) <;> aesop + rw [conv_eq_sum_sub']; symm; apply sum_nbij' Prod.snd (fun b ↦ (a - b, b)) <;> aesop end Fintype @@ -193,14 +186,15 @@ lemma conv_add (f g h : G → R) : f ∗ (g + h) = f ∗ g + f ∗ h := lemma add_conv (f g h : G → R) : (f + g) ∗ h = f ∗ h + g ∗ h := ConvolutionExists.add_distrib .of_finite .of_finite -lemma map_conv (m : R →+* S) (f g : G → R) (a : G) : m ((f ∗ g) a) = (m ∘ f ∗ m ∘ g) a := by +variable [CompleteSpace R] [CompleteSpace S] + +lemma map_conv (m : R →+* S) (f g : G → R) (a : G) : m ((f ∗ g) a) = (m ∘ f ∗ m ∘ g) a := by + classical cases nonempty_fintype G simp [conv_eq_sum, map_sum, map_mul] -lemma comp_conv [CommSemiring S] (m : R →+* S) (f g : G → R) : m ∘ (f ∗ g) = m ∘ f ∗ m ∘ g := - funext $ map_conv _ _ _ - -variable [CompleteSpace R] +lemma comp_conv (m : R →+* S) (f g : G → R) : m ∘ (f ∗ g) = m ∘ f ∗ m ∘ g := + funext <| map_conv _ _ _ lemma conv_assoc (f g h : G → R) : f ∗ g ∗ h = f ∗ (g ∗ h) := convolution_assoc'' _ _ _ _ mul_assoc .of_discrete .of_discrete .of_discrete @@ -245,6 +239,24 @@ lemma support_conv_subset (f g : G → R) : support (f ∗ g) ⊆ support f + su obtain ⟨x, hx, h⟩ := exists_ne_zero_of_sum_ne_zero ha exact ⟨_, left_ne_zero_of_mul h, _, right_ne_zero_of_mul h, (mem_filter.1 hx).2⟩ +end NormedCommRing + +section NormedField +variable [NormedField K] [CompleteSpace K] [NormedSpace ℝ K] [IsScalarTower ℝ K K] [Countable G] + [MeasurableSpace G] [MeasurableSingletonClass G] {f g : G → K} {a b : G} + +lemma tsum_conv_mul (hfg : ConvExists f g) (h : G → K) : + ∑' a, (f ∗ g) a * h a = ∑' a, ∑' b, f a * g b * h (a + b) := by + simp_rw [conv_eq_tsum_sub (hfg _), ← tsum_mul_right] + rw [tsum_comm] + exact tsum_congr fun x ↦ tsum_equiv (.subRight x) _ _ fun y ↦ by simp + sorry + +lemma tsum_conv (hfg : ConvExists f g) : ∑' a, (f ∗ g) a = (∑' a, f a) * ∑' a, g a := by + simpa only [tsum_mul_tsum, Pi.one_apply, mul_one] using tsum_conv_mul hfg 1 + +end NormedField + /-! ### Difference convolution -/ variable [StarRing R]