OAI/Analysis/PureInfiniteness/JointSpectralEstimates.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

The finite scalar estimates behind the joint nonunital spectral partition. Cells touching the joint origin are omitted; the resulting first-moment error is bounded independently of the number of cells.

  1. lemma OAI.WeakPureInfiniteness.gridHat_le_one line 14
  2. lemma OAI.WeakPureInfiniteness.productGridHat_le_one line 22
  3. lemma OAI.WeakPureInfiniteness.sum_productGridHat_first_moment line 26
  4. def OAI.WeakPureInfiniteness.retainedSpectralCell line 52

    Source documentation

    A retained cell has a coordinate at least two lattice units from zero.

    def retainedSpectralCell (s : I → Finset ℤ) (k : SpectralGridCell s) : Prop :=
…

    Mentions: OAI.WeakPureInfiniteness.SpectralGridCell

  5. instance OAI.WeakPureInfiniteness.(instance at line 55) line 55
  6. lemma OAI.WeakPureInfiniteness.productGridPlateau_zero_at_origin line 59
  7. lemma OAI.WeakPureInfiniteness.joint_spectral_omitted_moment line 68
  8. lemma OAI.WeakPureInfiniteness.joint_spectral_retained_moment line 96
  9. lemma OAI.WeakPureInfiniteness.productGridPlateau_coordinate_sq_le line 115
  10. lemma OAI.WeakPureInfiniteness.sum_productGridPlateau_coordinate_sq_le line 130