OAI/Analysis/LpDimension/SpectralProjection.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SubpolynomialLp.exponential_sum_integral line 15
  2. theorem OAI.SubpolynomialLp.gramHermitian line 48
  3. def OAI.SubpolynomialLp.gramEigenMatrix line 51
  4. def OAI.SubpolynomialLp.gramProjection line 54
  5. lemma OAI.SubpolynomialLp.gramEigenMatrix_zero line 58
  6. lemma OAI.SubpolynomialLp.gram_heat_apply line 67
  7. lemma OAI.SubpolynomialLp.gramProjection_heat_integral line 87
  8. lemma OAI.SubpolynomialLp.gramEigenMatrix_gram line 105
  9. lemma OAI.SubpolynomialLp.gramProjection_mul_eigenMatrix line 130
  10. lemma OAI.SubpolynomialLp.gramProjection_mul_self line 140
  11. lemma OAI.SubpolynomialLp.gramProjection_idempotent line 154
  12. lemma OAI.SubpolynomialLp.gramProjection_symmetric line 160
  13. lemma OAI.SubpolynomialLp.mul_gramProjection_of_fix line 165
  14. lemma OAI.SubpolynomialLp.gramProjection_eq_of_mutual_fix line 169
  15. lemma OAI.SubpolynomialLp.gramProjection_right_diagonal line 179