OAI/Analysis/Conductivity/Branching/AlignedEndingRegularity.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ScalarConductivity.permutedDilationEquiv line 14
  2. lemma OAI.ScalarConductivity.permutedDilationEquiv_apply line 18
  3. def OAI.ScalarConductivity.axialPairScaling line 24
  4. lemma OAI.ScalarConductivity.axialPairScaling_apply line 28
  5. lemma OAI.ScalarConductivity.alignedEnding_axialPair line 31
  6. def OAI.ScalarConductivity.alignedEndingSymmetricTensor line 38
  7. lemma OAI.ScalarConductivity.RegularPatch.alignedEnding line 41
  8. theorem OAI.ScalarConductivity.alignedEnding_regularRegion_ae line 69
  9. lemma OAI.ScalarConductivity.alignedEnding_regularRegion_conull line 85
  10. def OAI.ScalarConductivity.delayedEndingValue line 105
  11. lemma OAI.ScalarConductivity.delayedEndingValue_C2 line 108
  12. lemma OAI.ScalarConductivity.delayedEndingValue_initial_of_bound line 112
  13. lemma OAI.ScalarConductivity.delayedEndingValue_initial line 121
  14. lemma OAI.ScalarConductivity.delayedEndingValue_terminal line 128
  15. lemma OAI.ScalarConductivity.delayedEndingValue_periodic line 133
  16. def OAI.ScalarConductivity.matchedEndingPair line 140
  17. lemma OAI.ScalarConductivity.matchedEndingPair_C2 line 143
  18. lemma OAI.ScalarConductivity.matchedEndingPair_periodic line 157
  19. lemma OAI.ScalarConductivity.matchedEndingPair_terminal line 164