OAI/NumberTheory/JointDickman/Counting/LagEnvelopeMoments.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Row moments of the deterministic singular-factor envelope

  1. def OAI.JointDickman.lagEnvelope line 11
  2. theorem OAI.JointDickman.lagEnvelope_nonneg line 14
  3. theorem OAI.JointDickman.lagEnvelope_row_sum line 22
  4. theorem OAI.JointDickman.lagEnvelope_row_square_sum line 34
  5. theorem OAI.JointDickman.lagEnvelope_row_mean line 46
  6. theorem OAI.JointDickman.lagEnvelope_row_square_mass line 66