OAI/Analysis/Conductivity/Sources/CopiedEnergyAlgebra.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ScalarConductivity.BoundedRootSources.coefficient line 16
  2. lemma OAI.ScalarConductivity.BoundedRootSources.coefficient_measurable line 17
  3. lemma OAI.ScalarConductivity.BoundedRootSources.coefficient_bound line 18
  4. def OAI.ScalarConductivity.BoundedRootSources.form line 23
  5. lemma OAI.ScalarConductivity.BoundedRootSources.form_apply line 26
  6. lemma OAI.ScalarConductivity.BoundedRootSources.form_symm line 27
  7. lemma OAI.ScalarConductivity.BoundedRootSources.root_support line 29
  8. def OAI.ScalarConductivity.BoundedRootSources.root line 31
  9. lemma OAI.ScalarConductivity.BoundedRootSources.form_root line 32
  10. lemma OAI.ScalarConductivity.BoundedRootSources.form_child line 36
  11. lemma OAI.ScalarConductivity.BoundedRootSources.form_average line 40
  12. lemma OAI.ScalarConductivity.BoundedRootSources.form_difference line 51
  13. def OAI.ScalarConductivity.BoundedRootSources.sourceHarmonic line 62
  14. lemma OAI.ScalarConductivity.BoundedRootSources.harmonic_sourceHarmonic line 63
  15. lemma OAI.ScalarConductivity.BoundedRootSources.sourceHarmonic_child line 67
  16. lemma OAI.ScalarConductivity.BoundedRootSources.sourceHarmonic_mean line 73
  17. lemma OAI.ScalarConductivity.weakValue_bound_add line 91
  18. lemma OAI.ScalarConductivity.weakValue_bound_smul line 99
  19. def OAI.ScalarConductivity.sourceAveragePullIter line 106
  20. lemma OAI.ScalarConductivity.sourceAveragePullIter_succ line 110
  21. def OAI.ScalarConductivity.BoundedRootSources.seed line 122
  22. def OAI.ScalarConductivity.BoundedRootSources.initial line 123
  23. lemma OAI.ScalarConductivity.BoundedRootSources.seed_support line 125
  24. lemma OAI.ScalarConductivity.BoundedRootSources.initial_support line 127
  25. lemma OAI.ScalarConductivity.BoundedRootSources.seed_bounded line 132
  26. lemma OAI.ScalarConductivity.BoundedRootSources.initial_bounded line 136
  27. lemma OAI.ScalarConductivity.BoundedRootSources.form_seed line 143
  28. lemma OAI.ScalarConductivity.BoundedRootSources.form_initial line 155
  29. lemma OAI.ScalarConductivity.BoundedRootSources.form_averageIter line 166
  30. def OAI.ScalarConductivity.BoundedRootSources.finiteSource line 175
  31. lemma OAI.ScalarConductivity.BoundedRootSources.finiteSource_support line 178
  32. lemma OAI.ScalarConductivity.BoundedRootSources.form_finiteSource line 184
  33. theorem OAI.ScalarConductivity.BoundedRootSources.nested_source_limit_exists line 199