# Normed bump function #

In this file we define ContDiffBump.normed f μ to be the bump function f normalized so that ∫ x, f.normed μ x ∂μ = 1 and prove some properties of this function.

def ContDiffBump.normed {E : Type u_1} [] [] [] {c : E} (f : ) (μ : ) :
E

A bump function normed so that ∫ x, f.normed μ x ∂μ = 1.

Equations
• f.normed μ x = f x / ∫ (x : E), f xμ
Instances For
theorem ContDiffBump.normed_def {E : Type u_1} [] [] [] {c : E} (f : ) {μ : } (x : E) :
f.normed μ x = f x / ∫ (x : E), f xμ
theorem ContDiffBump.nonneg_normed {E : Type u_1} [] [] [] {c : E} (f : ) {μ : } (x : E) :
0 f.normed μ x
theorem ContDiffBump.contDiff_normed {E : Type u_1} [] [] [] {c : E} (f : ) {μ : } {n : ℕ∞} :
ContDiff n (f.normed μ)
theorem ContDiffBump.continuous_normed {E : Type u_1} [] [] [] {c : E} (f : ) {μ : } :
Continuous (f.normed μ)
theorem ContDiffBump.normed_sub {E : Type u_1} [] [] [] {c : E} (f : ) {μ : } (x : E) :
f.normed μ (c - x) = f.normed μ (c + x)
theorem ContDiffBump.normed_neg {E : Type u_1} [] [] [] {μ : } (f : ) (x : E) :
f.normed μ (-x) = f.normed μ x
theorem ContDiffBump.integrable {E : Type u_1} [] [] [] {c : E} (f : ) {μ : } [] [] :
theorem ContDiffBump.integrable_normed {E : Type u_1} [] [] [] {c : E} (f : ) {μ : } [] [] :
MeasureTheory.Integrable (f.normed μ) μ
theorem ContDiffBump.integral_pos {E : Type u_1} [] [] [] {c : E} (f : ) {μ : } [] [] [μ.IsOpenPosMeasure] :
0 < ∫ (x : E), f xμ
theorem ContDiffBump.integral_normed {E : Type u_1} [] [] [] {c : E} (f : ) {μ : } [] [] [μ.IsOpenPosMeasure] :
∫ (x : E), f.normed μ xμ = 1
theorem ContDiffBump.support_normed_eq {E : Type u_1} [] [] [] {c : E} (f : ) {μ : } [] [] [μ.IsOpenPosMeasure] :
Function.support (f.normed μ) = Metric.ball c f.rOut
theorem ContDiffBump.tsupport_normed_eq {E : Type u_1} [] [] [] {c : E} (f : ) {μ : } [] [] [μ.IsOpenPosMeasure] :
tsupport (f.normed μ) = Metric.closedBall c f.rOut
theorem ContDiffBump.hasCompactSupport_normed {E : Type u_1} [] [] [] {c : E} (f : ) {μ : } [] [] [μ.IsOpenPosMeasure] :
HasCompactSupport (f.normed μ)
theorem ContDiffBump.tendsto_support_normed_smallSets {E : Type u_1} [] [] [] {c : E} {μ : } [] [] [μ.IsOpenPosMeasure] {ι : Type u_2} {φ : ι} {l : } (hφ : Filter.Tendsto (fun (i : ι) => (φ i).rOut) l (nhds 0)) :
Filter.Tendsto (fun (i : ι) => Function.support fun (x : E) => (φ i).normed μ x) l (nhds c).smallSets
theorem ContDiffBump.integral_normed_smul {E : Type u_1} [] [] [] {c : E} (f : ) (μ : ) [] [] [μ.IsOpenPosMeasure] {X : Type u_2} [] [] (z : X) :
∫ (x : E), f.normed μ x zμ = z
theorem ContDiffBump.measure_closedBall_le_integral {E : Type u_1} [] [] [] {c : E} (f : ) (μ : ) [] [] :
(μ (Metric.closedBall c f.rIn)).toReal ∫ (x : E), f xμ
theorem ContDiffBump.normed_le_div_measure_closedBall_rIn {E : Type u_1} [] [] [] {c : E} (f : ) (μ : ) [] [] [μ.IsOpenPosMeasure] (x : E) :
f.normed μ x 1 / (μ (Metric.closedBall c f.rIn)).toReal
theorem ContDiffBump.integral_le_measure_closedBall {E : Type u_1} [] [] [] {c : E} (f : ) (μ : ) [] [] :
∫ (x : E), f xμ (μ (Metric.closedBall c f.rOut)).toReal
theorem ContDiffBump.measure_closedBall_div_le_integral {E : Type u_1} [] [] [] {c : E} (f : ) (μ : ) [] [] [μ.IsAddHaarMeasure] (K : ) (h : f.rOut K * f.rIn) :
(μ (Metric.closedBall c f.rOut)).toReal / ∫ (x : E), f xμ
theorem ContDiffBump.normed_le_div_measure_closedBall_rOut {E : Type u_1} [] [] [] {c : E} (f : ) (μ : ) [] [] [μ.IsOpenPosMeasure] [μ.IsAddHaarMeasure] (K : ) (h : f.rOut K * f.rIn) (x : E) :
f.normed μ x / (μ (Metric.closedBall c f.rOut)).toReal