Chart cutoffs on a Riemannian manifold #
To localize an integral estimate from the model space to a manifold with a continuous Riemannian
metric, one reads a function u in a chart around a point c and cuts it off with a bump function
b centred at the chart image of c. This file supplies the comparisons that such a localization
needs:
- near the chart image of
cthere is a coordinate ball on which the coordinate derivative of every function is bounded by a fixed multiple of the length of its gradient, and the chart volume density is comparable to its value atc(TauCeti.Manifold.exists_ball_norm_fderiv_le_and_chartVolumeDensity_mem_Ioo); - on such a ball,
∫ ‖D(b · u)‖ ^ pwith respect to Lebesgue measure on the model space is bounded by a constant multiple ofC₁ ^ p ∫ |∇u| ^ p dV + G ^ p ∫ |u| ^ p dV, whereC₁is the derivative comparison constant andGbounds the derivative of the bump (ContDiffBump.lintegral_enorm_fderiv_mul_comp_extChartAt_symm_rpow_le), so itsLᵖnorm is at most a constant times‖∇u‖_{Lᵖ} + ‖u‖_{Lᵖ}(ContDiffBump.eLpNorm_fderiv_mul_comp_extChartAt_symm_le); - where the bump is
1and the chart density is at mostm, an integral ofF ∘ uover the chart preimage of a ball is bounded bymtimes the integral ofF (b · u)over the ball (ContDiffBump.setLIntegral_inter_preimage_le_mul_setLIntegral_mul_comp_extChartAt_symm), so theL^{p'}norm ofuover that chart preimage is at mostm ^ (1 / p')times the flatL^{p'}norm ofb · u ∘ φ.symm(ContDiffBump.eLpNorm_restrict_inter_preimage_ball_le_mul_eLpNorm_mul_comp_extChartAt_symm).
They are used for the Trudinger and Sobolev inequalities on a closed Riemannian manifold.
Around the chart image of c there is a coordinate ball inside the chart target on which the
coordinate derivative of every function is bounded by a fixed multiple of the length of its
gradient, and the chart density lies between half and twice its value at c.
The derivative of a chart cutoff in Lᵖ. Let 1 ≤ p. On a coordinate ball where the
chart derivative is bounded by C₁ times the gradient and the chart density is at least m, the
cut-off coordinate expression of a C¹ function u has ∫ ‖D(b · u)‖ ^ p bounded by
2 ^ (p - 1) m⁻¹ (C₁ ^ p ∫ |∇u| ^ p dV + G ^ p ∫ |u| ^ p dV), where G bounds the derivative of
the bump b.
The derivative of a chart cutoff in Lᵖ, in norm form. Let 1 ≤ p. On a coordinate ball
where the chart derivative is bounded by C₁ times the gradient and the chart density is at least
m, the cut-off coordinate expression of a C¹ function u has
‖D(b · u)‖_{Lᵖ} ≤ 2 (C₁ + G) m^{-1/p} (‖∇u‖_{Lᵖ} + ‖u‖_{Lᵖ}), where G bounds the derivative of
the bump b.
Reading a chart cutoff back on M. If the chart density is at most m on the ball of
radius b.rIn, where the bump is 1, then for every F : ℝ → ℝ≥0∞ the integral of F ∘ u over
the chart preimage of that ball is at most m times the integral of F (b · u) over the ball, with
respect to Lebesgue measure on the model space.
The L^{p'} norm of u over the chart preimage of the ball of radius b.rIn is at most
m ^ (1 / p') times the flat L^{p'} norm of the cut-off function b * (u ∘ φ.symm), where m
bounds the chart volume density on that ball.