OAI/Analysis/PlanarPacking/MomentRecurrence.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Recurrences for the direct and transformed Gaussian moments

  1. lemma OAI.SharpPlanar.direct_factor_step line 10
  2. lemma OAI.SharpPlanar.transformed_factor_step line 16
  3. def OAI.SharpPlanar.IntegerIntervals.CBox.conj line 23
  4. lemma OAI.SharpPlanar.IntegerIntervals.CBox.conj_contains line 24
  5. lemma OAI.SharpPlanar.direct_factor_zero_contains line 26
  6. lemma OAI.SharpPlanar.transformed_factor_zero_contains line 35
  7. lemma OAI.SharpPlanar.factor_step_contains line 40