OAI/Analysis/Cotype/PatternPairing.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.Cotype.SignFrameRealization line 11
  2. def OAI.Cotype.signFrameChoice line 18
  3. def OAI.Cotype.GrowthPairingData.patternPairing line 30
  4. def OAI.Cotype.GrowthPairingData.patternPrimal line 34
  5. def OAI.Cotype.GrowthPairingData.patternDual line 38
  6. theorem OAI.Cotype.GrowthPairingData.patternPairing_eq line 42
  7. theorem OAI.Cotype.GrowthPairingData.patternPrimal_eq line 54
  8. theorem OAI.Cotype.GrowthPairingData.patternDual_eq line 66
  9. theorem OAI.Cotype.GrowthPairingData.patternPairing_primal_moment line 77
  10. theorem OAI.Cotype.GrowthPairingData.patternPairing_dual_moment line 88
  11. theorem OAI.Cotype.GrowthPairingData.patternPrimal_moment line 99
  12. theorem OAI.Cotype.GrowthPairingData.patternDual_moment line 106