OAI/Analysis/LpDimension/HeatKernel.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SubpolynomialLp.matrix_pow_nonneg line 16
  2. lemma OAI.SubpolynomialLp.matrix_tsum_apply line 27
  3. lemma OAI.SubpolynomialLp.matrix_exp_pos line 32
  4. lemma OAI.SubpolynomialLp.matrix_exp_scalar line 45
  5. lemma OAI.SubpolynomialLp.matrix_exp_add_scalar line 51
  6. lemma OAI.SubpolynomialLp.matrix_exp_pos_of_offdiag line 56
  7. lemma OAI.SubpolynomialLp.matrix_exp_conj_unitary line 79
  8. lemma OAI.SubpolynomialLp.matrix_exp_spectral line 86
  9. def OAI.SubpolynomialLp.spectralKernelProjection line 98
  10. lemma OAI.SubpolynomialLp.matrix_exp_neg_tendsto line 102
  11. lemma OAI.SubpolynomialLp.mul_spectralKernelProjection line 128
  12. def OAI.SubpolynomialLp.weightedGenerator line 145
  13. def OAI.SubpolynomialLp.symmetricGenerator line 148
  14. def OAI.SubpolynomialLp.weightedHeatKernel line 151
  15. lemma OAI.SubpolynomialLp.weightedHeatKernel_generator line 154
  16. lemma OAI.SubpolynomialLp.weightedHeatKernel_zero line 167
  17. lemma OAI.SubpolynomialLp.weightedHeatKernel_hasDerivAt line 171
  18. lemma OAI.SubpolynomialLp.weightedHeatKernel_continuous line 182
  19. lemma OAI.SubpolynomialLp.symmetricGenerator_symmetric line 186
  20. lemma OAI.SubpolynomialLp.weightedHeatKernel_symmetric line 191
  21. lemma OAI.SubpolynomialLp.weightedHeatKernel_semigroup line 198
  22. lemma OAI.SubpolynomialLp.symmetricGenerator_posSemidef line 220
  23. lemma OAI.SubpolynomialLp.weightedHeatKernel_entry_hasDerivAt line 225
  24. lemma OAI.SubpolynomialLp.weightedHeatKernel_pos line 238
  25. lemma OAI.SubpolynomialLp.weightedHeatKernel_tendsto line 250
  26. lemma OAI.SubpolynomialLp.weightedHeatKernel_limit_ker line 257