OAI/Analysis/LipschitzHilbert/Geometry/SlopeDirection.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Quantitative normalization of slope directions and the exact uncertainty-arc condition needed by the Lacey--Li rectangle input.

  1. def OAI.LipschitzHilbert.slopeDirection line 14
  2. theorem OAI.LipschitzHilbert.slopeDirection_norm line 16
  3. theorem OAI.LipschitzHilbert.slopeDirection_coordinates line 19
  4. theorem OAI.LipschitzHilbert.slopeDirection_inner line 24
  5. theorem OAI.LipschitzHilbert.arctan_lipschitz line 32
  6. theorem OAI.LipschitzHilbert.arctan_sub_le line 41
  7. theorem OAI.LipschitzHilbert.plane_norm_le_coordinate_sum line 44

    Distinct definitions of this name: OAI/Analysis/LipschitzHilbert/Geometry/DilatedRectangleInterior.lean:13 (same statement text; different proof or body). Qualify references as OAI.LipschitzHilbert.plane_norm_le_coordinate_sum@path.

  8. theorem OAI.LipschitzHilbert.slopeDirection_lipschitz line 52
  9. theorem OAI.LipschitzHilbert.cos_le_inner_slopeDirection line 67