ContDiffBump.integrable
theorem ContDiffBump.integrable :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : HasContDiffBump E]
[inst_3 : MeasurableSpace E] {c : E} (f : ContDiffBump c) {μ : MeasureTheory.Measure E} [inst_4 : BorelSpace E]
[inst_5 : FiniteDimensional ℝ E] [inst_6 : MeasureTheory.IsLocallyFiniteMeasure μ],
MeasureTheory.Integrable (↑f) μ
The theorem `ContDiffBump.integrable` states that for any continuously differentiable bump function `f` centered at a point `c` in a normed additive commutative group `E` that is also a normed space over the real numbers, and for which `E` is a measurable space, a Borel space, and a finite-dimensional vector space over the real numbers, and given a measure `μ` on `E` that is locally finite, the function `f` is integrable with respect to the measure `μ`. In mathematical terms, the integral of the norm of `f` with respect to `μ` is finite and that `f` is almost everywhere strongly measurable.
More concisely: A continuously differentiable bump function centered at a point in a locally finite, Borel measure on a finite-dimensional, normed additive commutative group that is also a normed space over the real numbers is integrable.
|
ContDiffBump.integral_pos
theorem ContDiffBump.integral_pos :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : HasContDiffBump E]
[inst_3 : MeasurableSpace E] {c : E} (f : ContDiffBump c) {μ : MeasureTheory.Measure E} [inst_4 : BorelSpace E]
[inst_5 : FiniteDimensional ℝ E] [inst_6 : MeasureTheory.IsLocallyFiniteMeasure μ] [inst_7 : μ.IsOpenPosMeasure],
0 < ∫ (x : E), ↑f x ∂μ
This theorem states that for any normed additive commutative group `E` (which also has a normed space over real numbers, and possesses a continuously differentiable "bump" function), given a measure `μ` on `E` which is both locally finite and positive on open sets, and a specific continuously differentiable bump function `f` centered at a point `c` in `E`, then the integral of `f` with respect to `μ` is always positive. Here, `E` is also assumed to be a Borel space and a finite-dimensional vector space over the real numbers.
More concisely: For any normed additive commutative group `E` (Borel, finite-dimensional over the real numbers) with a continuously differentiable "bump" function, a locally finite and positive measure `μ` on `E`, and a continuously differentiable bump function `f` centered at a point `c` in `E`, the integral of `f` with respect to `μ` is positive.
|
ContDiffBump.normed_def
theorem ContDiffBump.normed_def :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : HasContDiffBump E]
[inst_3 : MeasurableSpace E] {c : E} (f : ContDiffBump c) {μ : MeasureTheory.Measure E} (x : E),
f.normed μ x = ↑f x / ∫ (x : E), ↑f x ∂μ
The theorem `ContDiffBump.normed_def` states that for any type `E` that forms a normed additive commutative group, is a normed space over the real numbers, and has a "bump" function that is continuously differentiable, and for any `E` that forms a measurable space, any "bump" function `f` centered at a point `c` in `E`, any measure `μ` on `E`, and any point `x` in `E`, the value of the normalized "bump" function at `x` is equal to the value of `f` at `x` divided by the integral over `E` of `f` with respect to `μ`. In other words, the normalized "bump" function at a point is the ratio of the value of the "bump" function at that point to the "total area" under the "bump" function.
More concisely: For any normed additive commutative group `E` over the real numbers, with a continuously differentiable "bump" function `f` and a measurable space `(E, μ)`, the normalized bump function `f / ∫(f dμ)` equals the identity function at every point `x` in `E`. (Note: This statement assumes that the integral ∫(f dμ) is non-zero.)
|
ContDiffBump.support_normed_eq
theorem ContDiffBump.support_normed_eq :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : HasContDiffBump E]
[inst_3 : MeasurableSpace E] {c : E} (f : ContDiffBump c) {μ : MeasureTheory.Measure E} [inst_4 : BorelSpace E]
[inst_5 : FiniteDimensional ℝ E] [inst_6 : MeasureTheory.IsLocallyFiniteMeasure μ] [inst_7 : μ.IsOpenPosMeasure],
Function.support (f.normed μ) = Metric.ball c f.rOut
This theorem states that for a given continuously differentiable bump function `f` centered at `c` in a finite-dimensional normed add-commutative group `E` over the real numbers, the support of the normalized version of the bump function (where the normalization is such that the integral of the function over the measure space equals one) is equal to the open ball centered at `c` with radius equal to the outer radius of the bump function. Here, the measure space is assumed to have Borel-measurable sets, to be locally finite, and to have positive measure for open sets.
More concisely: For a continuously differentiable bump function `f` over a finite-dimensional normed add-commutative group `E` with center `c`, the support of the normalized version of `f` equals the open ball centered at `c` with radius equal to the outer radius of `f`, in a measure space with Borel-measurable sets, local finiteness, and positive measure for open sets.
|