exists_contDiff_dist_le_of_forall_mem_ball_dist_le

English

The integral of f.normed μ over μ equals 1: ∫ f.normed μ dμ = 1.

Русский

Интеграл f.normed μ по μ равен единице: ∫ f.normed μ dμ = 1.

LaTeX

$$$ \int_E f.normed\mu(x) \, d\mu(x) = 1 $$$

Lean4

theorem exists_contDiff_dist_le_of_forall_mem_ball_dist_le [MeasurableSpace E] [BorelSpace E] {μ : Measure E}
    [μ.IsAddHaarMeasure] (hf : LocallyIntegrable f μ) (hε : 0 < ε) :
    ∃ g : E → F, ContDiff ℝ ∞ g ∧ ∀ a, ∀ δ, (∀ x ∈ ball a ε, dist (f x) (f a) ≤ δ) → dist (g a) (f a) ≤ δ :=
  by
  set φ : ContDiffBump (0 : E) := ⟨ε / 2, ε, half_pos hε, half_lt_self hε⟩
  refine ⟨_, ?_, fun a δ ↦ φ.dist_normed_convolution_le hf.aestronglyMeasurable⟩
  exact φ.hasCompactSupport_normed.contDiff_convolution_left _ φ.contDiff_normed hf

Похожие утверждения