OAI/Analysis/FactorGeneration/TensorRefinement.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

A finite refinement retaining its actual commuting matrix factor. The relation composes, so finite energy descent can retain these witnesses.

  1. def OAI.Generator.FiniteMatrixStage.TensorExtension line 16
  2. theorem OAI.Generator.FiniteMatrixStage.TensorExtension.algebra_le line 21
  3. theorem OAI.Generator.FiniteMatrixStage.TensorExtension.refl line 27
  4. theorem OAI.Generator.FiniteMatrixStage.TensorExtension.trans line 35
  5. theorem OAI.Generator.FiniteMatrixStage.exists_tensor_refinement_descent line 59
  6. theorem OAI.Generator.FiniteMatrixStage.exists_tensor_finite_family_descent line 107
  7. theorem OAI.Generator.FiniteMatrixStage.exists_tensor_iterated_energy_descent line 124
  8. theorem OAI.Generator.FiniteMatrixStage.exists_tensor_finite_matrix_energy_budget line 141
  9. theorem OAI.Generator.FiniteMatrixStage.exists_countable_tensor_refinement line 171