OAI/Analysis/Conductivity/Variational/CrossingProfiles.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ScalarConductivity.smooth_deriv_infty line 10
  2. lemma OAI.ScalarConductivity.smoothTransition_flat_left line 15
  3. lemma OAI.ScalarConductivity.smoothTransition_flat_right line 22
  4. lemma OAI.ScalarConductivity.exists_transition_derivative_bound line 29
  5. def OAI.ScalarConductivity.crossingOn line 50
  6. def OAI.ScalarConductivity.crossingOff line 51
  7. def OAI.ScalarConductivity.crossingFirst line 53
  8. def OAI.ScalarConductivity.crossingSecond line 54
  9. lemma OAI.ScalarConductivity.crossingOn_smooth line 56
  10. lemma OAI.ScalarConductivity.crossingOff_smooth line 58
  11. lemma OAI.ScalarConductivity.crossingFirst_smooth line 61
  12. lemma OAI.ScalarConductivity.crossingSecond_smooth line 63
  13. lemma OAI.ScalarConductivity.crossingOn_bounds line 66
  14. lemma OAI.ScalarConductivity.crossingOff_bounds line 68
  15. lemma OAI.ScalarConductivity.crossingOn_eq_zero line 73
  16. lemma OAI.ScalarConductivity.crossingOn_eq_one line 78
  17. lemma OAI.ScalarConductivity.crossingOff_eq_one line 83
  18. lemma OAI.ScalarConductivity.crossingOff_eq_zero line 87
  19. lemma OAI.ScalarConductivity.crossingOn_hasDerivAt line 92
  20. lemma OAI.ScalarConductivity.crossingOff_hasDerivAt line 99
  21. lemma OAI.ScalarConductivity.deriv_crossingOn line 107
  22. lemma OAI.ScalarConductivity.deriv_crossingOff line 110
  23. lemma OAI.ScalarConductivity.crossingOn_second line 114
  24. lemma OAI.ScalarConductivity.crossingOff_second line 121