Length comparison for stabilized two-term pages with exhaustive target boundaries.

theorem AlgebraicAnalysis.TwoTermPageLength.exists_boundary_eq_top_of_iSup_eq_top {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] [IsNoetherian R M] (D : ℕ →o Submodule R M) (hD : ⨆ (r : ℕ), D r = ⊤) : ∃ (N : ℕ), D N = ⊤

theorem AlgebraicAnalysis.TwoTermPageLength.twoTermPage_length_target_le_source {R : Type u_1} [Ring R] (A : ℕ → Type u_2) (C : ℕ → Type u_3) [(r : ℕ) → AddCommGroup (A r)] [(r : ℕ) → Module R (A r)] [(r : ℕ) → AddCommGroup (C r)] [(r : ℕ) → Module R (C r)] (hA0 : IsFiniteLength R (A 0)) (hC0 : IsFiniteLength R (C 0)) (d : (r : ℕ) → A r →ₗ[R] C r) (sourceSucc : (r : ℕ) → A (r + 1) ≃ₗ[R] ↥(d r).ker) (targetSucc : (r : ℕ) → C (r + 1) ≃ₗ[R] C r ⧸ (d r).range) (N : ℕ) [Subsingleton (C N)] : Module.length R (C 0) ≤ Module.length R (A 0)