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.

noncomputable 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 ∂μ

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.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 μ)

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 μ)

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

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.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

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

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 μ)

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_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 μ] : μ.real (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 μ] [μ.IsOpenPosMeasure] (x : E) : f.normed μ x ≤ 1 / μ.real (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 ∂μ ≤ μ.real (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 μ] [μ.IsAddHaarMeasure] (K : ℝ) (h : f.rOut ≤ K * f.rIn) : μ.real (Metric.closedBall c f.rOut) / K ^ Module.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 μ] [μ.IsAddHaarMeasure] (K : ℝ) (h : f.rOut ≤ K * f.rIn) (x : E) : f.normed μ x ≤ K ^ Module.finrank ℝ E / μ.real (Metric.closedBall c f.rOut)