OAI/Analysis/InterpolatedFactors/Interpolation.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.FreeGroupFactorMain.Interpolation.selectedProjection_trace line 13
  2. theorem OAI.FreeGroupFactorMain.Interpolation.interpolationScale_pos line 20
  3. theorem OAI.FreeGroupFactorMain.Interpolation.Model.toRankTwo line 23
  4. theorem OAI.FreeGroupFactorMain.Interpolation.Model.allIsomorphic line 33
  5. theorem OAI.FreeGroupFactorMain.Interpolation.Model.projection_exists line 39
  6. theorem OAI.FreeGroupFactorMain.Interpolation.Model.allPositive line 50
  7. theorem OAI.FreeGroupFactorMain.Interpolation.Model.fundamentalGroup_eq line 61
  8. theorem OAI.FreeGroupFactorMain.Interpolation.parameterModel_top line 69
  9. theorem OAI.FreeGroupFactorMain.Interpolation.parameterModel_nat line 73
  10. theorem OAI.FreeGroupFactorMain.Interpolation.parameterModel_nonnatural line 80
  11. theorem OAI.FreeGroupFactorMain.Interpolation.parameterModel_valid line 85
  12. theorem OAI.FreeGroupFactorMain.Interpolation.allInterpolatedIsomorphic line 101

    Distinct definitions of this name: ComparatorChallenges/InterpolatedFactors.lean:216 (same statement text; different proof or body). Qualify references as OAI.FreeGroupFactorMain.Interpolation.allInterpolatedIsomorphic@path.

  13. theorem OAI.FreeGroupFactorMain.Interpolation.allInterpolatedAmplifications line 106
  14. theorem OAI.FreeGroupFactorMain.Interpolation.allInterpolatedFundamentalGroups line 114
  15. theorem OAI.FreeGroupFactorMain.Amplification.double_corner_matrix_iff line 123
  16. theorem OAI.FreeGroupFactorMain.Amplification.corner_weight_tensor_formula line 149
  17. theorem OAI.FreeGroupFactorMain.Interpolation.standardCornerScale_pos line 166
  18. theorem OAI.FreeGroupFactorMain.Interpolation.standardCornerScale_parameter line 173
  19. theorem OAI.FreeGroupFactorMain.Interpolation.standardCornerScale_two line 182
  20. theorem OAI.FreeGroupFactorMain.Interpolation.interpolationScale_parameter line 185
  21. theorem OAI.FreeGroupFactorMain.Interpolation.ofReal_parameter_valid line 190
  22. theorem OAI.FreeGroupFactorMain.Interpolation.interpolatedFactor_nat line 194
  23. theorem OAI.FreeGroupFactorMain.Interpolation.interpolatedFactor_infinity line 200
  24. theorem OAI.FreeGroupFactorMain.Interpolation.interpolatedTrace_one line 205
  25. theorem OAI.FreeGroupFactorMain.Interpolation.allInterpolatedProjections line 212
  26. theorem OAI.FreeGroupFactorMain.Interpolation.standardIntegerBaseProjection line 217
  27. theorem OAI.FreeGroupFactorMain.Interpolation.standardIntegerBaseIdentification line 222
  28. theorem OAI.FreeGroupFactorMain.Interpolation.interpolationAmplificationFormula line 236