OAI/Analysis/FactorGeneration/QuotientCorners.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Exact coordinate centering in projection corners whose traces have a uniform positive lower bound. The corner scalar is divided by its actual trace; no global-centering-to-corner-centering implication is assumed.

  1. theorem OAI.Generator.Tracial.corner_trace_norm_lower line 19
  2. def OAI.Generator.Tracial.boundedCornerScalar line 23
  3. def OAI.Generator.Tracial.boundedCornerCenter line 35
  4. theorem OAI.Generator.Tracial.boundedCornerCenter_trace line 39
  5. theorem OAI.Generator.Tracial.boundedCornerCenter_supported line 51
  6. theorem OAI.Generator.Tracial.boundedCornerCenter_quotient line 63
  7. theorem OAI.Generator.Tracial.quotientMap_eq_of_eventuallyEq line 104
  8. theorem OAI.Generator.Tracial.exists_uniform_positive_corner_representative line 112
  9. theorem OAI.Generator.Tracial.exists_eventually_positive_corner_representative line 167
  10. theorem OAI.Generator.Tracial.exists_eventually_centered_corner_representatives line 209
  11. theorem OAI.Generator.Tracial.exists_supported_centered_contraction line 253