OAI/Combinatorics/Progressions/Probability/AllocatedMixedLiftNormalizedMass.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.scaleMvPolynomialAxes_neg line 11
  2. theorem OAI.Erdos3.normalizedPolynomialMass_neg line 16
  3. theorem OAI.Erdos3.normalizedAxes_homogeneousComponent_commute line 20
  4. theorem OAI.Erdos3.normalizedMass_homogeneousComponent_projection_le line 29
  5. theorem OAI.Erdos3.normalizedMass_neg_weightedHomogeneousComponent_le line 45
  6. theorem OAI.Erdos3.mixedLiftPolynomial_scaled_coefficients line 66
  7. theorem OAI.Erdos3.mixedLiftPolynomial_scaled_mass line 83
  8. theorem OAI.Erdos3.VectorPolynomial.allocatedLayerSupported_normalized_mass line 122
  9. theorem OAI.Erdos3.VectorPolynomial.allocatedLayerSupported_normalized_top_mass line 153
  10. theorem OAI.Erdos3.VectorPolynomial.allocatedLayerSupported_normalized_mass_uniform line 166