OAI/Analysis/PureInfiniteness/SpectralProductGrid.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Finite-dimensional product grids for the joint spectral localization in KR02 Remark 7.5. The overlap bound depends on the number of coordinates, not on the mesh size or number of cells.

  1. lemma OAI.WeakPureInfiniteness.sum_gridHat_first_moment line 14
  2. abbrev OAI.WeakPureInfiniteness.SpectralGridCell line 35
  3. def OAI.WeakPureInfiniteness.productGridHat line 37
  4. def OAI.WeakPureInfiniteness.productGridPlateau line 40
  5. lemma OAI.WeakPureInfiniteness.productGridHat_nonneg line 43
  6. lemma OAI.WeakPureInfiniteness.productGridPlateau_bounds line 47
  7. lemma OAI.WeakPureInfiniteness.productGridPlateau_mul_hat line 53
  8. lemma OAI.WeakPureInfiniteness.continuous_productGridHat line 59
  9. lemma OAI.WeakPureInfiniteness.continuous_productGridPlateau line 64
  10. lemma OAI.WeakPureInfiniteness.sum_productGridHat line 71
  11. lemma OAI.WeakPureInfiniteness.sum_productGridPlateau_le line 80