OAI/Analysis/LipschitzHilbert/Estimates/PlanarHorizontalRescale.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Normalize a top's horizontal length while retaining its packet lattice and its original analyzing coefficients.

  1. theorem OAI.LipschitzHilbert.lineEnvelope_horizontalDilation line 15
  2. def OAI.LipschitzHilbert.PlanarPacketFamily.horizontalRescale line 25
  3. theorem OAI.LipschitzHilbert.PlanarPacketFamily.horizontalRescale_length line 50
  4. theorem OAI.LipschitzHilbert.PlanarPacketFamily.horizontalRescale_centerX line 55
  5. theorem OAI.LipschitzHilbert.PlanarPacketFamily.horizontalRescale_centerZ line 62
  6. theorem OAI.LipschitzHilbert.PlanarPacketFamily.horizontalRescale_wave line 66
  7. theorem OAI.LipschitzHilbert.PlanarPacketFamily.horizontalRescale_mainCoefficient line 70