# The reparametrization lemma
This file contains a proof of Gromov's parametric reparametrization lemma. It concerns the behaviour
of the average value of a loop γ : S¹ → F when the loop is reparametrized by precomposing with a
diffeomorphism S¹ → S¹.
Given a loop γ : S¹ → F for some real vector space F, one may integrate to obtain its average
∫ x in 0..1, (γ x) in F. Although this average depends on the loop's parametrization, it
satisfies a contraint that depends only on the image of the loop: the average is contained in the
convex hull of the image of γ. The non-parametric version of the reparametrization lemma says that
conversely, given any point g in the interior of the convex hull of the image of γ, one may find
a reparametrization of γ whose average is g.
The reparametrization lemma thus allows one to reduce the problem of constructing a loop whose average is a given point, to the problem of constructing a loop subject to a condition that depends only on its image.
In fact the reparametrization lemma holds parametrically. Given a smooth family of loops:
γ : E × S¹ → F, (x, t) ↦ γₓ t, together with a smooth function g : E → F, such that g x is
contained in the interior of the convex hull of the image of γₓ for all x, there exists a smooth
family of diffeomorphism φ : E × S¹ → S¹, (x, t) ↦ φₓ t such that the average of γₓ ∘ φₓ is
g x for all x.
The idea of the proof is simple: since g x is contained in the interior of the convex hull of
the image of γₓ one may find t₀, t₁, ..., tₙ and barycentric coordinates w₀, w₁, ..., wₙ such
that g x = ∑ᵢ wᵢ • γₓ(tᵢ). If there were no smoothness requirement on φₓ one could define
it to be a step function which spends time wᵢ at each tᵢ. However because there is a smoothness
condition, one rounds off the corners of the would-be step function by using a "delta mollifier"
(an approximation to a Dirac delta function).
The above construction works locally in the neighbourhood of any x in E and one uses a partition
of unity to globalise all the local solutions into the required family: φ : E × S¹ → S¹.
The key ingredients are theories of calculus, convex hulls, barycentric coordinates, existence of delta mollifiers, partitions of unity, and the inverse function theorem.
Equations
- termι = Lean.ParserDescr.node `termι 1024 (Lean.ParserDescr.symbol "ι")
Instances For
Given a smooth function g : E → F between normed vector spaces, a smooth surrounding family
is a smooth family of loops E → loop F, x ↦ γₓ such that γₓ surrounds g x for all x.
- toFun : E → Loop F
Instances For
Equations
Given γ : SmoothSurroundingFamily g and x : E, γ.surroundingParametersAt x are the
tᵢ : ℝ, for i = 0, 1, ..., dim F such that γ x tᵢ surround g x.
Equations
Instances For
Given γ : SmoothSurroundingFamily g and x : E, γ.surroundingPointsAt x are the
points γ x tᵢ surrounding g x for parameters tᵢ : ℝ, i = 0, 1, ..., dim F (defined
by γ.surroundingParametersAt x).
Equations
- γ.surroundingPointsAt x = ↑(γ.toFun x) ∘ γ.surroundingParametersAt x
Instances For
Given γ : SmoothSurroundingFamily g and x : E, γ.surrounding_weights_at x are the
barycentric coordinates of g x wrt to the points γ x tᵢ, for parameters tᵢ : ℝ,
i = 0, 1, ..., dim F (defined by γ.surroundingParametersAt x).
Equations
Instances For
Note that we are mollifying the loop γ y at the surrounding parameters for γ x.
Equations
- γ.approxSurroundingPointsAt x y n i = (γ.toFun y).mollify n (γ.surroundingParametersAt x i)
Instances For
The key property from which it should be easy to construct localCenteringDensity,
localCenteringDensityNhd etc below.
This is an auxiliary definition to help construct centeringDensity below.
Given x : E, it represents a smooth probability distribution on the circle with the property that:
∫ s in 0..1, γ.localCenteringDensity x y s • γ y s = g y
for all y in a neighbourhood of x (see localCenteringDensity_average below).
Equations
- One or more equations did not get rendered due to their size.
Instances For
This is an auxiliary definition to help construct centeringDensity below.
Equations
- One or more equations did not get rendered due to their size.
Instances For
This is an auxiliary definition to help construct centeringDensity below.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Given γ : SmoothSurroundingFamily g, together with a point x : E and a map f : ℝ → ℝ,
γ.is_centeringDensity x f is the proposition that f is periodic, strictly positive, and
has integral one and that the average of γₓ with respect to the measure that f defines on
the circle is g x.
The continuity assumption is just a legacy convenience and should be dropped.
- Periodic : Function.Periodic f 1
- Continuous : _root_.Continuous f
Instances For
This the key construction. It represents a smooth probability distribution on the circle with
the property that:
∫ s in 0..1, γ.centeringDensity x s • γ x s = g x
for all x : E (see centeringDensity_average below).
Equations
Instances For
Given γ : SmoothSurroundingFamily g, x ↦ γ.reparametrize x is a smooth family of
diffeomorphisms of the circle such that reparametrizing γₓ by γ.reparametrize x gives a loop
with average g x.
This is the key construction and the main "output" of the reparametrization lemma.
Equations
- One or more equations did not get rendered due to their size.