OAI/Analysis/Conductivity/Branching/Ending.lean

GitHub source file

50 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ScalarConductivity.initialConnectorRate line 13
  2. def OAI.ScalarConductivity.initialConnectorProfile line 16
  3. lemma OAI.ScalarConductivity.initialConnectorRate_smooth line 19
  4. lemma OAI.ScalarConductivity.initialConnectorRate_bounds line 24
  5. lemma OAI.ScalarConductivity.initialConnectorRate_left line 39
  6. lemma OAI.ScalarConductivity.initialConnectorRate_right line 44
  7. lemma OAI.ScalarConductivity.initialConnectorRate_deriv line 50
  8. lemma OAI.ScalarConductivity.exists_initialConnector_length line 60
  9. lemma OAI.ScalarConductivity.initialConnectorProfile_smooth line 78
  10. lemma OAI.ScalarConductivity.initialConnectorProfile_pos line 83
  11. lemma OAI.ScalarConductivity.initialConnectorProfile_hasDerivAt line 85
  12. lemma OAI.ScalarConductivity.initialConnectorProfile_second line 95
  13. def OAI.ScalarConductivity.initialConnectorAngular line 109
  14. lemma OAI.ScalarConductivity.initialConnectorAngular_smooth line 112
  15. lemma OAI.ScalarConductivity.initialConnectorAngular_bounds line 117
  16. lemma OAI.ScalarConductivity.initialConnectorProfile_left line 129
  17. lemma OAI.ScalarConductivity.initialConnectorProfile_right line 142
  18. lemma OAI.ScalarConductivity.initialConnector_constitution line 160
  19. lemma OAI.ScalarConductivity.cascadeProfile_near_start line 173
  20. lemma OAI.ScalarConductivity.cascadeProfile_deriv_near_start line 180
  21. lemma OAI.ScalarConductivity.cascadePhase_inactive_start line 191
  22. lemma OAI.ScalarConductivity.cascadeValue_near_start line 202
  23. lemma OAI.ScalarConductivity.cascadePotential_near_start line 214
  24. lemma OAI.ScalarConductivity.contDiff_axial_paste line 258
  25. lemma OAI.ScalarConductivity.axial_paste_eventually_left line 282
  26. lemma OAI.ScalarConductivity.axial_paste_eventually_right line 288
  27. def OAI.ScalarConductivity.finiteEndingValue line 299
  28. def OAI.ScalarConductivity.finiteEndingPotential line 304
  29. lemma OAI.ScalarConductivity.finiteEnding_value_overlap line 309
  30. lemma OAI.ScalarConductivity.finiteEnding_potential_overlap line 324
  31. lemma OAI.ScalarConductivity.finiteEndingValue_C2 line 342
  32. lemma OAI.ScalarConductivity.finiteEndingPotential_C2 line 352
  33. lemma OAI.ScalarConductivity.finiteEndingPotential_antisymm line 368
  34. lemma OAI.ScalarConductivity.finiteEndingValue_initial line 377
  35. lemma OAI.ScalarConductivity.finiteEndingValue_terminal line 382
  36. def OAI.ScalarConductivity.finiteEndingTensor line 396
  37. lemma OAI.ScalarConductivity.direction_translate line 400
  38. lemma OAI.ScalarConductivity.potentialCurl_translate line 404
  39. lemma OAI.ScalarConductivity.finiteEndingTensor_measurable line 409
  40. lemma OAI.ScalarConductivity.finiteEndingTensor_symm line 422
  41. lemma OAI.ScalarConductivity.finiteEndingTensor_normal line 429
  42. lemma OAI.ScalarConductivity.finiteEnding_constitution_left line 436
  43. lemma OAI.ScalarConductivity.finiteEnding_constitution_right line 452
  44. lemma OAI.ScalarConductivity.finiteEnding_constitution_ae line 478
  45. lemma OAI.ScalarConductivity.finiteEndingFlux_C1 line 493
  46. lemma OAI.ScalarConductivity.finiteEndingFlux_divergence line 499
  47. theorem OAI.ScalarConductivity.finiteEnding_weak_equation line 504
  48. lemma OAI.ScalarConductivity.pureModeTensor_general_bounds line 535
  49. theorem OAI.ScalarConductivity.exists_finiteEnding_parameters line 545
  50. theorem OAI.ScalarConductivity.positive_rate_finite_ending line 570