OAI/Analysis/LipschitzHilbert/Geometry/DirectionDilation.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Reciprocal-Lipschitz dilation and its exact L2 scaling in the plane.

  1. theorem OAI.LipschitzHilbert.memLp_two_comp_smul_iff line 13
  2. theorem OAI.LipschitzHilbert.toLp_norm_comp_smul line 27
  3. def OAI.LipschitzHilbert.rescaleSchwartz line 39
  4. theorem OAI.LipschitzHilbert.rescaleSchwartz_apply line 43
  5. theorem OAI.LipschitzHilbert.rescaleSchwartz_norm line 46
  6. theorem OAI.LipschitzHilbert.rescaleField_lipschitz_small line 57
  7. theorem OAI.LipschitzHilbert.shortTransform_dilation line 71