OAI/Analysis/PureInfiniteness/SpectralGridCFC.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Finite spectral localization with a uniform overlap bound. These are the one-coordinate building blocks of KR02 Remark 7.5.

  1. def OAI.WeakPureInfiniteness.gridHatElement line 15
  2. def OAI.WeakPureInfiniteness.gridPlateauElement line 18
  3. lemma OAI.WeakPureInfiniteness.gridHatElement_nonneg line 21
  4. lemma OAI.WeakPureInfiniteness.gridPlateauElement_nonneg line 25
  5. lemma OAI.WeakPureInfiniteness.gridPlateauElement_mul_gridHatElement line 30
  6. lemma OAI.WeakPureInfiniteness.sum_gridHatElement_eq_one line 45
  7. lemma OAI.WeakPureInfiniteness.norm_sum_gridPlateauElement_le line 63

    Source documentation

    The constant 5 depends only on one-dimensional overlap, not the number of spectral cells. This keeps subsequent cp estimates uniform under refinement.

    lemma norm_sum_gridPlateauElement_le (a : A) (r : ℝ) (s : Finset ℤ) :
    ‖∑ k ∈ s, gridPlateauElement a r k‖ ≤ 5 := by
…

    Mentions: OAI.WeakPureInfiniteness.gridPlateauElement