OAI/Analysis/Conductivity/Flux/LinearFluxWeakTransport.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ScalarConductivity.continuousLinearEquiv_det_ne_zero line 11
  2. lemma OAI.ScalarConductivity.continuousLinearEquiv_quasiMeasurePreserving line 17
  3. lemma OAI.ScalarConductivity.pi_clm_apply_sum line 22
  4. lemma OAI.ScalarConductivity.coordinate_flux_pairing line 31
  5. def OAI.ScalarConductivity.linearFluxPullback line 35
  6. lemma OAI.ScalarConductivity.linearFluxPullback_weak line 38
  7. lemma OAI.ScalarConductivity.continuous_flux_compact_test_integrable line 69
  8. lemma OAI.ScalarConductivity.linearFluxPullback_C1 line 79
  9. lemma OAI.ScalarConductivity.matrix_mul_transpose_col_sum line 91
  10. def OAI.ScalarConductivity.linearColumnsPullback line 98
  11. lemma OAI.ScalarConductivity.linearColumnsPullback_col line 104
  12. lemma OAI.ScalarConductivity.linearColumnsPullback_C1 line 116
  13. lemma OAI.ScalarConductivity.linearColumnsPullback_weak line 125
  14. lemma OAI.ScalarConductivity.linearTensorPullback_C1_representative line 151