OAI/Geometry/SurfaceImmersion/Primitive/PeriodicLocalizedBump.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Smooth positive-mass bumps on the unit circle, localized inside one period.

  1. def OAI.ClosedSurfaceR4.LoopDensity.circleBump line 12
  2. lemma OAI.ClosedSurfaceR4.LoopDensity.circleBump_smooth line 15
  3. lemma OAI.ClosedSurfaceR4.LoopDensity.circleBump_periodic line 19
  4. lemma OAI.ClosedSurfaceR4.LoopDensity.circleBump_at_center line 26
  5. lemma OAI.ClosedSurfaceR4.LoopDensity.sine_nonzero line 30
  6. theorem OAI.ClosedSurfaceR4.LoopDensity.exists_localized_bump line 41

    Source documentation

    An actual smooth periodic nonnegative density of mass one supported in any prescribed neighborhood of an interior point of the fundamental interval.

    theorem exists_localized_bump {c : ℝ} (hc : c ∈ Ioo (0 : ℝ) 1)
    {V : Set ℝ} (hV : IsOpen V) (hcV : c ∈ V) :
    ∃ ψ : ℝ → ℝ, ContDiff ℝ ∞ ψ ∧ Function.Periodic ψ 1 ∧
      (∀ t, 0 ≤ ψ t) ∧ (∫ t in 0..1, ψ t) = 1 ∧
      ∀ t ∈ Icc (0 : ℝ) 1, t ∉ V → ψ t = 0 := by
…