OAI/Analysis/StrictMeans/CriticalCovariance.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.StrictInverseFirstPower.affineUpperHomeomorph line 11
  2. lemma OAI.StrictInverseFirstPower.affineUpperHomeomorph_apply line 29
  3. def OAI.StrictInverseFirstPower.targetRebase line 32
  4. lemma OAI.StrictInverseFirstPower.targetRebase_injective line 35
  5. lemma OAI.StrictInverseFirstPower.criticalMap_rebase line 43
  6. lemma OAI.StrictInverseFirstPower.criticalMap_rebase_eq_iff line 55
  7. lemma OAI.StrictInverseFirstPower.affineProduct_im line 60
  8. def OAI.StrictInverseFirstPower.heightRebaseScale line 63
  9. lemma OAI.StrictInverseFirstPower.heightRebaseScale_pos line 66
  10. lemma OAI.StrictInverseFirstPower.criticalHeight_rebase line 71
  11. lemma OAI.StrictInverseFirstPower.reciprocalPotential_rebase line 82
  12. lemma OAI.StrictInverseFirstPower.goodPair_rebase line 95
  13. lemma OAI.StrictInverseFirstPower.goodPair_rebase_iff line 117