ContDiffBump.convolution_tendsto_right
theorem ContDiffBump.convolution_tendsto_right :
∀ {G : Type uG} {E' : Type uE'} [inst : NormedAddCommGroup E'] [inst_1 : MeasurableSpace G]
{μ : MeasureTheory.Measure G} [inst_2 : NormedSpace ℝ E'] [inst_3 : NormedAddCommGroup G]
[inst_4 : NormedSpace ℝ G] [inst_5 : HasContDiffBump G] [inst_6 : CompleteSpace E'] [inst_7 : BorelSpace G]
[inst_8 : MeasureTheory.IsLocallyFiniteMeasure μ] [inst_9 : μ.IsOpenPosMeasure] [inst_10 : FiniteDimensional ℝ G]
[inst_11 : μ.IsAddLeftInvariant] {ι : Type u_1} {φ : ι → ContDiffBump 0} {g : ι → G → E'} {k : ι → G} {x₀ : G}
{z₀ : E'} {l : Filter ι},
Filter.Tendsto (fun i => (φ i).rOut) l (nhds 0) →
(∀ᶠ (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).normed μ) (g i) (ContinuousLinearMap.lsmul ℝ ℝ) μ (k i)) l
(nhds z₀)
The theorem `ContDiffBump.convolution_tendsto_right` states that for a given set of conditions, the convolution of a sequence of normed bump functions `φ i`, and a sequence of functions `g i` that are almost everywhere strongly measurable with respect to a measure `μ`, evaluated at `k i`, tends to a limit `z₀` as `i` approaches a filter `l`. The conditions that must be satisfied are: the radial outer function `(φ i).rOut` tends to `0` as `i` approaches `l`; the function `g i` is `μ`-almost everywhere strongly measurable; the function `g i x` tends to `z₀` as the pair `(i, x)` tends to the product filter of `l` and the neighborhood filter at `x₀`; and the sequence `k i` tends to `x₀`. The theorem applies in the context of a normed additive commutative group `E'`, a measurable space `G` with a measure `μ`, a normed additive commutative group `G`, and a normed real vector space `G` which is finite-dimensional. The measure `μ` is assumed to be locally finite, is an open positive measure, is add-left-invariant, and the space `E'` is complete.
More concisely: Given a sequence of normed bump functions `φ i` with radial outer functions tending to 0, a sequence of almost everywhere strongly measurable functions `g i` with limits `z₀` at `x₀`, and a filter `l`, if `k i` tends to `x₀` and `E'` is a complete normed additive commutative group, `G` a finite-dimensional normed additive commutative group, `G` a measurable space with a locally finite, open positive, add-left-invariant measure `μ`, then the convolution of `φ i` with `g i` at `k i` tends to `z₀` as `i` approaches `l`.
|
ContDiffBump.ae_convolution_tendsto_right_of_locallyIntegrable
theorem ContDiffBump.ae_convolution_tendsto_right_of_locallyIntegrable :
∀ {G : Type uG} {E' : Type uE'} [inst : NormedAddCommGroup E'] {g : G → E'} [inst_1 : MeasurableSpace G]
{μ : MeasureTheory.Measure G} [inst_2 : NormedSpace ℝ E'] [inst_3 : NormedAddCommGroup G]
[inst_4 : NormedSpace ℝ G] [inst_5 : HasContDiffBump G] [inst_6 : CompleteSpace E'] [inst_7 : BorelSpace G]
[inst_8 : MeasureTheory.IsLocallyFiniteMeasure μ] [inst_9 : μ.IsOpenPosMeasure] [inst_10 : FiniteDimensional ℝ G]
[inst_11 : μ.IsAddLeftInvariant] {ι : Type u_1} {φ : ι → ContDiffBump 0} {l : Filter ι} {K : ℝ},
Filter.Tendsto (fun i => (φ i).rOut) l (nhds 0) →
(∀ᶠ (i : ι) in l, (φ i).rOut ≤ K * (φ i).rIn) →
MeasureTheory.LocallyIntegrable g μ →
∀ᵐ (x₀ : G) ∂μ,
Filter.Tendsto (fun i => convolution ((φ i).normed μ) g (ContinuousLinearMap.lsmul ℝ ℝ) μ x₀) l
(nhds (g x₀))
This theorem states that if a function `g` is locally integrable, then the convolution of `g` with a sequence of bump functions `φ i` converges almost everywhere to `g`. This holds if the support of `φ i` tends to `0` and the ratio between the inner and outer radii of `φ i` remains bounded. Here, a function is locally integrable if it is integrable on a neighborhood of every point. A bump function is a smooth function that is zero outside of a given set and equals one at a given point within that set. The convolution operation combines two functions to produce a third function, expressing how the shape of one is modified by the other.
More concisely: If a locally integrable function `g` and a sequence of bump functions `φ i` with bounded inner-to-outer radius ratio and shrinking support converge pointwise to `g`, then their convolutions converge almost everywhere to `g`.
|
ContDiffBump.normed_convolution_eq_right
theorem ContDiffBump.normed_convolution_eq_right :
∀ {G : Type uG} {E' : Type uE'} [inst : NormedAddCommGroup E'] {g : G → E'} [inst_1 : MeasurableSpace G]
{μ : MeasureTheory.Measure G} [inst_2 : NormedSpace ℝ E'] [inst_3 : NormedAddCommGroup G]
[inst_4 : NormedSpace ℝ G] [inst_5 : HasContDiffBump G] [inst_6 : CompleteSpace E'] {φ : ContDiffBump 0}
[inst_7 : BorelSpace G] [inst_8 : MeasureTheory.IsLocallyFiniteMeasure μ] [inst_9 : μ.IsOpenPosMeasure]
[inst_10 : FiniteDimensional ℝ G] {x₀ : G},
(∀ x ∈ Metric.ball x₀ φ.rOut, g x = g x₀) →
convolution (φ.normed μ) g (ContinuousLinearMap.lsmul ℝ ℝ) μ x₀ = g x₀
The theorem `ContDiffBump.normed_convolution_eq_right` states that for a normed bump function `φ`, if a function `g` (mapping from type `G` to `E'`) is constant on the metric ball (set of points `y` with distance from `y` to `x₀` less than `φ.rOut`), then the convolution of `φ.normed μ` and `g` evaluated at `x₀` is equal to `g x₀`. This theorem holds under several conditions: `G` is a finite-dimensional real vector space, `E'` is a complete normed space over ℝ, `g` is a measurable function, `μ` is a locally finite measure that is positive on open sets, and `φ` is a continuously differentiable bump function.
More concisely: For a continuously differentiable bump function φ with finite support in a finite-dimensional real vector space, if a measurable function g is constant on the metric ball determined by φ, then the convolution of μ, the measure integral of φ, and g evaluates to g(x₀), where x₀ is any point in the domain of g.
|
ContDiffBump.convolution_tendsto_right_of_continuous
theorem ContDiffBump.convolution_tendsto_right_of_continuous :
∀ {G : Type uG} {E' : Type uE'} [inst : NormedAddCommGroup E'] {g : G → E'} [inst_1 : MeasurableSpace G]
{μ : MeasureTheory.Measure G} [inst_2 : NormedSpace ℝ E'] [inst_3 : NormedAddCommGroup G]
[inst_4 : NormedSpace ℝ G] [inst_5 : HasContDiffBump G] [inst_6 : CompleteSpace E'] [inst_7 : BorelSpace G]
[inst_8 : MeasureTheory.IsLocallyFiniteMeasure μ] [inst_9 : μ.IsOpenPosMeasure] [inst_10 : FiniteDimensional ℝ G]
[inst_11 : μ.IsAddLeftInvariant] {ι : Type u_1} {φ : ι → ContDiffBump 0} {l : Filter ι},
Filter.Tendsto (fun i => (φ i).rOut) l (nhds 0) →
Continuous g →
∀ (x₀ : G),
Filter.Tendsto (fun i => convolution ((φ i).normed μ) g (ContinuousLinearMap.lsmul ℝ ℝ) μ x₀) l
(nhds (g x₀))
This theorem, `ContDiffBump.convolution_tendsto_right_of_continuous`, states that for a measurable space `G` with a measure `μ`, a function `g` mapping elements of `G` to a normed commutative addition group `E'`, if `g` is continuous and `l` is a filter, then for any point `x₀` in `G`, if the limit of the radius of `φ i` tends to 0 as `i` approaches `l`, the convolution of the normalized `φ i` and `g` under the linear scalar multiplication tends to `g(x₀)` as `i` approaches `l`. Here, `φ` is a function mapping elements of some set `ι` to a continuously differentiable bump function at `0`. This theorem holds when `G` is a finite-dimensional vector space over the real numbers, `μ` is a locally finite measure that is additively left invariant, `E'` is a complete normed space, and `G` is both a normed addition group and a normed space.
More concisely: Given a measurable space (G, μ) with a locally finite, additively invariant, and completable measure, a continuously differentiable bump function sequence φ i at 0 indexed by ι, a filter l, and a continuous function g from G to a normed commutative group E', the convolution of the normalized φ i and g tends to g(x₀) as the radius of φ i approaches 0 for each i in l.
|
ContDiffBump.dist_normed_convolution_le
theorem ContDiffBump.dist_normed_convolution_le :
∀ {G : Type uG} {E' : Type uE'} [inst : NormedAddCommGroup E'] {g : G → E'} [inst_1 : MeasurableSpace G]
{μ : MeasureTheory.Measure G} [inst_2 : NormedSpace ℝ E'] [inst_3 : NormedAddCommGroup G]
[inst_4 : NormedSpace ℝ G] [inst_5 : HasContDiffBump G] [inst_6 : CompleteSpace E'] {φ : ContDiffBump 0}
[inst_7 : BorelSpace G] [inst_8 : MeasureTheory.IsLocallyFiniteMeasure μ] [inst_9 : μ.IsOpenPosMeasure]
[inst_10 : FiniteDimensional ℝ G] [inst_11 : μ.IsAddLeftInvariant] {x₀ : G} {ε : ℝ},
MeasureTheory.AEStronglyMeasurable g μ →
(∀ x ∈ Metric.ball x₀ φ.rOut, dist (g x) (g x₀) ≤ ε) →
dist (convolution (φ.normed μ) g (ContinuousLinearMap.lsmul ℝ ℝ) μ x₀) (g x₀) ≤ ε
This theorem states that if `φ` is a normed bump function, we can approximate the value of the convolution of `φ` and another function `g` evaluated at a point `x₀`. The approximation holds when `g` is almost everywhere strongly measurable with respect to a measure `μ`, and stays close to `g(x₀)` inside a ball of radius `φ.rOut` centered at `x₀`. More specifically, if for every point `x` in the ball, the distance between `g(x)` and `g(x₀)` is less than or equal to some small positive number `ε`, then the distance between the value of the convolution at `x₀` and `g(x₀)` is also less than or equal to `ε`. This theorem relies on several other assumptions, such as `G` being a finite-dimensional real vector space and `μ` being a locally finite, open, positive, and left invariant measure.
More concisely: If `φ` is a normed bump function, `g` is almost everywhere strongly measurable and stays close to a fixed value `g(x₀)` inside a ball of radius `φ.rOut` centered at `x₀` with respect to a locally finite, open, positive, and left invariant measure `μ` on a finite-dimensional real vector space `G`, then the convolution of `φ` and `g` approaches `g(x₀)` as `φ` narrows, i.e., the distance between their values decreases, provided the difference between `g(x)` and `g(x₀)` is less than `ε` for all `x` in the ball.
|
ContDiffBump.convolution_eq_right
theorem ContDiffBump.convolution_eq_right :
∀ {G : Type uG} {E' : Type uE'} [inst : NormedAddCommGroup E'] {g : G → E'} [inst_1 : MeasurableSpace G]
{μ : MeasureTheory.Measure G} [inst_2 : NormedSpace ℝ E'] [inst_3 : NormedAddCommGroup G]
[inst_4 : NormedSpace ℝ G] [inst_5 : HasContDiffBump G] [inst_6 : CompleteSpace E'] {φ : ContDiffBump 0} {x₀ : G},
(∀ x ∈ Metric.ball x₀ φ.rOut, g x = g x₀) →
convolution (↑φ) g (ContinuousLinearMap.lsmul ℝ ℝ) μ x₀ = MeasureTheory.integral μ ↑φ • g x₀
This theorem, `ContDiffBump.convolution_eq_right`, states that given a type `G` and a type `E'` which are both normed addition commutative groups and normed spaces over real numbers, along with a measurable space structure on `G`, a measure theory measure `μ` on `G`, a bump function `φ` centered at `0`, and a point `x₀` in `G`, if a function `g` mapping from `G` to `E'` is constant on the metric ball centered at `x₀` with radius `φ.rOut`, then the convolution of `φ` and `g` at `x₀` (using the continuous linear map for scalar multiplication in real numbers) equals to the Bochner integral of `φ` times the constant function value `g x₀`. The convolution is a mathematical operation used in signal processing, and here it relates the convolution operation to the integral when the function `g` is constant on a local region.
More concisely: If a measurable function `g` is constant on the ball around `x₀` in a normed group `G` with respect to a bump function `φ` centered at `0`, then the convolution of `φ` and `g` at `x₀` equals the product of the Bochner integral of `φ` and the constant value `g(x₀)`.
|