OAI/Combinatorics/Progressions/Lattices/SpatialAffineFullMass.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.affineFramePolynomial line 15
  2. theorem OAI.Erdos3.affineFramePolynomial_degree line 18
  3. theorem OAI.Erdos3.affineFramePolynomial_support line 27
  4. theorem OAI.Erdos3.affineFramePolynomial_eval line 35
  5. theorem OAI.Erdos3.affineFramePolynomial_map line 41
  6. theorem OAI.Erdos3.PolynomialPatch.LowestLayerModel.exists_freeze_prepared_affine line 60
  7. theorem OAI.Erdos3.RankPreparationLayer.pullback_value line 150
  8. theorem OAI.Erdos3.RankPreparationFamily.pullback_potential line 161
  9. theorem OAI.Erdos3.RankPreparationFamily.pullback_value line 164
  10. theorem OAI.Erdos3.RankPreparationFamily.Sized.pullback line 171
  11. theorem OAI.Erdos3.RankPreparationFamily.PreparedHeights.pullback line 174
  12. theorem OAI.Erdos3.prepared_polynomial_identity_pullback line 181
  13. theorem OAI.Erdos3.affineFramePolynomial_eq_parameter line 191
  14. theorem OAI.Erdos3.integer_affineFramePolynomial_map line 197
  15. theorem OAI.Erdos3.integer_affineFramePolynomial_aeval_degree line 204
  16. theorem OAI.Erdos3.RankPreparationFamily.pullback_affine_identity line 211
  17. theorem OAI.Erdos3.affineFramePolynomial_top_one line 240
  18. theorem OAI.Erdos3.scaleMvPolynomialAxes_affineFrame_top_one line 251
  19. theorem OAI.Erdos3.scaleMvPolynomialAxes_C_mul line 263
  20. theorem OAI.Erdos3.spatialAffineTop_mass_le line 270
  21. theorem OAI.Erdos3.spatialAffineTop_inv_mul_mass_le line 282
  22. theorem OAI.Erdos3.spatialAffineTop_scaled_inv_mul_mass_le line 293
  23. theorem OAI.Erdos3.scaleMvPolynomialAxes_affineFrame_eq_const_add_top line 315
  24. theorem OAI.Erdos3.spatialAffineFull_mass_le line 327
  25. theorem OAI.Erdos3.spatialAffineFull_inv_mul_mass_le line 336
  26. theorem OAI.Erdos3.spatialAffineFull_scaled_inv_mul_mass_le line 350