OAI/Analysis/OInfinity/NegativeCorner.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

The explicit negative-corner stabilization of a canonical row

The row in 1 - s₀s₀* is the transport of the direct sum of the canonical row and its tail compression in 1 - s₀s₀* - s₁s₁*. All projections and row identities below are literal algebraic formulas.

  1. def OAI.WeakPureInfiniteness.canonicalTailProjection line 20

    Source documentation

    The remaining projection after the first n canonical ranges.

    def canonicalTailProjection (s : ℕ → E) (n : ℕ) : E :=
…
  2. lemma OAI.WeakPureInfiniteness.canonicalTailProjection_zero line 23
  3. lemma OAI.WeakPureInfiniteness.canonicalTailProjection_succ line 26
  4. lemma OAI.WeakPureInfiniteness.canonicalTailProjection_add line 32
  5. lemma OAI.WeakPureInfiniteness.canonicalTailProjection_star line 43
  6. lemma OAI.WeakPureInfiniteness.canonicalTailProjection_mul_generator line 47
  7. lemma OAI.WeakPureInfiniteness.canonicalTailProjection_generator_star line 63
  8. lemma OAI.WeakPureInfiniteness.canonicalTailProjection_idempotent line 71
  9. lemma OAI.WeakPureInfiniteness.canonicalTailProjection_ne_zero line 93
  10. def OAI.WeakPureInfiniteness.canonicalNegativeProjection line 106

    Source documentation

    The negative-unit corner used in the direct-sum stabilization.

    def canonicalNegativeProjection (s : ℕ → E) : E := canonicalTailProjection s 2

    Mentions: OAI.WeakPureInfiniteness.canonicalTailProjection

  11. def OAI.WeakPureInfiniteness.canonicalNegativeRow line 109

    Source documentation

    Transport of sᵢ ⊕ (sᵢ₊₂ p) along the rectangular row [s₁,p].

    def canonicalNegativeRow (s : ℕ → E) (i : ℕ) : E :=
…
  12. lemma OAI.WeakPureInfiniteness.canonicalNegativeProjection_le_tail line 112
  13. lemma OAI.WeakPureInfiniteness.canonicalNegativeRow_gram line 128
  14. lemma OAI.WeakPureInfiniteness.canonicalNegativeRow_support line 169
  15. lemma OAI.WeakPureInfiniteness.canonicalNegativeRow_range_term line 185
  16. lemma OAI.WeakPureInfiniteness.canonicalNegativeRow_residual line 221
  17. lemma OAI.WeakPureInfiniteness.canonicalNegativeRow_spare line 238
  18. lemma OAI.WeakPureInfiniteness.canonicalTailProjection_commutes line 271
  19. lemma OAI.WeakPureInfiniteness.canonicalNegativeRow_commutes line 277