OAI/Analysis/Conductivity/Variational/CompactRegularCorrection.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ScalarConductivity.cubePartial_smooth line 11
  2. lemma OAI.ScalarConductivity.cubePartial_add line 15
  3. lemma OAI.ScalarConductivity.cubePartial_sub line 19
  4. lemma OAI.ScalarConductivity.cubePartial_neg line 23
  5. lemma OAI.ScalarConductivity.cubePartial_commute line 27
  6. lemma OAI.ScalarConductivity.cubePartial_compact line 36
  7. lemma OAI.ScalarConductivity.cube_integration_by_parts line 39
  8. lemma OAI.ScalarConductivity.compact_divergence line 52
  9. lemma OAI.ScalarConductivity.cubePartial_fst_fst line 73
  10. lemma OAI.ScalarConductivity.cubePartial_snd_fst line 79
  11. lemma OAI.ScalarConductivity.cube_coordinate_divergence_moment line 85
  12. theorem OAI.ScalarConductivity.compact_regular_coordinate_correction line 109