OAI/Analysis/Conductivity/Sources/NestedGeometry.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ScalarConductivity.sourceScale line 10
  2. def OAI.ScalarConductivity.sourceOffset line 11
  3. def OAI.ScalarConductivity.sourceLength line 12
  4. def OAI.ScalarConductivity.sourceHole line 13
  5. def OAI.ScalarConductivity.sourceDomain line 15
  6. def OAI.ScalarConductivity.sourceOuterBox line 18
  7. def OAI.ScalarConductivity.sourceSwap line 20
  8. lemma OAI.ScalarConductivity.sourceSwap_apply line 23
  9. def OAI.ScalarConductivity.sourceShift line 29
  10. def OAI.ScalarConductivity.sourceSimilarity line 31
  11. lemma OAI.ScalarConductivity.sourceSimilarity_coord line 41
  12. lemma OAI.ScalarConductivity.sourceSimilarity_dist line 51
  13. lemma OAI.ScalarConductivity.sourceScale_rates line 58
  14. lemma OAI.ScalarConductivity.sourceDomain_isOpen line 61
  15. lemma OAI.ScalarConductivity.sourceOuterBox_isClosed line 69
  16. lemma OAI.ScalarConductivity.sourceDomain_subset_box line 74
  17. lemma OAI.ScalarConductivity.sourceClosure_subset_box line 82
  18. lemma OAI.ScalarConductivity.sourceBox_norm_bound line 85
  19. lemma OAI.ScalarConductivity.sourceClosure_subset_ball line 99
  20. lemma OAI.ScalarConductivity.sourceDomain_isBounded line 103
  21. lemma OAI.ScalarConductivity.sourceClosure_isCompact line 107
  22. lemma OAI.ScalarConductivity.source_children_coords line 110
  23. lemma OAI.ScalarConductivity.source_positive_child_in_parent line 131
  24. lemma OAI.ScalarConductivity.source_negative_child_in_parent line 142
  25. theorem OAI.ScalarConductivity.source_children_compact_inside line 153