OAI/MeasureTheory/Falconer/Estimates/PacketResidualRows.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Raw residual form of the packet row lift. This is stable under the actual affine centering, whose residual identity is exact.

  1. theorem OAI.Falconer.packet_raw_common_row line 11
  2. theorem OAI.Falconer.packet_row_pencil_lift_residual line 38