OAI/MeasureTheory/Falconer/Shells/RotatedInverseShell.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The full rotated inverse bounded by the original descriptor state

  1. abbrev OAI.Falconer.RootInverseFamilyIndex line 13
  2. def OAI.Falconer.rotatedInverseShellCost line 16
  3. def OAI.Falconer.rotatedInverseNormalizedSum line 23
  4. theorem OAI.Falconer.rotated_inverse_family_shell_integrable line 41
  5. theorem OAI.Falconer.rotated_inverse_family_shell_le line 101