OAI/Analysis/InterpolatedFactors/CornerStabilization.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.FreeGroupFactorMain.Amplification.cornerStabilization_weight_iff line 15
  2. theorem OAI.FreeGroupFactorMain.Amplification.doubleDiagonal_matrix line 30
  3. theorem OAI.FreeGroupFactorMain.Amplification.doubleFiniteDiagonal_supported line 38
  4. theorem OAI.FreeGroupFactorMain.Amplification.finiteFlatten_supported line 66
  5. def OAI.FreeGroupFactorMain.Amplification.cornerFiniteProjection line 76
  6. theorem OAI.FreeGroupFactorMain.Amplification.cornerFiniteProjection_projection line 80
  7. theorem OAI.FreeGroupFactorMain.Amplification.projection_weight_of_trace line 91
  8. theorem OAI.FreeGroupFactorMain.Amplification.corner_projection_weight line 99
  9. theorem OAI.FreeGroupFactorMain.Amplification.cornerStabilization_projection_exists line 112
  10. def OAI.FreeGroupFactorMain.Amplification.nestedNormalizedIso line 138
  11. theorem OAI.FreeGroupFactorMain.Amplification.cornerStabilization_allPositive line 154