OAI/Analysis/CircleDomains/Sobolev/NormalizedCircleEnergy.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Energy transport for circle models fixing infinity

Fixing infinity eliminates the exceptional target point from the finite chart. Thus the change-of-variables formula applies on every measurable source set in the finite chart, including the whole localized tail.

  1. theorem OAI.CircleDomainRigidity.integral_filled_circleEnergy_normalized_sphere_map line 23