PeriodicBumpAverage.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Localized positive periodic densities approximate any chosen path value.

theorem OAI.ClosedSurfaceR4.LoopDensity.exists_bump_average_near line 16

Source documentation

Point masses in the convex-hull argument can be replaced by actual smooth nonnegative densities while changing their vector moments arbitrarily little.

theorem exists_bump_average_near {f : ℝ → E} (hf : Continuous f)
    {c ε : ℝ} (hc : c ∈ Ioo (0 : ℝ) 1) (hε : 0 < ε) :
    ∃ ψ : ℝ → ℝ, ContDiff ℝ ∞ ψ ∧ Function.Periodic ψ 1 ∧
      (∀ t, 0 ≤ ψ t) ∧ (∫ t in 0..1, ψ t) = 1 ∧
      ‖(∫ t in 0..1, ψ t • f t) - f c‖ < ε := by
…