OAI/NumberTheory/JointDickman/Analysis/FractionalPowerBoundary.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The two boundary values on the fractional-power branch cut

  1. def OAI.JointDickman.fractionalPowerKernel line 11
  2. theorem OAI.JointDickman.fractionalPower_boundary_value line 14
  3. theorem OAI.JointDickman.fractionalPower_upper_cut line 22
  4. theorem OAI.JointDickman.fractionalPower_lower_cut line 33
  5. theorem OAI.JointDickman.fractionalPower_jump line 47
  6. theorem OAI.JointDickman.fractionalPower_norm line 57
  7. theorem OAI.JointDickman.fractionalPower_horizontal_bound line 63