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.

source
def ContDiffBump.normed {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [HasContDiffBump E] [MeasurableSpace E] {c : E} (f : ContDiffBump c) (μ : MeasureTheory.Measure E) :
E → ℝ

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

Equations
  • f.normed μ x = ↑f x / ∫ (x : E), ↑f x ∂μ
Instances For
    source
    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 ∂μ
    source
    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
    source
    theorem ContDiffBump.contDiff_normed {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [HasContDiffBump E] [MeasurableSpace E] {c : E} (f : ContDiffBump c) {μ : MeasureTheory.Measure E} {n : ℕ∞} :
    ContDiff ℝ (↑n) (f.normed μ)
    source
    theorem ContDiffBump.continuous_normed {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [HasContDiffBump E] [MeasurableSpace E] {c : E} (f : ContDiffBump c) {μ : MeasureTheory.Measure E} :
    Continuous (f.normed μ)
    source
    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)
    source
    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
    source
    theorem ContDiffBump.integrable {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 μ] :
    MeasureTheory.Integrable (↑f) μ
    source
    theorem ContDiffBump.integrable_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 μ] :
    MeasureTheory.Integrable (f.normed μ) μ
    source
    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 ∂μ
    source
    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
    source
    theorem ContDiffBump.support_normed_eq {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] :
    Function.support (f.normed μ) = Metric.ball c f.rOut
    source
    theorem ContDiffBump.tsupport_normed_eq {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] :
    tsupport (f.normed μ) = Metric.closedBall c f.rOut
    source
    theorem ContDiffBump.hasCompactSupport_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] :
    HasCompactSupport (f.normed μ)
    source
    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
    source
    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
    source
    theorem ContDiffBump.measure_closedBall_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 μ] :
    (μ (Metric.closedBall c f.rIn)).toReal ≤ ∫ (x : E), ↑f x ∂μ
    source
    theorem ContDiffBump.normed_le_div_measure_closedBall_rIn {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 / (μ (Metric.closedBall c f.rIn)).toReal
    source
    theorem ContDiffBump.integral_le_measure_closedBall {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 μ] :
    ∫ (x : E), ↑f x ∂μ ≤ (μ (Metric.closedBall c f.rOut)).toReal
    source
    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 ^ Module.finrank ℝ E ≤ ∫ (x : E), ↑f x ∂μ
    source
    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 μ] [μ.IsAddHaarMeasure] (K : ℝ) (h : f.rOut ≤ K * f.rIn) (x : E) :
    f.normed μ x ≤ K ^ Module.finrank ℝ E / (μ (Metric.closedBall c f.rOut)).toReal