OAI/Analysis/Conductivity/Variational/PreliminaryQ.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ScalarConductivity.preliminaryQ line 13
  2. def OAI.ScalarConductivity.preliminaryB line 15
  3. lemma OAI.ScalarConductivity.harmonic_parent_pos line 18
  4. theorem OAI.ScalarConductivity.preliminary_fractions line 22
  5. theorem OAI.ScalarConductivity.preliminary_matrix_mean line 46
  6. def OAI.ScalarConductivity.stretchedDiagonal line 70
  7. theorem OAI.ScalarConductivity.synchronized_path_is_join line 73
  8. abbrev OAI.ScalarConductivity.Mat3 line 124
  9. def OAI.ScalarConductivity.orthogonalFrames line 126
  10. lemma OAI.ScalarConductivity.isClosed_orthogonalFrames line 128
  11. lemma OAI.ScalarConductivity.orthogonalFrames_entry_bound line 133
  12. lemma OAI.ScalarConductivity.isCompact_orthogonalFrames line 143
  13. lemma OAI.ScalarConductivity.roots_charpoly_diagonal line 149
  14. lemma OAI.ScalarConductivity.same_multiset_permutation line 155
  15. lemma OAI.ScalarConductivity.diagonalizations_permute line 166
  16. lemma OAI.ScalarConductivity.exists_orthogonal_diagonalization line 177
  17. lemma OAI.ScalarConductivity.diagonalization_pullback line 188
  18. abbrev OAI.ScalarConductivity.Symmetric3 line 197
  19. def OAI.ScalarConductivity.spectralExtension line 199
  20. lemma OAI.ScalarConductivity.spectralExtension_rep_mem line 202
  21. lemma OAI.ScalarConductivity.continuous_diagonal_pullback line 213
  22. lemma OAI.ScalarConductivity.continuous_diagonal_pushforward line 218
  23. lemma OAI.ScalarConductivity.tendsto_diagonal_pullback line 223
  24. lemma OAI.ScalarConductivity.limit_diagonal_rep line 233
  25. theorem OAI.ScalarConductivity.isOpen_spectralExtension line 244