OAI/Analysis/Conductivity/Variational/ScaledSmoothSeries.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ScalarConductivity.compact_iteratedFDeriv_bound line 12
  2. lemma OAI.ScalarConductivity.sin_cos_iterated_bound line 21
  3. lemma OAI.ScalarConductivity.linear_comp_iterated_bound line 28
  4. def OAI.ScalarConductivity.cascadeMother line 37
  5. lemma OAI.ScalarConductivity.cascadeMother_smooth line 40
  6. lemma OAI.ScalarConductivity.cascadeMother_iterated_bound line 45
  7. lemma OAI.ScalarConductivity.scaled_iterated_bound line 75
  8. theorem OAI.ScalarConductivity.geometric_scaled_C2 line 88
  9. def OAI.ScalarConductivity.BoundedSmooth line 116
  10. lemma OAI.ScalarConductivity.BoundedSmooth.of_compact line 119
  11. lemma OAI.ScalarConductivity.BoundedSmooth.add line 123
  12. lemma OAI.ScalarConductivity.BoundedSmooth.smul line 135
  13. lemma OAI.ScalarConductivity.BoundedSmooth.sub line 144
  14. lemma OAI.ScalarConductivity.BoundedSmooth.mul line 149
  15. lemma OAI.ScalarConductivity.BoundedSmooth.comp_linear line 163
  16. lemma OAI.ScalarConductivity.BoundedSmooth.translate line 170
  17. lemma OAI.ScalarConductivity.sin_boundedSmooth line 178
  18. lemma OAI.ScalarConductivity.cos_boundedSmooth line 181