OAI/MeasureTheory/Falconer/Measures/ChartDensityEstimate.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Nonstationary chart integration with the surface density

The surface Jacobian is included in the differentiated amplitude. Its derivatives are bounded on the fixed chart, uniformly in the remaining coordinate parameters.

  1. theorem OAI.Falconer.density_tangent_chart_nonstationary line 19