OAI/Analysis/Conductivity/Variational/CrossingHxx.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ScalarConductivity.crossingHxx line 25
  2. def OAI.ScalarConductivity.crossingHxy line 29
  3. def OAI.ScalarConductivity.crossingFluxX line 32
  4. def OAI.ScalarConductivity.crossingFluxY line 36
  5. lemma OAI.ScalarConductivity.crossingFluxX_simplify line 39
  6. lemma OAI.ScalarConductivity.crossingFluxY_simplify line 46
  7. theorem OAI.ScalarConductivity.crossing_divergence line 52
  8. lemma OAI.ScalarConductivity.crossing_coefficients_small line 73
  9. lemma OAI.ScalarConductivity.crossing_quadratic_ellipticity line 110
  10. def OAI.ScalarConductivity.pushGradient line 143
  11. def OAI.ScalarConductivity.pushFlux line 146
  12. lemma OAI.ScalarConductivity.pushGradient_leftInverse line 149
  13. lemma OAI.ScalarConductivity.pushGradient_rank line 155
  14. lemma OAI.ScalarConductivity.push_pairing line 164
  15. lemma OAI.ScalarConductivity.pushFlux_constitutive line 175
  16. lemma OAI.ScalarConductivity.symmetric_gram_pairing line 181
  17. def OAI.ScalarConductivity.repairPushed line 188
  18. lemma OAI.ScalarConductivity.repairPushed_mul line 192
  19. lemma OAI.ScalarConductivity.repairPushed_exact line 202
  20. lemma OAI.ScalarConductivity.continuousAt_matrixInverse line 209
  21. lemma OAI.ScalarConductivity.continuousAt_pushGradient line 216
  22. lemma OAI.ScalarConductivity.continuousAt_pushFlux line 224
  23. lemma OAI.ScalarConductivity.continuousAt_repairPushed line 232