OAI/Analysis/Conductivity/Fourier/ModeConnector.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ScalarConductivity.connectorRate line 10
  2. def OAI.ScalarConductivity.connectorProfile line 13
  3. lemma OAI.ScalarConductivity.connectorRate_smooth line 16
  4. lemma OAI.ScalarConductivity.connectorRate_bounds line 20
  5. lemma OAI.ScalarConductivity.connectorRate_left line 25
  6. lemma OAI.ScalarConductivity.connectorRate_right line 30
  7. lemma OAI.ScalarConductivity.connectorRate_hasDerivAt line 36
  8. lemma OAI.ScalarConductivity.connectorRate_derivative_bounds line 47
  9. lemma OAI.ScalarConductivity.connectorProfile_pos line 63
  10. lemma OAI.ScalarConductivity.connectorProfile_smooth line 64
  11. lemma OAI.ScalarConductivity.connectorProfile_hasDerivAt line 68
  12. lemma OAI.ScalarConductivity.connectorProfile_second line 78
  13. def OAI.ScalarConductivity.connectorAngular line 90
  14. lemma OAI.ScalarConductivity.connectorAngular_formula line 93
  15. lemma OAI.ScalarConductivity.connectorAngular_bounds line 98
  16. lemma OAI.ScalarConductivity.connectorProfile_zero line 106
  17. lemma OAI.ScalarConductivity.connector_integral_pos line 109
  18. lemma OAI.ScalarConductivity.connectorProfile_le_one line 120