OAI/Analysis/Conductivity/Variational/DirectionCalculus.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ScalarConductivity.direction_const line 14
  2. lemma OAI.ScalarConductivity.direction_add line 16
  3. lemma OAI.ScalarConductivity.direction_sub line 19
  4. lemma OAI.ScalarConductivity.direction_mul line 22
  5. lemma OAI.ScalarConductivity.direction_const_mul line 26
  6. lemma OAI.ScalarConductivity.direction_comp_real line 29
  7. lemma OAI.ScalarConductivity.direction_congr_nhds line 37
  8. lemma OAI.ScalarConductivity.direction_coord line 41
  9. lemma OAI.ScalarConductivity.direction_scalar_coord line 49
  10. def OAI.ScalarConductivity.wedgePotential line 55
  11. lemma OAI.ScalarConductivity.wedgePotential_flux line 58
  12. lemma OAI.ScalarConductivity.direction_dilation line 75
  13. lemma OAI.ScalarConductivity.direction_sin_coord line 89
  14. lemma OAI.ScalarConductivity.direction_cos_coord line 95
  15. lemma OAI.ScalarConductivity.direction_scalar_sin line 102
  16. def OAI.ScalarConductivity.angularStream line 109
  17. lemma OAI.ScalarConductivity.angularStream_diff line 113
  18. lemma OAI.ScalarConductivity.angularStream_b line 118
  19. lemma OAI.ScalarConductivity.angularStream_a line 139