OAI/Analysis/Conductivity/Branching/ChildInverse.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ScalarConductivity.sourceChildInverse_map_volume line 13
  2. lemma OAI.ScalarConductivity.sourceChildInverse_quasi line 26
  3. def OAI.ScalarConductivity.sourceChildPushforwardCLM line 34
  4. lemma OAI.ScalarConductivity.sourceChildPushforwardCLM_ae line 39
  5. lemma OAI.ScalarConductivity.sourceChildInverse_contDiff line 43
  6. def OAI.ScalarConductivity.sourceChildInverseDerivative line 50
  7. lemma OAI.ScalarConductivity.sourceChildInverseDerivative_apply line 53
  8. lemma OAI.ScalarConductivity.sourceChildInverse_hasFDeriv line 59
  9. lemma OAI.ScalarConductivity.sourceChildInverse_single line 70
  10. lemma OAI.ScalarConductivity.sourceChild_euclidean_norm line 79
  11. def OAI.ScalarConductivity.sourceChildEuclidean line 97
  12. lemma OAI.ScalarConductivity.sourceChildEuclidean_apply line 101
  13. lemma OAI.ScalarConductivity.sourceChildEuclidean_symm_apply line 104
  14. lemma OAI.ScalarConductivity.sourceChildEuclidean_symm_contDiff line 107
  15. lemma OAI.ScalarConductivity.sourceChildEuclidean_ball line 112
  16. lemma OAI.ScalarConductivity.sourceChildEuclidean_comp_support line 124