OAI/NumberTheory/CubicMoment/Estimates/HeightWeightedMass.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Positivity transfers the actual full-variance height bound to any finite primary outer set with weight at most one, including μ².

  1. lemma OAI.CubicFirstMoment.finite_weighted_dispersion_le line 12
  2. lemma OAI.CubicFirstMoment.height_finite_weighted_dispersion_le line 49