OAI/Analysis/Conductivity/Sources/BranchCombine.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ScalarConductivity.source_child_push_inner_zero line 14
  2. def OAI.ScalarConductivity.sourceBranchCombine line 34
  3. lemma OAI.ScalarConductivity.sourceBranchCombine_support line 37
  4. lemma OAI.ScalarConductivity.norm_smul_sq_real line 42
  5. lemma OAI.ScalarConductivity.sourceBranchCombine_energy line 46
  6. lemma OAI.ScalarConductivity.sourceBranchCombine_bound line 65
  7. def OAI.ScalarConductivity.sourceAveragePush line 91
  8. def OAI.ScalarConductivity.sourceDifferencePush line 94
  9. def OAI.ScalarConductivity.sourceAveragePull line 97
  10. def OAI.ScalarConductivity.sourceDifferencePull line 98
  11. def OAI.ScalarConductivity.sourceRatio line 100
  12. lemma OAI.ScalarConductivity.sourceAveragePush_eq line 102
  13. lemma OAI.ScalarConductivity.sourceDifferencePush_eq line 106
  14. lemma OAI.ScalarConductivity.sourceRatio_pos line 112
  15. lemma OAI.ScalarConductivity.sourceRatio_lt_one line 113
  16. lemma OAI.ScalarConductivity.sourceAveragePush_support line 115
  17. lemma OAI.ScalarConductivity.sourceDifferencePush_support line 120
  18. lemma OAI.ScalarConductivity.sourceAveragePush_energy line 125
  19. lemma OAI.ScalarConductivity.sourceDifferencePush_energy line 131
  20. lemma OAI.ScalarConductivity.sourceAveragePush_bound line 137
  21. lemma OAI.ScalarConductivity.sourceDifferencePush_bound line 143
  22. lemma OAI.ScalarConductivity.sourceSupported_zero line 154
  23. lemma OAI.ScalarConductivity.SourceSupported.sum line 158
  24. lemma OAI.ScalarConductivity.sourceSupported_limit line 167
  25. lemma OAI.ScalarConductivity.sourceSupported_collar line 175
  26. def OAI.ScalarConductivity.sourceAverageIter line 184
  27. lemma OAI.ScalarConductivity.sourceAverageIter_support line 188
  28. lemma OAI.ScalarConductivity.sourceAverageIter_energy line 194
  29. lemma OAI.ScalarConductivity.sourceAverageIter_bound line 203
  30. theorem OAI.ScalarConductivity.sourceAverage_series_exists line 214