convolution_lsmul
theorem convolution_lsmul :
∀ {𝕜 : Type u𝕜} {G : Type uG} {F : Type uF} [inst : NormedAddCommGroup F] {x : G}
[inst_1 : NontriviallyNormedField 𝕜] [inst_2 : NormedSpace 𝕜 F] [inst_3 : MeasurableSpace G]
{μ : MeasureTheory.Measure G} [inst_4 : NormedSpace ℝ F] [inst_5 : Sub G] {f : G → 𝕜} {g : G → F},
convolution f g (ContinuousLinearMap.lsmul 𝕜 𝕜) μ x = ∫ (t : G), f t • g (x - t) ∂μ
This theorem defines the convolution of two functions `f` and `g` in the context of scalar multiplication. More precisely, for any given types `𝕜` (representing a nontrivially normed field), `G` (a measurable space), and `F` (a normed add commutative group), and a measure `μ` on `G`, the convolution of `f` (a function from `G` to `𝕜`) and `g` (a function from `G` to `F`) under the linear scalar multiplication operator equals the integral over `G` of the function that maps `t` to the scalar product of `f(t)` and `g(x - t)`, where `x` is any given element of `G`.
More concisely: For functions `f` from a measurable space `G` to a nontrivially normed field `𝕜` and `g` from `G` to a normed add commutative group `F`, and a measure `μ` on `G`, the convolution of `f` and `g` under scalar multiplication is equal to the integral over `G` of the scalar product of `f(t)` and `g(x - t)` with respect to `μ`.
|
contDiffOn_convolution_right_with_param
theorem contDiffOn_convolution_right_with_param :
∀ {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} {P : Type uP}
[inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup E'] [inst_2 : NormedAddCommGroup F] [inst_3 : RCLike 𝕜]
[inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜 E'] [inst_6 : NormedSpace ℝ F] [inst_7 : NormedSpace 𝕜 F]
[inst_8 : CompleteSpace F] [inst_9 : MeasurableSpace G] [inst_10 : NormedAddCommGroup G] [inst_11 : BorelSpace G]
[inst_12 : NormedSpace 𝕜 G] [inst_13 : NormedAddCommGroup P] [inst_14 : NormedSpace 𝕜 P]
{μ : MeasureTheory.Measure G} {f : G → E} {n : ℕ∞} (L : E →L[𝕜] E' →L[𝕜] F) {g : P → G → E'} {s : Set P}
{k : Set G},
IsOpen s →
IsCompact k →
(∀ (p : P) (x : G), p ∈ s → x ∉ k → g p x = 0) →
MeasureTheory.LocallyIntegrable f μ →
ContDiffOn 𝕜 n (↿g) (s ×ˢ Set.univ) →
ContDiffOn 𝕜 n (fun q => convolution f (g q.1) L μ q.2) (s ×ˢ Set.univ)
The theorem `contDiffOn_convolution_right_with_param` states that for every `𝕜`, `G`, `E`, `E'`, `F`, `P` and natural number `n`, given a continuous linear map `L` from `E` into the space of continuous linear maps from `E'` to `F`, a function `f` from `G` to `E`, a function `g` from `P` into the functions from `G` to `E'`, a set `s` of `P`, and a set `k` of `G`, if `s` is open, `k` is compact, for every `p` in `s` and `x` not in `k` we have `g p x` is equal to `0`, `f` is locally integrable with respect to a measure `μ`, and `g` is continuously differentiable `n` times on the product of `s` and the set of all points in `G`, then the function which takes a point `q` in the product of `s` and the set of all points in `G` and maps it to the convolution of `f` and `g q.1` with respect to `L` and `μ` at `q.2` is continuously differentiable `n` times on the product of `s` and the set of all points in `G`.
In simpler terms, this theorem asserts that the convolution of a locally integrable function and a continuously differentiable function with compact support is itself continuously differentiable when the functions and their properties meet certain conditions.
More concisely: Given a locally integrable function, a continuously differentiable function with compact support, and a continuous linear map between function spaces, their convolution is a continuously differentiable function if the functions and the map satisfy the given conditions.
|
contDiffOn_convolution_right_with_param_comp
theorem contDiffOn_convolution_right_with_param_comp :
∀ {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} {P : Type uP}
[inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup E'] [inst_2 : NormedAddCommGroup F] [inst_3 : RCLike 𝕜]
[inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜 E'] [inst_6 : NormedSpace ℝ F] [inst_7 : NormedSpace 𝕜 F]
[inst_8 : CompleteSpace F] [inst_9 : MeasurableSpace G] [inst_10 : NormedAddCommGroup G] [inst_11 : BorelSpace G]
[inst_12 : NormedSpace 𝕜 G] [inst_13 : NormedAddCommGroup P] [inst_14 : NormedSpace 𝕜 P]
{μ : MeasureTheory.Measure G} {n : ℕ∞} (L : E →L[𝕜] E' →L[𝕜] F) {s : Set P} {v : P → G},
ContDiffOn 𝕜 n v s →
∀ {f : G → E} {g : P → G → E'} {k : Set G},
IsOpen s →
IsCompact k →
(∀ (p : P) (x : G), p ∈ s → x ∉ k → g p x = 0) →
MeasureTheory.LocallyIntegrable f μ →
ContDiffOn 𝕜 n (↿g) (s ×ˢ Set.univ) → ContDiffOn 𝕜 n (fun x => convolution f (g x) L μ (v x)) s
The theorem `contDiffOn_convolution_right_with_param_comp` states that for certain types and conditions, the convolution `f * g` is continuously differentiable of any order `n` when the function `f` is locally integrable and the function `g` is continuously differentiable of any order `n` and has compact support. More specifically, this version of the theorem applies when `g` depends on an additional parameter in an open subset `s` of a parameter space `P`. The theorem further stipulates that the compact support `k` is independent of the parameter in `s`, and it provides for the convolution operation given in terms of composition with an additional continuously differentiable function. The theorem is parametrized by a continuous linear map `L: E →L[𝕜] E' →L[𝕜] F`, a measure `μ` on space `G`, a function `v: P → G` that is differentiable of order `n` on `s`, and functions `f: G → E` and `g: P → G → E'`. The theorem requires that the set `s` is open, the set `k` is compact, `g` is zero outside of `k` for any `p` in `s`, `f` is locally integrable, and `g` is differentiable of order `n` on `s ×ˢ Set.univ`. Under these conditions, the theorem guarantees that the convolution of `f` and `g` is differentiable of order `n` on `s`.
More concisely: For a locally integrable function `f` and a continuously differentiable function `g` with compact support that depends on a parameter `p` in an open subset `s` of a parameter space `P`, the convolution `(f * g)(p) = ∫g(p - x)f(x)dμ(x)` is differentiable of order `n` on `s`.
|
convolution_neg_of_neg_eq
theorem convolution_neg_of_neg_eq :
∀ {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} [inst : NormedAddCommGroup E]
[inst_1 : NormedAddCommGroup E'] [inst_2 : NormedAddCommGroup F] {f : G → E} {g : G → E'} {x : G}
[inst_3 : NontriviallyNormedField 𝕜] [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜 E']
[inst_6 : NormedSpace 𝕜 F] (L : E →L[𝕜] E' →L[𝕜] F) [inst_7 : MeasurableSpace G] {μ : MeasureTheory.Measure G}
[inst_8 : NormedSpace ℝ F] [inst_9 : AddCommGroup G] [inst_10 : μ.IsAddLeftInvariant] [inst_11 : μ.IsNegInvariant]
[inst_12 : MeasurableNeg G] [inst_13 : MeasurableAdd G],
(∀ᵐ (x : G) ∂μ, f (-x) = f x) →
(∀ᵐ (x : G) ∂μ, g (-x) = g x) → convolution f g L μ (-x) = convolution f g L μ x
This theorem states that the convolution of two even functions is also even. More specifically, for a nontrivially normed field 𝕜, normed add commutative groups E, E', and F, and functions f: G → E and g: G → E', if both f and g are even almost everywhere with respect to measure μ (i.e., f(-x) = f(x) and g(-x) = g(x) for almost all x in G), then their convolution with respect to L and μ is also even (i.e., convolution f g L μ (-x) = convolution f g L μ x). This holds under the conditions that G is a measurable and commutative add group, μ is left and negation invariant, and the normed spaces 𝕜 E, 𝕜 E', 𝕜 F, and ℝ F are properly defined.
More concisely: If two even, almost everywhere functions f and g with respect to a left and negation invariant measure μ on a commutative add group G belong to the convolution of normed spaces over the nontrivially normed field 𝕜, then their convolution is even.
|
continuousOn_convolution_right_with_param
theorem continuousOn_convolution_right_with_param :
∀ {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} {P : Type uP}
[inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup E'] [inst_2 : NormedAddCommGroup F] {f : G → E}
[inst_3 : NontriviallyNormedField 𝕜] [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜 E']
[inst_6 : NormedSpace 𝕜 F] (L : E →L[𝕜] E' →L[𝕜] F) [inst_7 : MeasurableSpace G] {μ : MeasureTheory.Measure G}
[inst_8 : NormedSpace ℝ F] [inst_9 : AddGroup G] [inst_10 : TopologicalSpace G] [inst_11 : TopologicalAddGroup G]
[inst_12 : BorelSpace G] [inst_13 : TopologicalSpace P] {g : P → G → E'} {s : Set P} {k : Set G},
IsCompact k →
(∀ (p : P) (x : G), p ∈ s → x ∉ k → g p x = 0) →
MeasureTheory.LocallyIntegrable f μ →
ContinuousOn (↿g) (s ×ˢ Set.univ) → ContinuousOn (fun q => convolution f (g q.1) L μ q.2) (s ×ˢ Set.univ)
This theorem states that for a given set of types and conditions, the convolution `f * g` is continuous if `f` is locally integrable, `g` is continuous and compactly supported. Here, `g` is a function that depends on an additional parameter in a subset `s` of a parameter space `P`. The convolution operation is defined with respect to a linear map `L` and a measure `μ`. The compact support `k` for `g` is independent of the parameter in `s`. For every parameter `p` in `s` and every element `x` not in `k`, `g` at `p` and `x` equals zero. The function `g` is continuous on the product set `s x Set.univ`. The result is that the function `q` mapping to the convolution of `f` and `g` at `q.1` with respect to `L` and `μ` at `q.2` is continuous on the product set `s x Set.univ`.
More concisely: Given locally integrable function `f`, continuous and compactly supported function `g` with compact support independent of an additional parameter `p` in a subset `s` of a parameter space `P`, the convolution `f * g` is a continuous function on the product set `s x Set.univ`.
|
BddAbove.continuous_convolution_right_of_integrable
theorem BddAbove.continuous_convolution_right_of_integrable :
∀ {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} [inst : NormedAddCommGroup E]
[inst_1 : NormedAddCommGroup E'] [inst_2 : NormedAddCommGroup F] {f : G → E} {g : G → E'}
[inst_3 : NontriviallyNormedField 𝕜] [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜 E']
[inst_6 : NormedSpace 𝕜 F] (L : E →L[𝕜] E' →L[𝕜] F) [inst_7 : MeasurableSpace G] {μ : MeasureTheory.Measure G}
[inst_8 : NormedSpace ℝ F] [inst_9 : AddGroup G] [inst_10 : TopologicalSpace G] [inst_11 : TopologicalAddGroup G]
[inst_12 : BorelSpace G] [inst_13 : FirstCountableTopology G] [inst_14 : SecondCountableTopologyEither G E'],
BddAbove (Set.range fun x => ‖g x‖) →
MeasureTheory.Integrable f μ → Continuous g → Continuous (convolution f g L μ)
This theorem states that the convolution of two functions is continuous under certain conditions. Specifically, given a field 𝕜, normed additive commutative groups E, E', F and function `f` from G to E and `g` from G to E', with G being a Borel space with first and second countable topology and simultaneous topological add group. If `g` is bounded above and continuous, and `f` is integrable with respect to a measure `μ`, then the convolution of `f` and `g` is continuous. The convolution is defined with respect to a continuous linear map `L` from E to the continuous linear maps from E' to F. This essentially means that if one function is integrable and the other is both bounded and continuous, their convolution will also be continuous.
More concisely: Given a field 𝕜, normed additive commutative groups E, E', F, Borel space G with first and second countable topology and simultaneous topological add group, bounded, continuous function g from G to E', integrable function f from G to E, and a continuous linear map L from E to the continuous linear maps from E' to F, the convolution (f * g) defined as (L ∘ f) ∘ g is a continuous function from G to F.
|
convolution_mul
theorem convolution_mul :
∀ {𝕜 : Type u𝕜} {G : Type uG} {x : G} [inst : NontriviallyNormedField 𝕜] [inst_1 : MeasurableSpace G]
{μ : MeasureTheory.Measure G} [inst_2 : Sub G] [inst_3 : NormedSpace ℝ 𝕜] {f g : G → 𝕜},
convolution f g (ContinuousLinearMap.mul 𝕜 𝕜) μ x = ∫ (t : G), f t * g (x - t) ∂μ
This theorem, `convolution_mul`, states that for any non-trivially normed field `𝕜`, any type `G` with a measurable space structure, a subtraction operation and associated measure `μ`, and any point `x` in `G`, the convolution of two functions `f` and `g` from `G` to `𝕜` with the bilinear operator defined as multiplication via the continuous linear map `ContinuousLinearMap.mul 𝕜 𝕜`, evaluated at `x`, is equal to the integral over `G` of the product of `f` at `t` and `g` at `x - t` with respect to the measure `μ`. In other words, it encodes the definition of convolution in the context of a non-unital normed algebra where the bilinear operation is multiplication.
More concisely: For any non-trivially normed field `𝕜`, measurable space `(G, Σ, μ)`, and functions `f` and `g` from `G` to `𝕜`, the convolution of `f` and `g` at `x` is equal to the integral of `f(t) * g(x - t)` with respect to `μ`.
|
contDiffOn_convolution_left_with_param
theorem contDiffOn_convolution_left_with_param :
∀ {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} {P : Type uP}
[inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup E'] [inst_2 : NormedAddCommGroup F] [inst_3 : RCLike 𝕜]
[inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜 E'] [inst_6 : NormedSpace ℝ F] [inst_7 : NormedSpace 𝕜 F]
[inst_8 : CompleteSpace F] [inst_9 : MeasurableSpace G] [inst_10 : NormedAddCommGroup G] [inst_11 : BorelSpace G]
[inst_12 : NormedSpace 𝕜 G] [inst_13 : NormedAddCommGroup P] [inst_14 : NormedSpace 𝕜 P]
{μ : MeasureTheory.Measure G} [inst_15 : μ.IsAddLeftInvariant] [inst_16 : μ.IsNegInvariant]
(L : E' →L[𝕜] E →L[𝕜] F) {f : G → E} {n : ℕ∞} {g : P → G → E'} {s : Set P} {k : Set G},
IsOpen s →
IsCompact k →
(∀ (p : P) (x : G), p ∈ s → x ∉ k → g p x = 0) →
MeasureTheory.LocallyIntegrable f μ →
ContDiffOn 𝕜 n (↿g) (s ×ˢ Set.univ) →
ContDiffOn 𝕜 n (fun q => convolution (g q.1) f L μ q.2) (s ×ˢ Set.univ)
This theorem states that, given a set of conditions, the convolution of two functions is continuously differentiable. More specifically, if you have a function 'f' that is locally integrable and a function 'g' that is continuously differentiable and has compact support, then their convolution 'g * f' is continuously differentiable. This version of the theorem adds a parameter space 'P' and an open subset 's' of 'P', where 'g' depends on an additional parameter in 's', however, the compact support 'k' of 'g' is not dependent on this parameter.
This theorem relies on several properties and conditions. Namely, the set 's' must be open, and 'k', the support of 'g', must be compact. Moreover, for any point 'p' in 's' and 'x' not in 'k', 'g' at 'p' and 'x' must equal zero. Additionally, 'f' must be locally integrable and 'g' must be continuously differentiable in the set 's' cross the universal set. If all these conditions are met, then the convolution of 'g' and 'f', in the sense of the operator 'L', is continuously differentiable in the set 's' cross the universal set.
More concisely: Given a locally integrable function $f$, a continuously differentiable function $g$ with compact support that does not depend on the additional parameter $p$ in the open set $s$, if for all $p \in s$ and $x \notin k$, $g(p,x) = 0$, then their convolution $g \ast f$ is continuously differentiable.
|
ConvolutionExistsAt.ofNorm'
theorem ConvolutionExistsAt.ofNorm' :
∀ {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} [inst : NormedAddCommGroup E]
[inst_1 : NormedAddCommGroup E'] [inst_2 : NormedAddCommGroup F] {f : G → E} {g : G → E'}
[inst_3 : NontriviallyNormedField 𝕜] [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜 E']
[inst_6 : NormedSpace 𝕜 F] (L : E →L[𝕜] E' →L[𝕜] F) [inst_7 : MeasurableSpace G] {μ : MeasureTheory.Measure G}
[inst_8 : AddGroup G] [inst_9 : MeasurableAdd G] [inst_10 : MeasurableNeg G] {x₀ : G},
ConvolutionExistsAt (fun x => ‖f x‖) (fun x => ‖g x‖) x₀ (ContinuousLinearMap.mul ℝ ℝ) μ →
MeasureTheory.AEStronglyMeasurable f μ →
MeasureTheory.AEStronglyMeasurable g (MeasureTheory.Measure.map (fun t => x₀ - t) μ) →
ConvolutionExistsAt f g x₀ L μ
The theorem `ConvolutionExistsAt.ofNorm'` states that for a given real number `𝕜`, types `G`, `E`, `E'`, `F`, and functions `f : G → E`, `g : G → E'`, if the convolution of the norms of `f` and `g` exists at a point `x₀`, then the convolution of `f` and `g` also exists at `x₀`, provided that `f` is almost everywhere strongly measurable with respect to a measure `μ` and `g` is almost everywhere strongly measurable with respect to the pushforward of `μ` by the function `t ↦ x₀ - t`. Here, `L` is a continuous bilinear map from `E` and `E'` to `F`. The convolution is taken with respect to the group operation in `G`, which is assumed to be a normed additive commutative group that is also measurable.
More concisely: If the convolution of the norms of almost everywhere strongly measurable functions `f : G → E` and `g : G → E'` with respect to a measure `μ` exists at a point `x₀`, then the convolution of `f` and `g` itself exists at `x₀` and is given by the continuous bilinear map `L` applied to the convolution of their norms.
|
dist_convolution_le
theorem dist_convolution_le :
∀ {G : Type uG} {E' : Type uE'} [inst : NormedAddCommGroup E'] {g : G → E'} [inst_1 : MeasurableSpace G]
{μ : MeasureTheory.Measure G} [inst_2 : SeminormedAddCommGroup G] [inst_3 : BorelSpace G]
[inst_4 : SecondCountableTopology G] [inst_5 : μ.IsAddLeftInvariant] [inst_6 : MeasureTheory.SigmaFinite μ]
[inst_7 : NormedSpace ℝ E'] [inst_8 : CompleteSpace E'] {f : G → ℝ} {x₀ : G} {R ε : ℝ} {z₀ : E'},
0 ≤ ε →
Function.support f ⊆ Metric.ball 0 R →
(∀ (x : G), 0 ≤ f x) →
∫ (x : G), f x ∂μ = 1 →
MeasureTheory.AEStronglyMeasurable g μ →
(∀ x ∈ Metric.ball x₀ R, dist (g x) z₀ ≤ ε) →
dist (convolution f g (ContinuousLinearMap.lsmul ℝ ℝ) μ x₀) z₀ ≤ ε
The theorem `dist_convolution_le` states that for any normed addition commutative group `G`, any type `E'` with a normed addition commutative group structure, a function `g` from `G` to `E'`, a measure `μ` on `G`, a function `f` from `G` to the real numbers `ℝ`, a point `x₀` in `G`, two real numbers `R` and `ε`, and a point `z₀` in `E'` such that `ε` is nonnegative, the support of `f` is contained within a ball of radius `R` around 0, `f` is nonnegative, the integral of `f` with respect to `μ` is 1, `g` is almost everywhere equal to the limit of a sequence of simple functions with respect to measure `μ` and for each point `x` in the ball of radius `R` around `x₀`, the distance from `g(x)` to `z₀` is less than or equal to `ε`, we can conclude that the distance between the convolution of `f` and `g` using the linear map `(ContinuousLinearMap.lsmul ℝ ℝ)` at `x₀` and `z₀` is less than or equal to `ε`.
In simpler terms, the theorem allows us to approximate a convolution of two functions (`f` and `g`) around a certain point (`x₀`), if `f` is nonnegative and is mostly non-zero within a certain region (a ball of radius `R`), and `g` behaves similarly to a simple function almost everywhere, and is close to a particular point (`z₀`) within the same region.
More concisely: Given a normed additive commutative group `G`, a type `E'` with a normed additive commutative group structure, a measure `μ` on `G`, a nonnegative, integrable function `f : G → ℝ` with support in a ball of radius `R` around 0, a function `g : G → E'` that converges almost everywhere to a simple function with respect to `μ`, and a point `x₀` in `G`, if the distance from `g(x)` to a fixed point `z₀` in `E'` is less than or equal to `ε` for all `x` in the ball of radius `R` around `x₀`, then the distance between the convolution of `f` and `g` at `x₀` is less than or equal to `ε`.
|
contDiffOn_convolution_right_with_param_aux
theorem contDiffOn_convolution_right_with_param_aux :
∀ {𝕜 : Type u𝕜} {E : Type uE} [inst : NormedAddCommGroup E] [inst_1 : RCLike 𝕜] [inst_2 : NormedSpace 𝕜 E]
{G E' F P : Type uP} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedAddCommGroup F] [inst_5 : NormedSpace 𝕜 E']
[inst_6 : NormedSpace ℝ F] [inst_7 : NormedSpace 𝕜 F] [inst_8 : CompleteSpace F] [inst_9 : MeasurableSpace G]
{μ : MeasureTheory.Measure G} [inst_10 : NormedAddCommGroup G] [inst_11 : BorelSpace G]
[inst_12 : NormedSpace 𝕜 G] [inst_13 : NormedAddCommGroup P] [inst_14 : NormedSpace 𝕜 P] {f : G → E} {n : ℕ∞}
(L : E →L[𝕜] E' →L[𝕜] F) {g : P → G → E'} {s : Set P} {k : Set G},
IsOpen s →
IsCompact k →
(∀ (p : P) (x : G), p ∈ s → x ∉ k → g p x = 0) →
MeasureTheory.LocallyIntegrable f μ →
ContDiffOn 𝕜 n (↿g) (s ×ˢ Set.univ) →
ContDiffOn 𝕜 n (fun q => convolution f (g q.1) L μ q.2) (s ×ˢ Set.univ)
This theorem states that the convolution `f * g` is continuously differentiable of any order `n` when `f` is a function that is locally integrable and `g` is a function that is continuously differentiable of any order `n` and has compact support. The continuous differentiability of `f * g` is demonstrated where `g` depends on an additional parameter defined in an open subset `s` of a parameter space `P`. The theorem also specifies that the compact support `k` of `g` is independent of the parameter in `s`. Notably, for this theorem, all the types involved belong to the same universe. This is significant as it allows induction to be applied in the proof. However, if this restriction is not desirable, one can use `contDiffOn_convolution_right_with_param`, which removes this limitation.
More concisely: The convolution of a locally integrable function `f` and a continuously differentiable function `g` of any order with compact support, independent of a parameter in an open subset of a parameter space, is continuously differentiable of any order.
|
continuousOn_convolution_right_with_param_comp
theorem continuousOn_convolution_right_with_param_comp :
∀ {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} {P : Type uP}
[inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup E'] [inst_2 : NormedAddCommGroup F] {f : G → E}
[inst_3 : NontriviallyNormedField 𝕜] [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜 E']
[inst_6 : NormedSpace 𝕜 F] (L : E →L[𝕜] E' →L[𝕜] F) [inst_7 : MeasurableSpace G] {μ : MeasureTheory.Measure G}
[inst_8 : NormedSpace ℝ F] [inst_9 : AddGroup G] [inst_10 : TopologicalSpace G] [inst_11 : TopologicalAddGroup G]
[inst_12 : BorelSpace G] [inst_13 : TopologicalSpace P] {s : Set P} {v : P → G},
ContinuousOn v s →
∀ {g : P → G → E'} {k : Set G},
IsCompact k →
(∀ (p : P) (x : G), p ∈ s → x ∉ k → g p x = 0) →
MeasureTheory.LocallyIntegrable f μ →
ContinuousOn (↿g) (s ×ˢ Set.univ) → ContinuousOn (fun x => convolution f (g x) L μ (v x)) s
This theorem states that, for a certain configuration of types and conditions, if we have a function `v` that is continuous on a set `s`, a function `g` that equals zero outside of a compact set `k`, and a function `f` that is locally integrable, then the convolution of `f` and `g` is a continuous function on the set `s`. Here, the convolution is given in terms of compositions with an additional continuous map. The function `g` is allowed to depend on an additional parameter in an open subset `s` of a parameter space `P`, and the compact support `k` is independent of the parameter in `s`. This is a generalization of a convolution theorem from harmonic analysis.
More concisely: If `v` is a continuous function on a set `s`, `g` is a continuous function on `s` with compact support `k` that equals zero outside a compact set, and `f` is a locally integrable function, then the convolution of `f` and `g` given by composition with an additional continuous map is a continuous function on `s`.
|
convolution_mul_swap
theorem convolution_mul_swap :
∀ {𝕜 : Type u𝕜} {G : Type uG} {x : G} [inst : NontriviallyNormedField 𝕜] [inst_1 : MeasurableSpace G]
{μ : MeasureTheory.Measure G} [inst_2 : AddCommGroup G] [inst_3 : μ.IsAddLeftInvariant]
[inst_4 : μ.IsNegInvariant] [inst_5 : MeasurableNeg G] [inst_6 : MeasurableAdd G] [inst_7 : NormedSpace ℝ 𝕜]
{f g : G → 𝕜}, convolution f g (ContinuousLinearMap.mul 𝕜 𝕜) μ x = ∫ (t : G), f (x - t) * g t ∂μ
This theorem, `convolution_mul_swap`, states that for any non-trivially normed field `𝕜` and any type `G`, along with a variable `x` of type `G`, given certain conditions like `G` having a measurable space structure, the measure `μ` is add left invariant and negative invariant, `G` being a measurable negation and a measurable addition, and `𝕜` being a normed space over the real numbers `ℝ`, the convolution of two functions `f` and `g` from `G` to `𝕜` using the multiplication as the bilinear operator (defined as a continuous linear map) and the measure `μ` at the point `x` is equal to the Lebesgue integral over the measure space `G` of the product of the function `f` at the point `x - t` and the function `g` at the point `t`. This notion of convolution and the theorem are important in the field of harmonic analysis, where they help to study functions, measures, and operators.
More concisely: For any non-trivially normed field 𝕜, measurable space (G, Σ, μ), measurable functions f and g from G to 𝕜, and point x in G, the convolution of f and g at x using multiplication as the bilinear operator equals the Lebesgue integral of f(x - t) \* g(t) dμ(t).
|
HasCompactSupport.continuous_convolution_right
theorem HasCompactSupport.continuous_convolution_right :
∀ {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} [inst : NormedAddCommGroup E]
[inst_1 : NormedAddCommGroup E'] [inst_2 : NormedAddCommGroup F] {f : G → E} {g : G → E'}
[inst_3 : NontriviallyNormedField 𝕜] [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜 E']
[inst_6 : NormedSpace 𝕜 F] (L : E →L[𝕜] E' →L[𝕜] F) [inst_7 : MeasurableSpace G] {μ : MeasureTheory.Measure G}
[inst_8 : NormedSpace ℝ F] [inst_9 : AddGroup G] [inst_10 : TopologicalSpace G] [inst_11 : TopologicalAddGroup G]
[inst_12 : BorelSpace G],
HasCompactSupport g → MeasureTheory.LocallyIntegrable f μ → Continuous g → Continuous (convolution f g L μ)
The theorem `HasCompactSupport.continuous_convolution_right` states that the convolution operation is continuous if one function is locally integrable and the other function has compact support and is also continuous. Here, the convolution operation is performed on two functions, `f` and `g`, where `f` is a function from a type `G` to a normed add commutative group `E` and `g` is a function from the same type `G` to another normed add commutative group `E'`. The result of this convolution operation is a function from `G` to a normed add commutative group `F`. The theorem asserts that if function `f` is locally integrable, and function `g` is continuous and has a compact support, then the convolution of `f` and `g` is a continuous function.
More concisely: If `f` is a locally integrable function and `g` is a continuous function with compact support, then the convolution of `f` and `g` is a continuous function.
|
convolution_tendsto_right
theorem convolution_tendsto_right :
∀ {G : Type uG} {E' : Type uE'} [inst : NormedAddCommGroup E'] [inst_1 : MeasurableSpace G]
{μ : MeasureTheory.Measure G} [inst_2 : SeminormedAddCommGroup G] [inst_3 : BorelSpace G]
[inst_4 : SecondCountableTopology G] [inst_5 : μ.IsAddLeftInvariant] [inst_6 : MeasureTheory.SigmaFinite μ]
[inst_7 : NormedSpace ℝ E'] [inst_8 : CompleteSpace E'] {ι : Type u_1} {g : ι → G → E'} {l : Filter ι} {x₀ : G}
{z₀ : E'} {φ : ι → G → ℝ} {k : ι → G},
(∀ᶠ (i : ι) in l, ∀ (x : G), 0 ≤ φ i x) →
(∀ᶠ (i : ι) in l, ∫ (x : G), φ i x ∂μ = 1) →
Filter.Tendsto (fun n => Function.support (φ n)) l (nhds 0).smallSets →
(∀ᶠ (i : ι) in l, MeasureTheory.AEStronglyMeasurable (g i) μ) →
Filter.Tendsto (Function.uncurry g) (l ×ˢ nhds x₀) (nhds z₀) →
Filter.Tendsto k l (nhds x₀) →
Filter.Tendsto (fun i => convolution (φ i) (g i) (ContinuousLinearMap.lsmul ℝ ℝ) μ (k i)) l
(nhds z₀)
The theorem `convolution_tendsto_right` states that for a sequence of functions `φ i`, which are nonnegative and whose integrals converge to `1` with respect to a certain filter `l`, and another function `g i`, which is almost everywhere strongly measurable with respect to the measure `μ`, the convolution of `φ i` and `g i` tends to a limit `z₀`. This holds under certain conditions:
- The support of `φ` tends to small neighborhoods around `(0 : G)` as `i` tends to `l`. In other words, the set of points where `φ i` is nonzero becomes increasingly concentrated around 0 as `i` increases.
- The function `g i x` tends to `z₀` as the pair `(i, x)` tends to the product of the filter `l` and the neighborhood filter at `x₀`.
- A sequence `k i` tends to `x₀` as `i` tends to `l`.
The convolution here is represented by `convolution (φ i) (g i) (ContinuousLinearMap.lsmul ℝ ℝ) μ (k i)`. This theorem is useful in the analysis of functions and their limits, particularly in the context of measure theory and functional analysis.
More concisely: Given a sequence of nonnegative functions `φ i` with integrals converging to 1 with respect to filter `l`, and another almost everywhere strongly measurable function `g i` such that the support of `φ i` concentrates around 0, `g i x` converges to a limit `z₀` as `(i, x)` approaches the product of `l` and the neighborhood filter at some fixed point `x₀`, and `k i` converges to `x₀` as `i` approaches `l`, then the convolution of `φ i` and `g i` with respect to the Lebesgue measure and `k i` tends to the limit `z₀`.
|
convolution_lsmul_swap
theorem convolution_lsmul_swap :
∀ {𝕜 : Type u𝕜} {G : Type uG} {F : Type uF} [inst : NormedAddCommGroup F] {x : G}
[inst_1 : NontriviallyNormedField 𝕜] [inst_2 : NormedSpace 𝕜 F] [inst_3 : MeasurableSpace G]
{μ : MeasureTheory.Measure G} [inst_4 : NormedSpace ℝ F] [inst_5 : AddCommGroup G] [inst_6 : μ.IsAddLeftInvariant]
[inst_7 : μ.IsNegInvariant] [inst_8 : MeasurableNeg G] [inst_9 : MeasurableAdd G] {f : G → 𝕜} {g : G → F},
convolution f g (ContinuousLinearMap.lsmul 𝕜 𝕜) μ x = ∫ (t : G), f (x - t) • g t ∂μ
This theorem, `convolution_lsmul_swap`, states that in a given normed additive commutative group `F` and a nontrivially normed field `𝕜`, for every element `x` of some type `G`, and under certain conditions such as `G` being a measurable space, `μ` being an add-left-invariant and neg-invariant measure on `G`, and `G` supporting negation and addition operations, the convolution of functions `f : G → 𝕜` and `g : G → F` using the continuous linear scalar multiplication operator is equal to the integral over `G` of the expression `f (x - t) • g t`, where `t` is the variable of integration and `•` represents scalar multiplication.
More concisely: For measurable functions `f : G -> ℝ` and `g : G -> F` on a measurable space `(G, μ)` with a nontrivially normed field `𝕜`, the convolution of `f` and `g` using the continuous linear scalar multiplication operator equals the integral of `f (x - t) * g t` over `G`.
|
contDiffOn_convolution_left_with_param_comp
theorem contDiffOn_convolution_left_with_param_comp :
∀ {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} {P : Type uP}
[inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup E'] [inst_2 : NormedAddCommGroup F] [inst_3 : RCLike 𝕜]
[inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜 E'] [inst_6 : NormedSpace ℝ F] [inst_7 : NormedSpace 𝕜 F]
[inst_8 : CompleteSpace F] [inst_9 : MeasurableSpace G] [inst_10 : NormedAddCommGroup G] [inst_11 : BorelSpace G]
[inst_12 : NormedSpace 𝕜 G] [inst_13 : NormedAddCommGroup P] [inst_14 : NormedSpace 𝕜 P]
{μ : MeasureTheory.Measure G} [inst_15 : μ.IsAddLeftInvariant] [inst_16 : μ.IsNegInvariant]
(L : E' →L[𝕜] E →L[𝕜] F) {s : Set P} {n : ℕ∞} {v : P → G},
ContDiffOn 𝕜 n v s →
∀ {f : G → E} {g : P → G → E'} {k : Set G},
IsOpen s →
IsCompact k →
(∀ (p : P) (x : G), p ∈ s → x ∉ k → g p x = 0) →
MeasureTheory.LocallyIntegrable f μ →
ContDiffOn 𝕜 n (↿g) (s ×ˢ Set.univ) → ContDiffOn 𝕜 n (fun x => convolution (g x) f L μ (v x)) s
This theorem states that the convolution of two functions `g` and `f`, denoted as `g * f`, is `C^n` smooth (i.e., `n` times continuously differentiable) under certain conditions. Specifically, `f` must be locally integrable and `g` must be `C^n` smooth and have compact support. In this version, `g` depends on an additional parameter from an open subset `s` of a parameter space `P`, and the compact support `k` is independent of the parameter in `s`. The theorem is given in terms of composition with additional smooth functions. It ensures that if `v` is `n` times continuously differentiable on `s`, `f` is locally integrable, `g` is `n` times continuously differentiable on the product space `s ×ˢ Set.univ`(i.e., the product of `s` and the universal set), `s` is open, `k` is compact, and `g` is zero outside `k` for all points in `s`, then the function `x ↦ (g x) * f` (where * denotes convolution and the function is parameterized by `v` and a linear map `L`) is also `n` times continuously differentiable on `s`.
More concisely: Given locally integrable function `f`, `C^n` smooth function `g` with compact support `k` independent of a parameter `s` from an open subset, if `g` is zero outside `k` for all points in `s`, then the convolution `(g x) * f` is `n` times continuously differentiable on `s`.
|
convolution_flip
theorem convolution_flip :
∀ {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} [inst : NormedAddCommGroup E]
[inst_1 : NormedAddCommGroup E'] [inst_2 : NormedAddCommGroup F] {f : G → E} {g : G → E'}
[inst_3 : NontriviallyNormedField 𝕜] [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜 E']
[inst_6 : NormedSpace 𝕜 F] (L : E →L[𝕜] E' →L[𝕜] F) [inst_7 : MeasurableSpace G] {μ : MeasureTheory.Measure G}
[inst_8 : NormedSpace ℝ F] [inst_9 : AddCommGroup G] [inst_10 : μ.IsAddLeftInvariant] [inst_11 : μ.IsNegInvariant]
[inst_12 : MeasurableNeg G] [inst_13 : MeasurableAdd G], convolution g f L.flip μ = convolution f g L μ
This theorem, named `convolution_flip`, states the commutativity of convolution. In the setting where `𝕜` is a nontrivially normed field, `E`, `E'`, and `F` are normed add commutative groups which are normed spaces over `𝕜`, `G` is an additive group with a measure `μ` that is both add-left-invariant and neg-invariant, and `f` and `g` are measurable functions from `G` to `E` and `E'` respectively, the convolution of `g` and `f` under the flipped linear map `L.flip` is equal to the convolution of `f` and `g` under the linear map `L`. This essentially means that the order of `f` and `g` in the convolution operation can be reversed if the operator `L` is also flipped.
More concisely: If `𝕜` is a nontrivially normed field, `G` is a measure space with an add-left-invariant and neg-invariant measure `μ`, and `f: G → E` and `g: G → E'` are measurable functions, then `(f ⊛ g) (L.flip) = (g ⊛ f) L`, where `⊛` denotes convolution.
|
ConvolutionExistsAt.ofNorm
theorem ConvolutionExistsAt.ofNorm :
∀ {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} [inst : NormedAddCommGroup E]
[inst_1 : NormedAddCommGroup E'] [inst_2 : NormedAddCommGroup F] {f : G → E} {g : G → E'}
[inst_3 : NontriviallyNormedField 𝕜] [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜 E']
[inst_6 : NormedSpace 𝕜 F] (L : E →L[𝕜] E' →L[𝕜] F) [inst_7 : MeasurableSpace G] {μ : MeasureTheory.Measure G}
[inst_8 : AddGroup G] [inst_9 : MeasurableAdd₂ G] [inst_10 : MeasurableNeg G]
[inst_11 : MeasureTheory.SigmaFinite μ] [inst_12 : μ.IsAddRightInvariant] {x₀ : G},
ConvolutionExistsAt (fun x => ‖f x‖) (fun x => ‖g x‖) x₀ (ContinuousLinearMap.mul ℝ ℝ) μ →
MeasureTheory.AEStronglyMeasurable f μ →
MeasureTheory.AEStronglyMeasurable g μ → ConvolutionExistsAt f g x₀ L μ
This theorem states that in a context with various normed spaces, measures, and group structures, if the convolution at a point `x₀` of the norms of two functions `f` and `g` exists with respect to a measure `μ` and the multiplication is carried out in the real numbers, and if both `f` and `g` are almost everywhere strongly measurable with respect to the measure `μ`, then the convolution of the functions `f` and `g` itself at the point `x₀` exists. Here, the term "almost everywhere strongly measurable" means that the function is almost everywhere equal to the limit of a sequence of simple functions.
More concisely: If `f` and `g` are almost everywhere strongly measurable functions on a measure space with respect to a measure `μ`, and their convolutions with real-number valued functions exist at a point `x₀`, then the convolution of `f` and `g` also exists at `x₀`.
|