OAI/Analysis/Conductivity/Variational/SmoothSupportedAdd.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.ScalarConductivity.smooth_supported_add line 14
  2. theorem OAI.ScalarConductivity.smooth_supported_smul line 20
  3. theorem OAI.ScalarConductivity.smooth_supported_neg line 25
  4. theorem OAI.ScalarConductivity.smooth_supported_sub line 31
  5. theorem OAI.ScalarConductivity.localizedFirstPotential_support line 37
  6. theorem OAI.ScalarConductivity.localizedSecondPotential_support line 44
  7. theorem OAI.ScalarConductivity.airyFlux_support line 51
  8. theorem OAI.ScalarConductivity.transverseFlux_support line 66
  9. theorem OAI.ScalarConductivity.localizedTwoFlux_support line 80
  10. theorem OAI.ScalarConductivity.exists_localized_two_flux line 95
  11. def OAI.ScalarConductivity.lineShift line 118
  12. theorem OAI.ScalarConductivity.lineShift_bijective line 121
  13. def OAI.ScalarConductivity.rankOneEquiv line 170
  14. theorem OAI.ScalarConductivity.rankOneEquiv_apply line 201
  15. theorem OAI.ScalarConductivity.exists_smooth_lineShift_inverse line 205