Delta mollifiers

A key ingredient in the proof of the reparametrization lemma is the existence of a smooth approximation to the Dirac delta function. Such an approximation is a sequence of functions δ : ℕ × S¹ → S¹, (i, t) ↦ δᵢ t such that:

• δᵢ is smooth for all i,
• δᵢ is non-negative for all i,
• ∫ x in 0..1, (δᵢ x) = 1 for all i,
• ∫ x in 0..1, (δᵢ x) • f x → f 0, as i → ∞ for any continuous function f on S¹.

This file contains a construction approxDirac of such a family δ together with code which packages this into the precise form required for the proof of the reparametrization lemma: deltaMollifier, Loop.mollify.

The key ingredients are the existence of smooth "bump functions" and a powerful theory of convolutions.

Bump family

In this section we construct bump (n : ℕ), a bump function with support in Ioo (-1/(n+2)) (1/(n+2)).

noncomputable def bump (n : ℕ) : ContDiffBump 0

bump n is a bump function on ℝ which has support Ioo (-(1/(n+2))) (1/(n+2)) and equals one on Icc (-(1/(n+3))) (1/(n+3)).

Equations

• bump n = { rIn := 1 / (↑n + 3), rOut := 1 / (↑n + 2), rIn_pos := ⋯, rIn_lt_rOut := ⋯ }

theorem support_bump (n : ℕ) : Function.support ↑(bump n) = Set.Ioo (-(1 / (↑n + 2))) (1 / (↑n + 2))

theorem support_bump_subset (n : ℕ) : Function.support ↑(bump n) ⊆ Set.Ioc (-(1 / 2)) (1 / 2)

theorem support_shifted_normed_bump_subset (n : ℕ) (t : ℝ) : (Function.support fun (x : ℝ) => (bump n).normed MeasureTheory.volume (x - t)) ⊆ Set.Ioc (t - 1 / 2) (t + 1 / 2)

Periodize

In this section we turn any function f : ℝ → E into a 1-periodic function fun t : ℝ ↦ ∑ᶠ n : ℤ, f (t+n).

noncomputable def periodize {M : Type u_2} [AddCommMonoid M] (f : ℝ → M) (t : ℝ) : M

Turn a function into a 1-periodic function. If its support lies in a (non-closed) interval of length 1, then this will be that function made periodic with period 1.

Equations

• periodize f t = ∑ᶠ (n : ℤ), f (t + ↑n)

theorem periodic_periodize {M : Type u_2} [AddCommMonoid M] (f : ℝ → M) : Function.Periodic (periodize f) 1

theorem periodize_nonneg {f : ℝ → ℝ} (h : ∀ (t : ℝ), 0 ≤ f t) (t : ℝ) : 0 ≤ periodize f t

theorem ContDiff.periodize {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ → E} {n : ℕ∞} (h : 𝒞 (↑n) f) (h' : HasCompactSupport f) : 𝒞 (↑n) (_root_.periodize f)

theorem periodize_comp_sub {M : Type u_2} [AddCommMonoid M] (f : ℝ → M) (x t : ℝ) : periodize (fun (x' : ℝ) => f (x' - t)) x = periodize f (x - t)

theorem periodize_smul_periodic {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : ℝ → ℝ) {g : ℝ → E} (hg : Function.Periodic g 1) (t : ℝ) : periodize f t • g t = periodize (fun (x : ℝ) => f x • g x) t

theorem integral_periodize {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : ℝ → E) {a : ℝ} (hf : Function.support f ⊆ Set.Ioc a (a + 1)) : ∫ (t : ℝ) in a..a + 1, periodize f t = ∫ (t : ℝ) in a..a + 1, f t

theorem intervalIntegral_periodize_smul {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : ℝ → ℝ) (γ : Loop E) {a b c d : ℝ} (h : b ≤ a + 1) (h2 : d = c + 1) (hf : Function.support f ⊆ Set.Ioc a b) : ∫ (t : ℝ) in c..d, periodize f t • ↑γ t = ∫ (t : ℝ), f t • ↑γ t

An approximate Dirac "on the circle".

noncomputable def approxDirac (n : ℕ) : ℝ → ℝ

A periodized bump function, which we can view as a function from 𝕊¹ → ℝ. As n → ∞ this tends to the Dirac delta function located at 0.

Equations

• approxDirac n = periodize ((bump n).normed MeasureTheory.volume)

theorem periodic_approxDirac (n : ℕ) : Function.Periodic (approxDirac n) 1

theorem approxDirac_nonneg (n : ℕ) (t : ℝ) : 0 ≤ approxDirac n t

theorem contDiff_approxDirac (n : ℕ) : 𝒞 (↑⊤) (approxDirac n)

theorem approxDirac_integral_eq_one (n : ℕ) {a b : ℝ} (h : b = a + 1) : ∫ (s : ℝ) in a..b, approxDirac n s = 1

noncomputable def deltaMollifier (n : ℕ) (t : ℝ) : ℝ → ℝ

A sequence of functions that converges to the Dirac delta function located at t, with the properties that this sequence is everywhere positive and

Equations

• deltaMollifier n t x = ↑n / (↑n + 1) * approxDirac n (x - t) + 1 / (↑n + 1)

theorem deltaMollifier_periodic {n : ℕ} {t : ℝ} : Function.Periodic (deltaMollifier n t) 1

theorem deltaMollifier_pos {n : ℕ} {t : ℝ} (s : ℝ) : 0 < deltaMollifier n t s

theorem contDiff_deltaMollifier {n : ℕ} {t : ℝ} : 𝒞 (↑⊤) (deltaMollifier n t)

@[simp]

theorem deltaMollifier_integral_eq_one {n : ℕ} {t : ℝ} : ∫ (s : ℝ) in 0..1, deltaMollifier n t s = 1

noncomputable def Loop.mollify {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] (γ : Loop F) (n : ℕ) (t : ℝ) : F

γ.mollify n t is a weighted average of γ using weights deltaMollifier n t. This means that as n → ∞ this value tends to γ t, but because deltaMollifier n t is positive, we know that we can reparametrize γ to obtain a loop that has γ.mollify n t as its actual average.

Equations

• γ.mollify n t = ∫ (s : ℝ) in 0..1, deltaMollifier n t s • ↑γ s

theorem Loop.mollify_eq_convolution {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] {n : ℕ} (γ : Loop F) (hγ : Continuous ↑γ) (t : ℝ) : γ.mollify n t = (↑n / (↑n + 1)) • MeasureTheory.convolution ((bump n).normed MeasureTheory.volume) (↑γ) (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume t + (1 / (↑n + 1)) • ∫ (t : ℝ) in 0..1, ↑γ t