OAI/Analysis/RieszRectifiability/Foundations/SeparatedParameterPatchGluing.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Gluing separated parameter patches

Separation of the parameter centers and control of the image centers give a uniform cross-patch Lipschitz estimate. The glued map extends to a parameter ball, whose image covers all patches with an explicit Lipschitz constant.

  1. def OAI.RieszRectifiability.separatedPatchGluingConstant line 21
  2. theorem OAI.RieszRectifiability.separated_parameter_patch_cross_dist_le line 24
  3. theorem OAI.RieszRectifiability.exists_ball_lipschitz_cover_of_separated_parameter_patches line 73