OAI/Analysis/JiangSu/DimensionDrop/DimensionDropPolynomialNorm.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.DimensionDropModel.Gen line 19
  2. def OAI.DimensionDropModel.values line 20
  3. def OAI.DimensionDropModel.lowerValues line 23
  4. def OAI.DimensionDropModel.upperValues line 26
  5. lemma OAI.DimensionDropModel.amplify_lower line 29
  6. lemma OAI.DimensionDropModel.embed_upper line 33
  7. abbrev OAI.DimensionDropModel.Interval line 37
  8. lemma OAI.DimensionDropModel.continuous_values line 38
  9. lemma OAI.DimensionDropModel.Term.continuous_eval line 40
  10. def OAI.DimensionDropModel.realization line 48
  11. def OAI.DimensionDropRelations.Witness.interpret line 59
  12. lemma OAI.DimensionDropRelations.Witness.lower_interpret line 62
  13. lemma OAI.DimensionDropRelations.Witness.upper_interpret line 66
  14. lemma OAI.DimensionDropRelations.Witness.interior_interpret line 71
  15. theorem OAI.DimensionDropRelations.Witness.scalar_polynomial_norm line 77
  16. theorem OAI.DimensionDropRelations.Witness.polynomial_norm_of_generated line 102