OAI/NumberTheory/JointDickman/Analysis/FractionalPowerHorizontal.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Horizontal approach to the fractional-power cut and its integrable majorant

  1. theorem OAI.JointDickman.fractionalPower_upper_horizontal line 14
  2. theorem OAI.JointDickman.fractionalPower_lower_horizontal line 28
  3. theorem OAI.JointDickman.fractionalPower_positive line 42
  4. theorem OAI.JointDickman.fractionalPower_continuousAt_positive line 49
  5. theorem OAI.JointDickman.integrable_abs_rpow_on_bounded_interval line 55