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} [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

• ContDiffBump.normed f μ x = ↑f x / ∫ (x : E), ↑f x ∂μ

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) : ContDiffBump.normed f μ 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 ≤ ContDiffBump.normed f μ x

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 (ContDiffBump.normed f μ)

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 (ContDiffBump.normed f μ)

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) : ContDiffBump.normed f μ (c - x) = ContDiffBump.normed f μ (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) : ContDiffBump.normed f μ (-x) = ContDiffBump.normed f μ x

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

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 (ContDiffBump.normed f μ)

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 μ] [MeasureTheory.Measure.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 μ] [MeasureTheory.Measure.IsOpenPosMeasure μ] : ∫ (x : E), ContDiffBump.normed f μ x ∂μ = 1

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 μ] [MeasureTheory.Measure.IsOpenPosMeasure μ] : Function.support (ContDiffBump.normed f μ) = Metric.ball c f.rOut

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 μ] [MeasureTheory.Measure.IsOpenPosMeasure μ] : tsupport (ContDiffBump.normed f μ) = Metric.closedBall c f.rOut

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 μ] [MeasureTheory.Measure.IsOpenPosMeasure μ] : HasCompactSupport (ContDiffBump.normed f μ)

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 μ] [MeasureTheory.Measure.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) => ContDiffBump.normed (φ i) μ x) l (Filter.smallSets (nhds c))

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 μ] [MeasureTheory.Measure.IsOpenPosMeasure μ] {X : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] (z : X) : ∫ (x : E), ContDiffBump.normed f μ x • z ∂μ = z

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 μ] : ENNReal.toReal (↑↑μ (Metric.closedBall c f.rIn)) ≤ ∫ (x : E), ↑f x ∂μ

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 μ] [MeasureTheory.Measure.IsOpenPosMeasure μ] (x : E) : ContDiffBump.normed f μ x ≤ 1 / ENNReal.toReal (↑↑μ (Metric.closedBall c f.rIn))

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 ∂μ ≤ ENNReal.toReal (↑↑μ (Metric.closedBall c f.rOut))

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 μ] [MeasureTheory.Measure.IsAddHaarMeasure μ] (K : ℝ) (h : f.rOut ≤ K * f.rIn) : ENNReal.toReal (↑↑μ (Metric.closedBall c f.rOut)) / 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 μ] [MeasureTheory.Measure.IsOpenPosMeasure μ] [MeasureTheory.Measure.IsAddHaarMeasure μ] (K : ℝ) (h : f.rOut ≤ K * f.rIn) (x : E) : ContDiffBump.normed f μ x ≤ K ^ FiniteDimensional.finrank ℝ E / ENNReal.toReal (↑↑μ (Metric.closedBall c f.rOut))