OAI/Analysis/FactorGeneration/UniformPartitions.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Finite equal-trace partitions in an actual diffuse algebra, constructed by repeated exact trace cuts. No matrix units or comparison theorem are assumed. These partitions do not yet approximate an arbitrary given spectral partition.

  1. theorem OAI.Generator.Tracial.exists_uniform_trace_partition line 23
  2. theorem OAI.Generator.Tracial.exists_uniform_trace_extension line 88
  3. theorem OAI.Generator.Tracial.exists_rounded_trace_subprojection line 150
  4. theorem OAI.Generator.Tracial.exists_uniform_trace_approximation line 182
  5. theorem OAI.Generator.Tracial.exists_dyadic_trace_approximation line 221
  6. theorem OAI.Generator.Tracial.norm₂_finset_sum_le line 245
  7. theorem OAI.Generator.Tracial.exists_dyadic_spectral_sum_approximation line 258
  8. theorem OAI.Generator.Tracial.exists_finite_uniform_spectral_approximation line 311