OAI/NumberTheory/JointDickman.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.JointDickman.main_results_of_rational_fixedScale line 8

   Source documentation

   A rational fixed-scale joint law implies the moving joint law and both order densities.

   theorem main_results_of_rational_fixedScale (h : RationalFixedScaleLaw) :
       JointDickmanLaw ∧ IncreasingOrderLaw ∧ DecreasingOrderLaw := by
   …

   Mentions: OAI.JointDickman.RationalFixedScaleLaw, OAI.JointDickman.JointDickmanLaw, OAI.JointDickman.IncreasingOrderLaw, OAI.JointDickman.DecreasingOrderLaw