OAI/Analysis/PureInfiniteness/JointSpectralSecondMoment.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The sampled square has error at most the square of the mesh size. Together with the first moment this bounds the concrete return map's Schwarz defect.

  1. def OAI.WeakPureInfiniteness.jointGridSquareReconstruction line 16
  2. lemma OAI.WeakPureInfiniteness.scalarStarHom_squareReconstruction line 20
  3. lemma OAI.WeakPureInfiniteness.norm_jointGridSquareReconstruction_sub_le line 33