OAI/Geometry/NodalSets/Elliptic/ContinuousPolynomialFamily.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Yau.Jets.ContinuousPolyFamily line 11
  2. lemma OAI.Yau.Jets.polynomial_sum_of_support_subset line 15
  3. lemma OAI.Yau.Jets.continuousPolyFamily_of_representation line 21
  4. lemma OAI.Yau.Jets.ContinuousPolyFamily.const line 41
  5. lemma OAI.Yau.Jets.ContinuousPolyFamily.add line 44
  6. lemma OAI.Yau.Jets.ContinuousPolyFamily.smul line 59
  7. lemma OAI.Yau.Jets.ContinuousPolyFamily.sum line 73
  8. lemma OAI.Yau.Jets.ContinuousPolyFamily.linearMap line 83
  9. lemma OAI.Yau.Jets.ContinuousPolyFamily.mul line 94
  10. lemma OAI.Yau.Jets.ContinuousPolyFamily.C line 108
  11. lemma OAI.Yau.Jets.continuousPolyFamily_aeval_fixed line 112
  12. lemma OAI.Yau.Jets.ContinuousPolyFamily.aeval line 120
  13. theorem OAI.Yau.Jets.ContinuousPolyFamily.uniform_derivative_bound line 133