ae_eq_zero_of_integral_smooth_smul_eq_zero
theorem ae_eq_zero_of_integral_smooth_smul_eq_zero :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
{F : Type u_2} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] [inst_5 : CompleteSpace F]
{H : Type u_3} [inst_6 : TopologicalSpace H] (I : ModelWithCorners ℝ E H) {M : Type u_4}
[inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace H M] [inst_9 : SmoothManifoldWithCorners I M]
[inst_10 : MeasurableSpace M] [inst_11 : BorelSpace M] [inst_12 : SigmaCompactSpace M] [inst_13 : T2Space M]
{f : M → F} {μ : MeasureTheory.Measure M},
MeasureTheory.LocallyIntegrable f μ →
(∀ (g : M → ℝ), Smooth I (modelWithCornersSelf ℝ ℝ) g → HasCompactSupport g → ∫ (x : M), g x • f x ∂μ = 0) →
∀ᵐ (x : M) ∂μ, f x = 0
This theorem states that given a locally integrable function `f` from a finite-dimensional real manifold `M` to a normed space `F`, if the integral of `f` multiplied by any smooth function `g` with compact support is zero for all such `g`, then `f` is almost everywhere equal to zero (meaning that it equals zero except on a set of measure zero). In other words, if `f` is such that its integral against every compactly supported smooth function is zero, then `f` itself must be zero almost everywhere.
More concisely: If a locally integrable function `f` from a finite-dimensional real manifold `M` to a normed space `F` satisfies ∫ₙf.dμ = 0 for all compactly supported smooth functions `g` on `M`, then `f` is almost everywhere equal to the zero function.
|
ae_eq_zero_of_integral_contDiff_smul_eq_zero
theorem ae_eq_zero_of_integral_contDiff_smul_eq_zero :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
{F : Type u_2} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] [inst_5 : CompleteSpace F]
[inst_6 : MeasurableSpace E] [inst_7 : BorelSpace E] {f : E → F} {μ : MeasureTheory.Measure E},
MeasureTheory.LocallyIntegrable f μ →
(∀ (g : E → ℝ), ContDiff ℝ ⊤ g → HasCompactSupport g → ∫ (x : E), g x • f x ∂μ = 0) → ∀ᵐ (x : E) ∂μ, f x = 0
The theorem states that for a locally integrable function `f` on a finite-dimensional real vector space, if the integral of `f` multiplied by any infinitely differentiable (smooth) function with compact support is zero, then `f` is zero almost everywhere. Here, a function is said to have compact support if it is zero outside a compact set. In other words, the result of multiplying `f` by any smooth function that is non-zero only on a compact set and then integrating over the entire space is always zero, it implies that `f` must be zero almost everywhere in the space.
More concisely: If a locally integrable function `f` on a finite-dimensional real vector space annihilates all infinitely differentiable functions with compact support during integration, then `f` is almost everywhere zero.
|
ae_eq_of_integral_smooth_smul_eq
theorem ae_eq_of_integral_smooth_smul_eq :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
{F : Type u_2} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] [inst_5 : CompleteSpace F]
{H : Type u_3} [inst_6 : TopologicalSpace H] (I : ModelWithCorners ℝ E H) {M : Type u_4}
[inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace H M] [inst_9 : SmoothManifoldWithCorners I M]
[inst_10 : MeasurableSpace M] [inst_11 : BorelSpace M] [inst_12 : SigmaCompactSpace M] [inst_13 : T2Space M]
{f f' : M → F} {μ : MeasureTheory.Measure M},
MeasureTheory.LocallyIntegrable f μ →
MeasureTheory.LocallyIntegrable f' μ →
(∀ (g : M → ℝ),
Smooth I (modelWithCornersSelf ℝ ℝ) g →
HasCompactSupport g → ∫ (x : M), g x • f x ∂μ = ∫ (x : M), g x • f' x ∂μ) →
∀ᵐ (x : M) ∂μ, f x = f' x
The theorem `ae_eq_of_integral_smooth_smul_eq` states that given two locally integrable functions `f` and `f'` on a finite-dimensional real manifold `M`, if for every smooth function `g` with compact support, the integral of `g` multiplied by `f` equals the integral of `g` multiplied by `f'`, then `f` and `f'` are equal almost everywhere. Here, a function is considered to be locally integrable if it is integrable on a neighbourhood of every point. The function `g` is smooth if it's infinitely differentiable, and has compact support if it equals zero outside a compact set. The term 'almost everywhere' means that the set of points where the equality doesn't hold has measure zero.
More concisely: If two locally integrable functions on a finite-dimensional real manifold have equal integrals against every smooth function with compact support, then they are almost everywhere equal.
|
IsOpen.ae_eq_zero_of_integral_contDiff_smul_eq_zero
theorem IsOpen.ae_eq_zero_of_integral_contDiff_smul_eq_zero :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
{F : Type u_2} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] [inst_5 : CompleteSpace F]
[inst_6 : MeasurableSpace E] [inst_7 : BorelSpace E] {f : E → F} {μ : MeasureTheory.Measure E} {U : Set E},
IsOpen U →
MeasureTheory.LocallyIntegrableOn f U μ →
(∀ (g : E → ℝ), ContDiff ℝ ⊤ g → HasCompactSupport g → tsupport g ⊆ U → ∫ (x : E), g x • f x ∂μ = 0) →
∀ᵐ (x : E) ∂μ, x ∈ U → f x = 0
This theorem states that if a function `f` is locally integrable on an open subset `U` of a finite-dimensional real manifold, and if the integral of `f` multiplied by any smooth function that has compact support within `U` is zero, then the function `f` equals zero almost everywhere in `U`. Here, "almost everywhere" means that the set of points where the function does not equal zero has a measure of zero. The smooth function with compact support is differentiable to any order and is zero outside a compact set. The condition about the integral being zero effectively ensures that `f` and the smooth function are orthogonal in terms of the L^2 inner product, which is the integral of their product.
More concisely: If a locally integrable function `f` on an open subset `U` of a finite-dimensional real manifold satisfies the property that the integral of `f` with any smooth, compactly supported function equals zero, then `f` equals zero almost everywhere in `U`.
|
IsOpen.ae_eq_zero_of_integral_smooth_smul_eq_zero'
theorem IsOpen.ae_eq_zero_of_integral_smooth_smul_eq_zero' :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
{F : Type u_2} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] [inst_5 : CompleteSpace F]
{H : Type u_3} [inst_6 : TopologicalSpace H] (I : ModelWithCorners ℝ E H) {M : Type u_4}
[inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace H M] [inst_9 : SmoothManifoldWithCorners I M]
[inst_10 : MeasurableSpace M] [inst_11 : BorelSpace M] [inst_12 : T2Space M] {f : M → F}
{μ : MeasureTheory.Measure M} {U : Set M},
IsOpen U →
IsSigmaCompact U →
MeasureTheory.LocallyIntegrableOn f U μ →
(∀ (g : M → ℝ),
Smooth I (modelWithCornersSelf ℝ ℝ) g →
HasCompactSupport g → tsupport g ⊆ U → ∫ (x : M), g x • f x ∂μ = 0) →
∀ᵐ (x : M) ∂μ, x ∈ U → f x = 0
The theorem `IsOpen.ae_eq_zero_of_integral_smooth_smul_eq_zero'` describes the following mathematical statement:
If we have a function `f` that is locally integrable on an open subset `U` of a finite-dimensional real manifold, and given any smooth function `g` that is compactly supported in `U`, the integral of `f` multiplied by `g` over the entire manifold is equal to zero, then `f` equals zero almost everywhere in `U`.
In this context, 'almost everywhere' is defined with respect to a given measure `μ`. The function `f` takes points from the manifold to a complete normed additive commutative group. The open subset `U` is required to be σ-compact, which means it can be expressed as a countable union of compact sets. The function `g` is assumed to be smooth and its support is contained within `U`. The theorem's conclusion states that for almost all points `x` in `U` (i.e., except possibly for a set of measure zero), the value of `f` at `x` is zero.
More concisely: If a locally integrable function `f` on a σ-compact open subset `U` of a finite-dimensional real manifold satisfies the property that the integral of `f` multiplied by any smooth, compactly supported function `g` over the entire manifold is zero, then `f` equals zero almost everywhere in `U` with respect to a given measure.
|
ae_eq_of_integral_contDiff_smul_eq
theorem ae_eq_of_integral_contDiff_smul_eq :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
{F : Type u_2} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] [inst_5 : CompleteSpace F]
[inst_6 : MeasurableSpace E] [inst_7 : BorelSpace E] {f f' : E → F} {μ : MeasureTheory.Measure E},
MeasureTheory.LocallyIntegrable f μ →
MeasureTheory.LocallyIntegrable f' μ →
(∀ (g : E → ℝ), ContDiff ℝ ⊤ g → HasCompactSupport g → ∫ (x : E), g x • f x ∂μ = ∫ (x : E), g x • f' x ∂μ) →
∀ᵐ (x : E) ∂μ, f x = f' x
This theorem states that if we have two locally integrable functions, `f` and `f'`, on a finite-dimensional real vector space, and for every smooth function `g` with compact support, the integral of `g` times `f` is equal to the integral of `g` times `f'`, then `f` and `f'` are equal almost everywhere. Here, a function is said to be locally integrable if it is integrable on a neighborhood of every point, and a function has compact support if it is equal to zero outside a compact set. The theorem assumes that the space in which functions are defined is equipped with a measure (denoted `μ`), which is often used to "weigh" different parts of the space differently.
More concisely: If two locally integrable functions on a finite-dimensional real vector space with a measure have the same integral against every smooth function with compact support, then they are almost everywhere equal.
|