OAI/Analysis/PureInfiniteness/JointSpectralPartition.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Finite joint partitions with an explicit nonunital origin condition. The reconstruction bound is the mesh size; no estimate depends on the number of lattice cells.

  1. def OAI.WeakPureInfiniteness.jointGrid line 17
  2. def OAI.WeakPureInfiniteness.jointGridReconstruction line 19
  3. lemma OAI.WeakPureInfiniteness.scalarStarHom_reconstruction line 23
  4. lemma OAI.WeakPureInfiniteness.norm_jointGridReconstruction_sub_le line 35
  5. lemma OAI.WeakPureInfiniteness.jointGridPlateau_in_kernel line 66
  6. lemma OAI.WeakPureInfiniteness.jointGridHat_in_kernel line 76
  7. lemma OAI.WeakPureInfiniteness.jointGrid_bound_at_ceil line 89
  8. lemma OAI.WeakPureInfiniteness.exists_jointGrid_bound line 108
  9. lemma OAI.WeakPureInfiniteness.norm_sum_retained_hats_le line 115