tendsto_integral_exp_inner_smul_cocompact_of_continuous_compact_support
theorem tendsto_integral_exp_inner_smul_cocompact_of_continuous_compact_support :
∀ {E : Type u_1} {V : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : V → E}
[inst_2 : NormedAddCommGroup V] [inst_3 : MeasurableSpace V] [inst_4 : BorelSpace V]
[inst_5 : InnerProductSpace ℝ V] [inst_6 : FiniteDimensional ℝ V],
Continuous f →
HasCompactSupport f →
Filter.Tendsto (fun w => ∫ (v : V), Real.fourierChar (-⟪v, w⟫_ℝ) • f v) (Filter.cocompact V) (nhds 0)
This Lean theorem is the Riemann-Lebesgue Lemma for continuous and compactly-supported functions. It states that, given a function `f` from a finite-dimensional real inner product space `V` to a normed complex vector space `E` that is continuous and has compact support, the integral of `f` weighted by the exponential of the inner product with a variable `w` tends to zero when `w` tends to infinity. In more formal mathematical terms, for every `w` in `V`, we consider the function `v ↦ exp(-2π⟪w, v⟫) * f(v)`, where `⟪w, v⟫` denotes the inner product of `w` and `v` in `V`, and we integrate this function over `V`. As `w` varies and tends to infinity in the complement of compact sets (the cocompact filter), this integral tends to zero. This result is a stepping stone towards a more general theorem where the function `f` doesn't need to be continuous nor to have compact support.
More concisely: Given a continuous, compactly-supported function `f` from a finite-dimensional real inner product space `V` to a normed complex vector space `E`, the integral of `exp(-2π〈w, v〉) * f(v) dv` over `V` tends to zero as `w` tends to infinity in the complement of compact sets in `V`.
|
tendsto_integral_exp_smul_cocompact
theorem tendsto_integral_exp_smul_cocompact :
∀ {E : Type u_1} {V : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] (f : V → E)
[inst_2 : AddCommGroup V] [inst_3 : TopologicalSpace V] [inst_4 : TopologicalAddGroup V] [inst_5 : T2Space V]
[inst_6 : MeasurableSpace V] [inst_7 : BorelSpace V] [inst_8 : Module ℝ V] [inst_9 : ContinuousSMul ℝ V]
[inst_10 : FiniteDimensional ℝ V] (μ : MeasureTheory.Measure V) [inst_11 : μ.IsAddHaarMeasure],
Filter.Tendsto (fun w => ∫ (v : V), Real.fourierChar (-w v) • f v ∂μ) (Filter.cocompact (V →L[ℝ] ℝ)) (nhds 0)
This theorem statement is a version of the Riemann-Lebesgue lemma for functions defined on a finite-dimensional real vector space, formulated in terms of the space's dual. The theorem states that for a given function `f` mapping a vector space `V` to a normed additive commutative group `E`, under certain conditions on `V` (such as it being a topological vector space, a `T2Space`, a `FiniteDimensional` real vector space, etc., and given a measure `μ` on `V` that is an additive Haar measure), the function that maps `w` (an element from the space of continuous linear maps from `V` into real numbers) to the integral of the product of `Real.fourierChar` function evaluated at `-w v` and `f v` (integrated with respect to the measure `μ`), converges to `0` as `w` tends to infinity in the complement of compact sets of the space of continuous linear maps from `V` into real numbers. This is expressed in Lean 4 using the `Filter.Tendsto` predicate, which captures the notion of a function tending to a limit.
More concisely: For a continuous function `f` on a finite-dimensional real vector space `V` endowed with a Haar measure `μ`, the integral of the product of `f v` and the character of a continuous linear functional `w` with respect to `μ` approaches zero as `w` tends to infinity outside of compact sets.
|
tendsto_integral_exp_smul_cocompact_of_inner_product
theorem tendsto_integral_exp_smul_cocompact_of_inner_product :
∀ {E : Type u_1} {V : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] (f : V → E)
[inst_2 : NormedAddCommGroup V] [inst_3 : MeasurableSpace V] [inst_4 : BorelSpace V]
[inst_5 : InnerProductSpace ℝ V] [inst_6 : FiniteDimensional ℝ V] (μ : MeasureTheory.Measure V)
[inst_7 : μ.IsAddHaarMeasure],
Filter.Tendsto (fun w => ∫ (v : V), Real.fourierChar (-w v) • f v ∂μ) (Filter.cocompact (V →L[ℝ] ℝ)) (nhds 0)
This is the Riemann-Lebesgue lemma for functions on a finite-dimensional inner-product space, expressed using the dual space. This theorem states that for every normed additive commutative group `E`, normed space `ℂ E`, function `f` from `V` to `E`, normed additive commutative group `V`, measurable space `V`, Borel space `V`, inner product space `ℝ V`, finite dimensional `ℝ V`, and measure `μ` which is an additive Haar measure, the limit of the integral of `Real.fourierChar (-w v) • f v` with respect to `μ` as `w` approaches the compact complement of the dual space of `V` over `ℝ` is equal to 0 in the neighborhood filter of 0. This theorem is not meant to be used directly, but is a stepping stone to `tendsto_integral_exp_smul_cocompact` where the inner product space structure is not required.
More concisely: For every measurable function `f` from a finite-dimensional inner product space `V` to a normed space `E`, with respect to an additive Haar measure `μ` on the Borel space `V`, the integral of `f(v) ⊤ χ(-w ⊤ v) dv` with respect to `w` in the compact complement of the dual space of `V` converges to 0 as `w` approaches the boundary.
|
Real.tendsto_integral_exp_smul_cocompact
theorem Real.tendsto_integral_exp_smul_cocompact :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] (f : ℝ → E),
Filter.Tendsto (fun w => ∫ (v : ℝ), Real.fourierChar (-(v * w)) • f v) (Filter.cocompact ℝ) (nhds 0)
The theorem `Real.tendsto_integral_exp_smul_cocompact` is a version of the Riemann-Lebesgue lemma for functions on the real numbers. It states that for every function `f` from the real numbers to a complex normed space `E`, the limit as `w` approaches a compact set in the real numbers of the integral over `v` of `f(v)` multiplied by the exponential of `-v * w * 2πi` (where `i` is the imaginary unit) is zero. Here, the limit is taken with respect to the filter of complements of compact sets (cocompact filter) in the real numbers, and the limit is zero in the neighborhood filter at 0.
More concisely: For every real-valued function `f` on the real numbers and any compact set in the real numbers, the Riemann-Lebesgue integral of `f(v) * exp(-v * w * 2πi) dv` with respect to the cocompact filter on `w` is zero.
|
Real.zero_at_infty_fourierIntegral
theorem Real.zero_at_infty_fourierIntegral :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] (f : ℝ → E),
Filter.Tendsto (Real.fourierIntegral f) (Filter.cocompact ℝ) (nhds 0)
The theorem `Real.zero_at_infty_fourierIntegral` is the statement of the Riemann-Lebesgue lemma for functions on real numbers (`ℝ`), formulated using Fourier integrals. For any normed additively commutative group `E` that is also a normed space over the complex numbers (`ℂ`), and for any function `f` from real numbers to `E`, the Fourier integral of `f` tends to zero at infinity. In other words, as we take the Fourier integral over larger and larger complements of compact sets (represented by `Filter.cocompact ℝ`), the value of the Fourier integral approaches zero (represented by `nhds 0`). This captures the essence of the Riemann-Lebesgue lemma, which states that the Fourier transform of a function that is absolutely integrable over `ℝ` tends to zero at infinity.
More concisely: For any function `f` from real numbers to a normed additively commutative group `E` over the complex numbers, the Fourier integral of `f` with respect to ` Filter.cocompact ℝ` approaches zero.
|
tendsto_integral_exp_inner_smul_cocompact
theorem tendsto_integral_exp_inner_smul_cocompact :
∀ {E : Type u_1} {V : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] (f : V → E)
[inst_2 : NormedAddCommGroup V] [inst_3 : MeasurableSpace V] [inst_4 : BorelSpace V]
[inst_5 : InnerProductSpace ℝ V] [inst_6 : FiniteDimensional ℝ V],
Filter.Tendsto (fun w => ∫ (v : V), Real.fourierChar (-⟪v, w⟫_ℝ) • f v) (Filter.cocompact V) (nhds 0)
The theorem `tendsto_integral_exp_inner_smul_cocompact` is Lean's version of the Riemann-Lebesgue Lemma for functions on a real inner-product space. The lemma states that for a given function `f` mapping from a finite-dimensional real vector space `V` to a complex normed addative commutative group `E`, the integral of `f` where it is multiplied by an exponential factor `exp (-2 * π * ⟪w, v⟫ * I)` (with `⟪w, v⟫` representing the inner product of `w` and `v` in `V`) tends to zero as `w` approaches infinity. Here, the convergence is considered with respect to a co-compact filter on `V` and the neighborhood filter at zero. In mathematical terms, we would express the statement of the lemma as:
\[ \lim_{{w \to \infty, w \in V}} \int_V exp(-2\pi \langle v, w \rangle i) f(v) dv = 0\]
The theorem assumes that `V` is equipped with a Borel measurable space structure and that `f` is measurable with respect to this structure.
More concisely: The theorem `tendsto_integral_exp_inner_smul_cocompact` asserts that for a measurable function `f` from a finite-dimensional real inner-product space `V` to a complex normed additive commutative group `E`, equipped with a Borel measurable space structure, the integral of `f` multiplied by `exp(-2*π**I)` over `V` tends to zero with respect to the co-compact filter on `V` as `w` approaches infinity.
|
Real.zero_at_infty_vector_fourierIntegral
theorem Real.zero_at_infty_vector_fourierIntegral :
∀ {E : Type u_1} {V : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] (f : V → E)
[inst_2 : AddCommGroup V] [inst_3 : TopologicalSpace V] [inst_4 : TopologicalAddGroup V] [inst_5 : T2Space V]
[inst_6 : MeasurableSpace V] [inst_7 : BorelSpace V] [inst_8 : Module ℝ V] [inst_9 : ContinuousSMul ℝ V]
[inst_10 : FiniteDimensional ℝ V] (μ : MeasureTheory.Measure V) [inst_11 : μ.IsAddHaarMeasure],
Filter.Tendsto (VectorFourier.fourierIntegral Real.fourierChar μ (topDualPairing ℝ V).flip f)
(Filter.cocompact (V →L[ℝ] ℝ)) (nhds 0)
This theorem is the Riemann-Lebesgue lemma in the context of Fourier integrals applied to vector spaces. The lemma states that for a given function `f` mapping from a finite-dimensional vector space `V` to a normed additive commutative group `E`, under certain conditions on `V`, including it being a topological space, a topological add group, a `T2` space, a measurable space, a Borel space, a real module, and a vector space with a continuous scalar multiplication operation, and `V` having a measure `μ` that is an additive Haar measure, the Fourier integral of `f` with respect to the standard additive character of real numbers and the measure `μ`, paired with its dual space `V` using a flipped version of the canonical pairing, tends to zero when evaluated at infinity. This is expressed in the language of filter theory as the function `VectorFourier.fourierIntegral Real.fourierChar μ (topDualPairing ℝ V).flip f` tends to zero in the filter of the complements of compact sets in the space of continuous linear maps from `V` to the real numbers.
More concisely: Given a function `f` from a topological vector space `V` to a normed additive commutative group `E`, with `V` being a measurable Borel real module, endowed with a continuous scalar multiplication and a Haar measure `μ`, the Fourier integral of `f` with respect to the standard additive character of real numbers and `μ`, evaluated using the flipped canonical pairing, tends to zero on the space of continuous linear functions as `μ` restricts to the complements of compact sets.
|