OAI/Analysis/PureInfiniteness/SpectralGrid.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

A finite one-dimensional localization used in KR02 Remark 7.5. The plateau overlap bound is independent of the size of the finite grid.

  1. def OAI.WeakPureInfiniteness.gridHat line 13
  2. def OAI.WeakPureInfiniteness.gridPlateau line 14
  3. lemma OAI.WeakPureInfiniteness.continuous_gridHat line 16
  4. lemma OAI.WeakPureInfiniteness.continuous_gridPlateau line 19
  5. lemma OAI.WeakPureInfiniteness.gridHat_nonneg line 22
  6. lemma OAI.WeakPureInfiniteness.gridPlateau_bounds line 25
  7. lemma OAI.WeakPureInfiniteness.gridPlateau_mul_gridHat line 29
  8. lemma OAI.WeakPureInfiniteness.gridHat_floor line 36
  9. lemma OAI.WeakPureInfiniteness.gridHat_floor_add_one line 43
  10. lemma OAI.WeakPureInfiniteness.gridHat_eq_zero_off_floor line 51
  11. lemma OAI.WeakPureInfiniteness.sum_gridHat_eq_one line 66
  12. lemma OAI.WeakPureInfiniteness.gridPlateau_eq_zero_off_near_floor line 84
  13. lemma OAI.WeakPureInfiniteness.sum_gridPlateau_le_five line 101

    Source documentation

    Uniform overlap: the estimate does not grow with the finite grid.

    lemma sum_gridPlateau_le_five (s : Finset ℤ) (x : ℝ) :
    ∑ k ∈ s, gridPlateau k x ≤ 5 := by
…

    Mentions: OAI.WeakPureInfiniteness.gridPlateau