OAI/Analysis/PureInfiniteness/RelativeInnerCalculus.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Finite sums and output compressions of relatively approximately inner maps. These are the coefficient operations required by the local cone proof.

  1. lemma OAI.WeakPureInfiniteness.approximatelyInnerAlong_innerHomCompression line 15
  2. lemma OAI.WeakPureInfiniteness.ApproximatelyInnerAlong.add line 22
  3. lemma OAI.WeakPureInfiniteness.ApproximatelyInnerAlong.outputCompression line 40
  4. lemma OAI.WeakPureInfiniteness.ApproximatelyInnerAlong.finset_sum line 64