OAI/Analysis/Conductivity/Variational/SynchronizedChartWaves.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.ScalarConductivity.exists_synchronized_chart_waves line 29
  2. abbrev OAI.ScalarConductivity.Coord3 line 114
  3. def OAI.ScalarConductivity.operatorMatrix line 116
  4. lemma OAI.ScalarConductivity.operatorMatrix_norm_le line 120
  5. lemma OAI.ScalarConductivity.operatorMatrix_sub line 127
  6. lemma OAI.ScalarConductivity.operatorMatrix_comp line 132
  7. lemma OAI.ScalarConductivity.operatorMatrix_id line 138
  8. lemma OAI.ScalarConductivity.operatorMatrix_det line 141
  9. lemma OAI.ScalarConductivity.operatorMatrix_mulVec line 144
  10. lemma OAI.ScalarConductivity.operatorMatrix_continuous line 148
  11. lemma OAI.ScalarConductivity.columns_norm_lt line 154
  12. lemma OAI.ScalarConductivity.operatorMatrix_inverse_fderiv line 160
  13. lemma OAI.ScalarConductivity.gradientColumns_recomposition line 168
  14. lemma OAI.ScalarConductivity.piolaFlux_columns line 178