Documentation

Mathlib.Analysis.Calculus.BumpFunction.Normed

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.

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} [NormedAddCommGroup E] [NormedSpace E] [HasContDiffBump E] [MeasurableSpace E] {c : E} (f : ContDiffBump c) {μ : MeasureTheory.Measure E} (x : E) :
    f.normed μ x = f x / ∫ (x : E), f xμ
    theorem ContDiffBump.nonneg_normed {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] [HasContDiffBump E] [MeasurableSpace E] {c : E} (f : ContDiffBump c) {μ : MeasureTheory.Measure E} (x : E) :
    0 f.normed μ x
    theorem ContDiffBump.normed_sub {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] [HasContDiffBump E] [MeasurableSpace E] {c : E} (f : ContDiffBump c) {μ : MeasureTheory.Measure E} (x : E) :
    f.normed μ (c - x) = f.normed μ (c + x)
    theorem ContDiffBump.normed_neg {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] [HasContDiffBump E] [MeasurableSpace E] {μ : MeasureTheory.Measure E} (f : ContDiffBump 0) (x : E) :
    f.normed μ (-x) = f.normed μ x
    theorem ContDiffBump.integral_pos {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] [HasContDiffBump E] [MeasurableSpace E] {c : E} (f : ContDiffBump c) {μ : MeasureTheory.Measure E} [BorelSpace E] [FiniteDimensional E] [MeasureTheory.IsLocallyFiniteMeasure μ] [μ.IsOpenPosMeasure] :
    0 < ∫ (x : E), f xμ
    theorem ContDiffBump.integral_normed {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] [HasContDiffBump E] [MeasurableSpace E] {c : E} (f : ContDiffBump c) {μ : MeasureTheory.Measure E} [BorelSpace E] [FiniteDimensional E] [MeasureTheory.IsLocallyFiniteMeasure μ] [μ.IsOpenPosMeasure] :
    ∫ (x : E), f.normed μ xμ = 1
    theorem ContDiffBump.tendsto_support_normed_smallSets {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] [HasContDiffBump E] [MeasurableSpace E] {c : E} {μ : MeasureTheory.Measure E} [BorelSpace E] [FiniteDimensional E] [MeasureTheory.IsLocallyFiniteMeasure μ] [μ.IsOpenPosMeasure] {ι : Type u_2} {φ : ιContDiffBump c} {l : Filter ι} (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} [NormedAddCommGroup E] [NormedSpace E] [HasContDiffBump E] [MeasurableSpace E] {c : E} (f : ContDiffBump c) (μ : MeasureTheory.Measure E) [BorelSpace E] [FiniteDimensional E] [MeasureTheory.IsLocallyFiniteMeasure μ] [μ.IsOpenPosMeasure] {X : Type u_2} [NormedAddCommGroup X] [NormedSpace X] [CompleteSpace X] (z : X) :
    ∫ (x : E), f.normed μ x zμ = z
    theorem ContDiffBump.measure_closedBall_div_le_integral {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] [HasContDiffBump E] [MeasurableSpace E] {c : E} (f : ContDiffBump c) (μ : MeasureTheory.Measure E) [BorelSpace E] [FiniteDimensional E] [MeasureTheory.IsLocallyFiniteMeasure μ] [μ.IsAddHaarMeasure] (K : ) (h : f.rOut K * f.rIn) :
    (μ (Metric.closedBall c f.rOut)).toReal / K ^ FiniteDimensional.finrank E ∫ (x : E), f xμ
    theorem ContDiffBump.normed_le_div_measure_closedBall_rOut {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] [HasContDiffBump E] [MeasurableSpace E] {c : E} (f : ContDiffBump c) (μ : MeasureTheory.Measure E) [BorelSpace E] [FiniteDimensional E] [MeasureTheory.IsLocallyFiniteMeasure μ] [μ.IsOpenPosMeasure] [μ.IsAddHaarMeasure] (K : ) (h : f.rOut K * f.rIn) (x : E) :
    f.normed μ x K ^ FiniteDimensional.finrank E / (μ (Metric.closedBall c f.rOut)).toReal